%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ROB017-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 12:36:16 PM UTC 2026
% Result : Unsatisfiable 134.53s 40.79s
% Output : Refutation 281.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 30
% Syntax : Number of formulae : 212 ( 60 unt; 23 def)
% Number of atoms : 520 ( 156 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 601 ( 293 ~; 288 |; 0 &)
% ( 20 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 22 ( 20 usr; 21 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 82 ( 0 sgn 82 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_add) ).
fof(f2,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f3,axiom,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(X0,negate(X1))))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',robbins_axiom) ).
fof(f4,axiom,
negate(add(f,add(f,h))) = negate(h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition1) ).
fof(f5,axiom,
negate(add(f,add(f,add(f,h)))) = negate(h),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condition2) ).
fof(f6,plain,
negate(h) = negate(add(f,add(f,add(f,h)))),
inference(reorient_equations,[],[f5]) ).
fof(f9,negated_conjecture,
add(f,add(f,add(f,h))) != add(f,add(f,h)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_result) ).
fof(f10,plain,
add(f,add(f,h)) != add(f,add(f,add(f,h))),
inference(reorient_equations,[],[f9]) ).
fof(f11,definition,
sF0 = add(f,h),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f12,plain,
add(f,h) = sF0,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF1 = add(f,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f14,plain,
add(f,sF0) = sF1,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF2 = add(f,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f16,plain,
add(f,sF1) = sF2,
inference(reorient_equations,[],[f15]) ).
fof(f17,plain,
sF1 != sF2,
inference(definition_folding,[],[f10,f16,f14,f12,f14,f12]) ).
fof(f19,definition,
( spl3_1
<=> sF1 = sF2 ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f22,plain,
~ spl3_1,
inference(avatar_split_clause,[],[f17,f19]) ).
fof(f24,definition,
( spl3_2
<=> negate(h) = negate(add(f,add(f,add(f,h)))) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f26,plain,
( negate(h) = negate(add(f,add(f,add(f,h))))
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f27,plain,
spl3_2,
inference(avatar_split_clause,[],[f6,f24]) ).
fof(f29,definition,
( spl3_3
<=> negate(add(f,add(f,h))) = negate(h) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f31,plain,
( negate(add(f,add(f,h))) = negate(h)
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f29]) ).
fof(f32,plain,
spl3_3,
inference(avatar_split_clause,[],[f4,f29]) ).
fof(f34,definition,
( spl3_4
<=> add(f,h) = sF0 ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f36,plain,
( add(f,h) = sF0
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f37,plain,
spl3_4,
inference(avatar_split_clause,[],[f12,f34]) ).
fof(f39,definition,
( spl3_5
<=> add(f,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f41,plain,
( add(f,sF0) = sF1
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f39]) ).
fof(f42,plain,
spl3_5,
inference(avatar_split_clause,[],[f14,f39]) ).
fof(f44,definition,
( spl3_6
<=> add(f,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f46,plain,
( add(f,sF1) = sF2
| ~ spl3_6 ),
inference(avatar_component_clause,[],[f44]) ).
fof(f47,plain,
spl3_6,
inference(avatar_split_clause,[],[f16,f44]) ).
fof(f59,plain,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(X1,negate(X0))))) = X1,
inference(superposition,[],[f3,f1]) ).
fof(f60,plain,
( f = negate(add(negate(h),negate(add(f,negate(add(f,add(f,h)))))))
| ~ spl3_2 ),
inference(superposition,[],[f3,f26]) ).
fof(f62,plain,
( ! [X0] : negate(add(negate(add(X0,add(f,add(f,add(f,h))))),negate(add(X0,negate(h))))) = X0
| ~ spl3_2 ),
inference(superposition,[],[f3,f26]) ).
fof(f65,plain,
! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(negate(X0),X1)))) = X1,
inference(superposition,[],[f3,f1]) ).
fof(f66,plain,
! [X0,X1] : negate(add(X0,X1)) = negate(add(negate(add(negate(add(X0,X1)),add(X0,negate(X1)))),X0)),
inference(superposition,[],[f3,f3]) ).
fof(f67,plain,
! [X0,X1] : negate(add(X0,X1)) = negate(add(X0,negate(add(negate(add(X0,X1)),add(X0,negate(X1)))))),
inference(forward_demodulation,[],[f66,f1]) ).
fof(f69,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,add(f,add(f,add(f,h))))))) = X0
| ~ spl3_2 ),
inference(forward_demodulation,[],[f62,f1]) ).
fof(f70,plain,
( f = negate(add(negate(h),negate(add(f,negate(h)))))
| ~ spl3_2
| ~ spl3_3 ),
inference(forward_demodulation,[],[f60,f31]) ).
fof(f81,plain,
! [X0,X1] : negate(add(X0,X1)) = negate(add(X0,negate(add(add(X0,negate(X1)),negate(add(X0,X1)))))),
inference(forward_demodulation,[],[f67,f1]) ).
fof(f82,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,add(f,add(f,sF0)))))) = X0
| ~ spl3_2
| ~ spl3_4 ),
inference(forward_demodulation,[],[f69,f36]) ).
fof(f84,definition,
( spl3_10
<=> f = negate(add(negate(h),negate(add(f,negate(h))))) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f86,plain,
( f = negate(add(negate(h),negate(add(f,negate(h)))))
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f84]) ).
fof(f87,plain,
( spl3_10
| ~ spl3_2
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f70,f29,f24,f84]) ).
fof(f88,plain,
! [X0,X1] : negate(add(X0,X1)) = negate(add(X0,negate(add(X0,add(negate(X1),negate(add(X0,X1))))))),
inference(forward_demodulation,[],[f81,f2]) ).
fof(f89,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,add(f,sF1))))) = X0
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5 ),
inference(forward_demodulation,[],[f82,f41]) ).
fof(f90,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,sF2)))) = X0
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(forward_demodulation,[],[f89,f46]) ).
fof(f91,plain,
( ! [X0] : negate(add(negate(add(X0,sF2)),negate(add(X0,negate(h))))) = X0
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(forward_demodulation,[],[f90,f1]) ).
fof(f92,plain,
( ! [X0] : add(f,add(h,X0)) = add(sF0,X0)
| ~ spl3_4 ),
inference(superposition,[],[f2,f36]) ).
fof(f93,plain,
( ! [X0] : add(f,add(sF0,X0)) = add(sF1,X0)
| ~ spl3_5 ),
inference(superposition,[],[f2,f41]) ).
fof(f95,plain,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X1,add(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f101,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X2,add(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f102,plain,
! [X2,X0,X1] : add(X0,X1) = negate(add(negate(add(add(X0,X1),X2)),negate(add(X0,add(X1,negate(X2)))))),
inference(superposition,[],[f3,f2]) ).
fof(f103,plain,
! [X2,X0,X1] : add(X0,X1) = negate(add(negate(add(X0,add(X1,X2))),negate(add(X0,add(X1,negate(X2)))))),
inference(forward_demodulation,[],[f102,f2]) ).
fof(f107,plain,
( ! [X0] : add(f,add(sF1,X0)) = add(sF2,X0)
| ~ spl3_6 ),
inference(superposition,[],[f2,f46]) ).
fof(f132,plain,
( f = negate(add(negate(h),negate(add(f,negate(add(f,h))))))
| ~ spl3_3 ),
inference(superposition,[],[f3,f31]) ).
fof(f134,plain,
( ! [X0] : negate(add(negate(add(X0,add(f,add(f,h)))),negate(add(X0,negate(h))))) = X0
| ~ spl3_3 ),
inference(superposition,[],[f3,f31]) ).
fof(f135,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,add(f,add(f,h)))))) = X0
| ~ spl3_3 ),
inference(forward_demodulation,[],[f134,f1]) ).
fof(f137,plain,
( f = negate(add(negate(h),negate(add(f,negate(sF0)))))
| ~ spl3_3
| ~ spl3_4 ),
inference(forward_demodulation,[],[f132,f36]) ).
fof(f139,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,add(f,sF0))))) = X0
| ~ spl3_3
| ~ spl3_4 ),
inference(forward_demodulation,[],[f135,f36]) ).
fof(f142,definition,
( spl3_12
<=> f = negate(add(negate(h),negate(add(f,negate(sF0))))) ),
introduced(definition,[new_symbols(definition,[spl3_12])],[avatar_definition]) ).
fof(f144,plain,
( f = negate(add(negate(h),negate(add(f,negate(sF0)))))
| ~ spl3_12 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f145,plain,
( spl3_12
| ~ spl3_3
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f137,f34,f29,f142]) ).
fof(f151,plain,
( ! [X0] : negate(add(negate(add(X0,negate(h))),negate(add(X0,sF1)))) = X0
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(forward_demodulation,[],[f139,f41]) ).
fof(f153,plain,
( ! [X0] : negate(add(negate(add(X0,sF1)),negate(add(X0,negate(h))))) = X0
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(forward_demodulation,[],[f151,f1]) ).
fof(f164,plain,
( ! [X0] : negate(add(negate(add(X0,sF1)),negate(add(negate(h),X0)))) = X0
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(superposition,[],[f153,f1]) ).
fof(f243,plain,
! [X0,X1] : negate(add(negate(add(X0,X1)),negate(add(negate(X0),X1)))) = X1,
inference(superposition,[],[f65,f1]) ).
fof(f480,plain,
! [X2,X3,X0,X1] : add(add(X0,X1),add(X3,X2)) = add(X3,add(X0,add(X1,X2))),
inference(superposition,[],[f101,f101]) ).
fof(f502,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(add(X2,X0),X1),
inference(superposition,[],[f1,f101]) ).
fof(f511,plain,
( ! [X0,X1] : add(sF0,add(X1,X0)) = add(f,add(X0,add(h,X1)))
| ~ spl3_4 ),
inference(superposition,[],[f92,f101]) ).
fof(f517,plain,
! [X2,X3,X0,X1] : add(X0,add(X1,add(X2,X3))) = add(X2,add(X3,add(X0,X1))),
inference(superposition,[],[f2,f101]) ).
fof(f539,plain,
! [X2,X3,X0,X1] : add(X3,add(X0,add(X1,X2))) = add(X0,add(X1,add(X3,X2))),
inference(forward_demodulation,[],[f480,f2]) ).
fof(f566,plain,
( add(f,f) = negate(add(negate(h),negate(add(f,add(f,negate(add(f,h)))))))
| ~ spl3_2 ),
inference(superposition,[],[f103,f26]) ).
fof(f629,plain,
( add(f,f) = negate(add(negate(h),negate(add(f,add(f,negate(sF0))))))
| ~ spl3_2
| ~ spl3_4 ),
inference(forward_demodulation,[],[f566,f36]) ).
fof(f648,definition,
( spl3_29
<=> add(f,f) = negate(add(negate(h),negate(add(f,add(f,negate(sF0)))))) ),
introduced(definition,[new_symbols(definition,[spl3_29])],[avatar_definition]) ).
fof(f650,plain,
( add(f,f) = negate(add(negate(h),negate(add(f,add(f,negate(sF0))))))
| ~ spl3_29 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,plain,
( spl3_29
| ~ spl3_2
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f629,f34,f24,f648]) ).
fof(f698,plain,
( ! [X0,X1] : negate(add(negate(add(add(negate(add(X0,sF1)),negate(add(X0,negate(h)))),X1)),negate(add(X1,X0)))) = X1
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(superposition,[],[f59,f153]) ).
fof(f699,plain,
( ! [X0,X1] : negate(add(negate(add(add(negate(add(X0,sF2)),negate(add(X0,negate(h)))),X1)),negate(add(X1,X0)))) = X1
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(superposition,[],[f59,f91]) ).
fof(f756,plain,
( ! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(add(negate(add(X0,sF2)),negate(add(X0,negate(h)))),X1)))) = X1
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(forward_demodulation,[],[f699,f1]) ).
fof(f757,plain,
( ! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(add(negate(add(X0,sF1)),negate(add(X0,negate(h)))),X1)))) = X1
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(forward_demodulation,[],[f698,f1]) ).
fof(f795,plain,
( ! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(negate(add(X0,sF2)),add(negate(add(X0,negate(h))),X1))))) = X1
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(forward_demodulation,[],[f756,f2]) ).
fof(f796,plain,
( ! [X0,X1] : negate(add(negate(add(X1,X0)),negate(add(negate(add(X0,sF1)),add(negate(add(X0,negate(h))),X1))))) = X1
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5 ),
inference(forward_demodulation,[],[f757,f2]) ).
fof(f983,plain,
( negate(add(f,negate(h))) = negate(add(negate(add(negate(add(f,negate(h))),sF1)),f))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_10 ),
inference(superposition,[],[f164,f86]) ).
fof(f1014,plain,
( negate(add(f,negate(h))) = negate(add(f,negate(add(negate(add(f,negate(h))),sF1))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_10 ),
inference(forward_demodulation,[],[f983,f1]) ).
fof(f1026,plain,
( negate(add(f,negate(h))) = negate(add(f,negate(add(sF1,negate(add(f,negate(h)))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_10 ),
inference(forward_demodulation,[],[f1014,f1]) ).
fof(f1037,definition,
( spl3_42
<=> negate(add(f,negate(h))) = negate(add(f,negate(add(sF1,negate(add(f,negate(h))))))) ),
introduced(definition,[new_symbols(definition,[spl3_42])],[avatar_definition]) ).
fof(f1039,plain,
( negate(add(f,negate(h))) = negate(add(f,negate(add(sF1,negate(add(f,negate(h)))))))
| ~ spl3_42 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1040,plain,
( spl3_42
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f1026,f84,f39,f34,f29,f1037]) ).
fof(f1289,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(add(f,h)),negate(h))))))
| ~ spl3_3 ),
inference(superposition,[],[f88,f31]) ).
fof(f1359,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(f,h)))))))
| ~ spl3_3 ),
inference(forward_demodulation,[],[f1289,f1]) ).
fof(f1392,plain,
( negate(h) = negate(add(f,h))
| ~ spl3_3 ),
inference(forward_demodulation,[],[f1359,f88]) ).
fof(f1399,definition,
( spl3_46
<=> negate(h) = negate(sF0) ),
introduced(definition,[new_symbols(definition,[spl3_46])],[avatar_definition]) ).
fof(f1401,plain,
( negate(h) = negate(sF0)
| ~ spl3_46 ),
inference(avatar_component_clause,[],[f1399]) ).
fof(f1406,plain,
( negate(h) = negate(sF0)
| ~ spl3_3
| ~ spl3_4 ),
inference(forward_demodulation,[],[f1392,f36]) ).
fof(f1411,plain,
( spl3_46
| ~ spl3_3
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f1406,f34,f29,f1399]) ).
fof(f1820,plain,
( negate(add(f,add(f,negate(sF0)))) = negate(add(negate(add(negate(add(f,add(f,negate(sF0)))),h)),add(f,f)))
| ~ spl3_29 ),
inference(superposition,[],[f65,f650]) ).
fof(f1865,plain,
( negate(add(f,add(f,negate(sF0)))) = negate(add(add(f,f),negate(add(negate(add(f,add(f,negate(sF0)))),h))))
| ~ spl3_29 ),
inference(forward_demodulation,[],[f1820,f1]) ).
fof(f1888,plain,
( negate(add(f,add(f,negate(sF0)))) = negate(add(f,add(f,negate(add(negate(add(f,add(f,negate(sF0)))),h)))))
| ~ spl3_29 ),
inference(forward_demodulation,[],[f1865,f2]) ).
fof(f1912,plain,
( negate(add(f,add(f,negate(sF0)))) = negate(add(f,add(f,negate(add(h,negate(add(f,add(f,negate(sF0)))))))))
| ~ spl3_29 ),
inference(forward_demodulation,[],[f1888,f1]) ).
fof(f1927,plain,
( negate(add(f,add(f,negate(h)))) = negate(add(f,add(f,negate(add(h,negate(add(f,add(f,negate(h)))))))))
| ~ spl3_29
| ~ spl3_46 ),
inference(forward_demodulation,[],[f1912,f1401]) ).
fof(f1945,definition,
( spl3_52
<=> negate(add(f,add(f,negate(h)))) = negate(add(f,add(f,negate(add(h,negate(add(f,add(f,negate(h))))))))) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f1947,plain,
( negate(add(f,add(f,negate(h)))) = negate(add(f,add(f,negate(add(h,negate(add(f,add(f,negate(h)))))))))
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f1945]) ).
fof(f1948,plain,
( spl3_52
| ~ spl3_29
| ~ spl3_46 ),
inference(avatar_split_clause,[],[f1927,f1399,f648,f1945]) ).
fof(f1959,definition,
( spl3_54
<=> negate(h) = negate(add(sF1,negate(add(f,add(f,negate(h)))))) ),
introduced(definition,[new_symbols(definition,[spl3_54])],[avatar_definition]) ).
fof(f1961,plain,
( negate(h) = negate(add(sF1,negate(add(f,add(f,negate(h))))))
| ~ spl3_54 ),
inference(avatar_component_clause,[],[f1959]) ).
fof(f2144,plain,
( ! [X0,X1] : add(sF2,add(X1,X0)) = add(f,add(X0,add(sF1,X1)))
| ~ spl3_6 ),
inference(superposition,[],[f107,f101]) ).
fof(f2449,plain,
( negate(h) = negate(add(f,negate(add(negate(add(negate(add(f,negate(sF0))),sF2)),add(negate(add(negate(add(f,negate(sF0))),negate(h))),negate(h))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(superposition,[],[f795,f144]) ).
fof(f2517,plain,
( negate(h) = negate(add(f,negate(add(negate(h),add(negate(add(negate(add(f,negate(sF0))),sF2)),negate(add(negate(add(f,negate(sF0))),negate(h))))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f2449,f101]) ).
fof(f2556,plain,
( negate(h) = negate(add(f,negate(add(negate(h),add(negate(add(negate(add(f,negate(sF0))),sF2)),negate(add(negate(h),negate(add(f,negate(sF0))))))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f2517,f1]) ).
fof(f2591,plain,
( negate(h) = negate(add(f,negate(add(negate(h),add(negate(add(negate(add(f,negate(sF0))),sF2)),f)))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f2556,f144]) ).
fof(f2627,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(negate(add(f,negate(sF0))),sF2)))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f2591,f101]) ).
fof(f2646,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(sF2,negate(add(f,negate(sF0))))))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12 ),
inference(forward_demodulation,[],[f2627,f1]) ).
fof(f2662,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(sF2,negate(add(f,negate(h))))))))))
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12
| ~ spl3_46 ),
inference(forward_demodulation,[],[f2646,f1401]) ).
fof(f2664,definition,
( spl3_75
<=> negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(sF2,negate(add(f,negate(h)))))))))) ),
introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition]) ).
fof(f2666,plain,
( negate(h) = negate(add(f,negate(add(f,add(negate(h),negate(add(sF2,negate(add(f,negate(h))))))))))
| ~ spl3_75 ),
inference(avatar_component_clause,[],[f2664]) ).
fof(f2672,plain,
( spl3_75
| ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12
| ~ spl3_46 ),
inference(avatar_split_clause,[],[f2662,f1399,f142,f44,f39,f34,f24,f2664]) ).
fof(f3037,plain,
( negate(h) = negate(add(add(f,f),negate(add(negate(add(negate(add(f,add(f,negate(sF0)))),sF1)),add(negate(add(negate(add(f,add(f,negate(sF0)))),negate(h))),negate(h))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(superposition,[],[f796,f650]) ).
fof(f3112,plain,
( negate(h) = negate(add(f,add(f,negate(add(negate(add(negate(add(f,add(f,negate(sF0)))),sF1)),add(negate(add(negate(add(f,add(f,negate(sF0)))),negate(h))),negate(h)))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3037,f2]) ).
fof(f3155,plain,
( negate(h) = negate(add(f,add(f,negate(add(negate(h),add(negate(add(negate(add(f,add(f,negate(sF0)))),sF1)),negate(add(negate(add(f,add(f,negate(sF0)))),negate(h)))))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3112,f101]) ).
fof(f3193,plain,
( negate(h) = negate(add(f,add(f,negate(add(negate(h),add(negate(add(negate(add(f,add(f,negate(sF0)))),sF1)),negate(add(negate(h),negate(add(f,add(f,negate(sF0))))))))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3155,f1]) ).
fof(f3230,plain,
( negate(h) = negate(add(f,add(f,negate(add(negate(h),add(negate(add(negate(add(f,add(f,negate(sF0)))),sF1)),add(f,f)))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3193,f650]) ).
fof(f3245,plain,
( negate(h) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(negate(add(f,add(f,negate(sF0)))),sF1)))))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3230,f517]) ).
fof(f3263,plain,
( negate(h) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(sF1,negate(add(f,add(f,negate(sF0)))))))))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29 ),
inference(forward_demodulation,[],[f3245,f1]) ).
fof(f3273,plain,
( negate(h) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(sF1,negate(add(f,add(f,negate(h)))))))))))))
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29
| ~ spl3_46 ),
inference(forward_demodulation,[],[f3263,f1401]) ).
fof(f3279,definition,
( spl3_88
<=> negate(h) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(sF1,negate(add(f,add(f,negate(h))))))))))))) ),
introduced(definition,[new_symbols(definition,[spl3_88])],[avatar_definition]) ).
fof(f3281,plain,
( negate(h) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(sF1,negate(add(f,add(f,negate(h)))))))))))))
| ~ spl3_88 ),
inference(avatar_component_clause,[],[f3279]) ).
fof(f3282,plain,
( spl3_88
| ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29
| ~ spl3_46 ),
inference(avatar_split_clause,[],[f3273,f1399,f648,f39,f34,f29,f3279]) ).
fof(f6295,plain,
( add(f,f) = negate(add(negate(add(f,add(f,add(h,negate(add(f,add(f,negate(h)))))))),negate(add(f,add(f,negate(h))))))
| ~ spl3_52 ),
inference(superposition,[],[f103,f1947]) ).
fof(f6365,plain,
( add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(f,add(f,add(h,negate(add(f,add(f,negate(h))))))))))
| ~ spl3_52 ),
inference(forward_demodulation,[],[f6295,f1]) ).
fof(f6390,plain,
( add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(sF0,add(negate(add(f,add(f,negate(h)))),f)))))
| ~ spl3_4
| ~ spl3_52 ),
inference(forward_demodulation,[],[f6365,f511]) ).
fof(f6400,plain,
( add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(f,add(sF0,negate(add(f,add(f,negate(h)))))))))
| ~ spl3_4
| ~ spl3_52 ),
inference(forward_demodulation,[],[f6390,f101]) ).
fof(f6405,plain,
( add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(sF1,negate(add(f,add(f,negate(h))))))))
| ~ spl3_4
| ~ spl3_5
| ~ spl3_52 ),
inference(forward_demodulation,[],[f6400,f93]) ).
fof(f6418,definition,
( spl3_159
<=> add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(sF1,negate(add(f,add(f,negate(h)))))))) ),
introduced(definition,[new_symbols(definition,[spl3_159])],[avatar_definition]) ).
fof(f6420,plain,
( add(f,f) = negate(add(negate(add(f,add(f,negate(h)))),negate(add(sF1,negate(add(f,add(f,negate(h))))))))
| ~ spl3_159 ),
inference(avatar_component_clause,[],[f6418]) ).
fof(f6421,plain,
( spl3_159
| ~ spl3_4
| ~ spl3_5
| ~ spl3_52 ),
inference(avatar_split_clause,[],[f6405,f1945,f39,f34,f6418]) ).
fof(f8075,plain,
! [X2,X0,X1] : add(X0,add(X1,X2)) = add(X0,add(X2,X1)),
inference(superposition,[],[f95,f502]) ).
fof(f9189,plain,
( f = negate(add(negate(add(f,add(sF1,negate(add(f,negate(h)))))),negate(add(f,negate(h)))))
| ~ spl3_42 ),
inference(superposition,[],[f3,f1039]) ).
fof(f9272,plain,
( f = negate(add(negate(add(f,negate(h))),negate(add(f,add(sF1,negate(add(f,negate(h))))))))
| ~ spl3_42 ),
inference(forward_demodulation,[],[f9189,f1]) ).
fof(f9292,plain,
( f = negate(add(negate(add(f,negate(h))),negate(add(sF2,negate(add(f,negate(h)))))))
| ~ spl3_6
| ~ spl3_42 ),
inference(forward_demodulation,[],[f9272,f107]) ).
fof(f9317,definition,
( spl3_223
<=> f = negate(add(negate(add(f,negate(h))),negate(add(sF2,negate(add(f,negate(h))))))) ),
introduced(definition,[new_symbols(definition,[spl3_223])],[avatar_definition]) ).
fof(f9319,plain,
( f = negate(add(negate(add(f,negate(h))),negate(add(sF2,negate(add(f,negate(h)))))))
| ~ spl3_223 ),
inference(avatar_component_clause,[],[f9317]) ).
fof(f9320,plain,
( spl3_223
| ~ spl3_6
| ~ spl3_42 ),
inference(avatar_split_clause,[],[f9292,f1037,f44,f9317]) ).
fof(f18770,plain,
( negate(add(sF2,negate(add(f,negate(h))))) = negate(add(negate(add(add(f,negate(h)),negate(add(sF2,negate(add(f,negate(h))))))),f))
| ~ spl3_223 ),
inference(superposition,[],[f243,f9319]) ).
fof(f18875,plain,
( negate(add(sF2,negate(add(f,negate(h))))) = negate(add(f,negate(add(add(f,negate(h)),negate(add(sF2,negate(add(f,negate(h)))))))))
| ~ spl3_223 ),
inference(forward_demodulation,[],[f18770,f1]) ).
fof(f18904,plain,
( negate(add(sF2,negate(add(f,negate(h))))) = negate(add(f,negate(add(f,add(negate(h),negate(add(sF2,negate(add(f,negate(h))))))))))
| ~ spl3_223 ),
inference(forward_demodulation,[],[f18875,f2]) ).
fof(f18935,plain,
( negate(h) = negate(add(sF2,negate(add(f,negate(h)))))
| ~ spl3_75
| ~ spl3_223 ),
inference(forward_demodulation,[],[f18904,f2666]) ).
fof(f18948,definition,
( spl3_402
<=> negate(h) = negate(add(sF2,negate(add(f,negate(h))))) ),
introduced(definition,[new_symbols(definition,[spl3_402])],[avatar_definition]) ).
fof(f18950,plain,
( negate(h) = negate(add(sF2,negate(add(f,negate(h)))))
| ~ spl3_402 ),
inference(avatar_component_clause,[],[f18948]) ).
fof(f18951,plain,
( spl3_402
| ~ spl3_75
| ~ spl3_223 ),
inference(avatar_split_clause,[],[f18935,f9317,f2664,f18948]) ).
fof(f22316,plain,
( sF2 = negate(add(negate(add(sF2,add(f,negate(h)))),negate(h)))
| ~ spl3_402 ),
inference(superposition,[],[f3,f18950]) ).
fof(f22426,plain,
( sF2 = negate(add(negate(h),negate(add(sF2,add(f,negate(h))))))
| ~ spl3_402 ),
inference(forward_demodulation,[],[f22316,f1]) ).
fof(f22462,plain,
( sF2 = negate(add(negate(h),negate(add(f,add(negate(h),sF2)))))
| ~ spl3_402 ),
inference(forward_demodulation,[],[f22426,f101]) ).
fof(f22511,plain,
( sF2 = negate(add(negate(h),negate(add(f,add(sF2,negate(h))))))
| ~ spl3_402 ),
inference(forward_demodulation,[],[f22462,f8075]) ).
fof(f22541,definition,
( spl3_461
<=> sF2 = negate(add(negate(h),negate(add(f,add(sF2,negate(h)))))) ),
introduced(definition,[new_symbols(definition,[spl3_461])],[avatar_definition]) ).
fof(f22544,plain,
( spl3_461
| ~ spl3_402 ),
inference(avatar_split_clause,[],[f22511,f18948,f22541]) ).
fof(f31338,plain,
( negate(add(sF1,negate(add(f,add(f,negate(h)))))) = negate(add(negate(add(add(f,add(f,negate(h))),negate(add(sF1,negate(add(f,add(f,negate(h)))))))),add(f,f)))
| ~ spl3_159 ),
inference(superposition,[],[f243,f6420]) ).
fof(f31472,plain,
( negate(add(sF1,negate(add(f,add(f,negate(h)))))) = negate(add(add(f,f),negate(add(add(f,add(f,negate(h))),negate(add(sF1,negate(add(f,add(f,negate(h))))))))))
| ~ spl3_159 ),
inference(forward_demodulation,[],[f31338,f1]) ).
fof(f31531,plain,
( negate(add(sF1,negate(add(f,add(f,negate(h)))))) = negate(add(f,add(f,negate(add(add(f,add(f,negate(h))),negate(add(sF1,negate(add(f,add(f,negate(h)))))))))))
| ~ spl3_159 ),
inference(forward_demodulation,[],[f31472,f2]) ).
fof(f31577,plain,
( negate(add(sF1,negate(add(f,add(f,negate(h)))))) = negate(add(f,add(f,negate(add(f,add(add(f,negate(h)),negate(add(sF1,negate(add(f,add(f,negate(h))))))))))))
| ~ spl3_159 ),
inference(forward_demodulation,[],[f31531,f2]) ).
fof(f31612,plain,
( negate(add(sF1,negate(add(f,add(f,negate(h)))))) = negate(add(f,add(f,negate(add(f,add(f,add(negate(h),negate(add(sF1,negate(add(f,add(f,negate(h)))))))))))))
| ~ spl3_159 ),
inference(forward_demodulation,[],[f31577,f2]) ).
fof(f31624,plain,
( negate(h) = negate(add(sF1,negate(add(f,add(f,negate(h))))))
| ~ spl3_88
| ~ spl3_159 ),
inference(forward_demodulation,[],[f31612,f3281]) ).
fof(f31647,plain,
( spl3_54
| ~ spl3_88
| ~ spl3_159 ),
inference(avatar_split_clause,[],[f31624,f6418,f3279,f1959]) ).
fof(f31729,plain,
( sF1 = negate(add(negate(add(sF1,add(f,add(f,negate(h))))),negate(h)))
| ~ spl3_54 ),
inference(superposition,[],[f3,f1961]) ).
fof(f31864,plain,
( sF1 = negate(add(negate(h),negate(add(sF1,add(f,add(f,negate(h)))))))
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31729,f1]) ).
fof(f31913,plain,
( sF1 = negate(add(negate(h),negate(add(f,add(add(f,negate(h)),sF1)))))
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31864,f101]) ).
fof(f31942,plain,
( sF1 = negate(add(negate(h),negate(add(f,add(sF1,add(f,negate(h)))))))
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31913,f8075]) ).
fof(f31960,plain,
( sF1 = negate(add(negate(h),negate(add(f,add(f,add(sF1,negate(h)))))))
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31942,f539]) ).
fof(f31976,plain,
( sF1 = negate(add(negate(h),negate(add(sF2,add(negate(h),f)))))
| ~ spl3_6
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31960,f2144]) ).
fof(f31992,plain,
( sF1 = negate(add(negate(h),negate(add(f,add(sF2,negate(h))))))
| ~ spl3_6
| ~ spl3_54 ),
inference(forward_demodulation,[],[f31976,f101]) ).
fof(f32013,definition,
( spl3_656
<=> sF1 = negate(add(negate(h),negate(add(f,add(sF2,negate(h)))))) ),
introduced(definition,[new_symbols(definition,[spl3_656])],[avatar_definition]) ).
fof(f32016,plain,
( spl3_656
| ~ spl3_6
| ~ spl3_54 ),
inference(avatar_split_clause,[],[f31992,f1959,f44,f32013]) ).
fof(f32071,plain,
( sF2 != negate(add(negate(h),negate(add(f,add(sF2,negate(h))))))
| sF1 != negate(add(negate(h),negate(add(f,add(sF2,negate(h))))))
| sF1 = sF2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl3_1,
inference(sat_conversion,[],[f22]) ).
cnf(s2,plain,
spl3_2,
inference(sat_conversion,[],[f27]) ).
cnf(s3,plain,
spl3_3,
inference(sat_conversion,[],[f32]) ).
cnf(s4,plain,
spl3_4,
inference(sat_conversion,[],[f37]) ).
cnf(s5,plain,
spl3_5,
inference(sat_conversion,[],[f42]) ).
cnf(s6,plain,
spl3_6,
inference(sat_conversion,[],[f47]) ).
cnf(s10,plain,
( ~ spl3_2
| ~ spl3_3
| spl3_10 ),
inference(sat_conversion,[],[f87]) ).
cnf(s12,plain,
( ~ spl3_3
| ~ spl3_4
| spl3_12 ),
inference(sat_conversion,[],[f145]) ).
cnf(s28,plain,
( ~ spl3_2
| ~ spl3_4
| spl3_29 ),
inference(sat_conversion,[],[f651]) ).
cnf(s42,plain,
( ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_10
| spl3_42 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s48,plain,
( ~ spl3_3
| ~ spl3_4
| spl3_46 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s55,plain,
( ~ spl3_29
| ~ spl3_46
| spl3_52 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s82,plain,
( ~ spl3_2
| ~ spl3_4
| ~ spl3_5
| ~ spl3_6
| ~ spl3_12
| ~ spl3_46
| spl3_75 ),
inference(sat_conversion,[],[f2672]) ).
cnf(s103,plain,
( ~ spl3_3
| ~ spl3_4
| ~ spl3_5
| ~ spl3_29
| ~ spl3_46
| spl3_88 ),
inference(sat_conversion,[],[f3282]) ).
cnf(s192,plain,
( ~ spl3_4
| ~ spl3_5
| ~ spl3_52
| spl3_159 ),
inference(sat_conversion,[],[f6421]) ).
cnf(s268,plain,
( ~ spl3_6
| ~ spl3_42
| spl3_223 ),
inference(sat_conversion,[],[f9320]) ).
cnf(s506,plain,
( ~ spl3_75
| ~ spl3_223
| spl3_402 ),
inference(sat_conversion,[],[f18951]) ).
cnf(s575,plain,
( ~ spl3_402
| spl3_461 ),
inference(sat_conversion,[],[f22544]) ).
cnf(s816,plain,
( spl3_54
| ~ spl3_88
| ~ spl3_159 ),
inference(sat_conversion,[],[f31647]) ).
cnf(s843,plain,
( ~ spl3_6
| ~ spl3_54
| spl3_656 ),
inference(sat_conversion,[],[f32016]) ).
cnf(s853,plain,
( spl3_1
| ~ spl3_461
| ~ spl3_656 ),
inference(sat_conversion,[],[f32071]) ).
cnf(s880,plain,
spl3_46,
inference(rat,[],[s48,s4,s3]) ).
cnf(s884,plain,
spl3_12,
inference(rat,[],[s12,s4,s3]) ).
cnf(s1046,plain,
spl3_75,
inference(rat,[],[s82,s884,s880,s4,s6,s5,s2]) ).
cnf(s1049,plain,
spl3_29,
inference(rat,[],[s28,s4,s2]) ).
cnf(s1051,plain,
spl3_10,
inference(rat,[],[s10,s3,s2]) ).
cnf(s1097,plain,
spl3_52,
inference(rat,[],[s55,s880,s1049]) ).
cnf(s1101,plain,
spl3_88,
inference(rat,[],[s103,s880,s3,s4,s5,s1049]) ).
cnf(s1110,plain,
spl3_42,
inference(rat,[],[s42,s3,s4,s5,s1051]) ).
cnf(s1141,plain,
spl3_159,
inference(rat,[],[s192,s4,s5,s1097]) ).
cnf(s1158,plain,
spl3_54,
inference(rat,[],[s816,s1141,s1101]) ).
cnf(s1208,plain,
spl3_223,
inference(rat,[],[s268,s6,s1110]) ).
cnf(s1286,plain,
spl3_656,
inference(rat,[],[s843,s6,s1158]) ).
cnf(s1309,plain,
spl3_402,
inference(rat,[],[s506,s1046,s1208]) ).
cnf(s1329,plain,
spl3_461,
inference(rat,[],[s575,s1309]) ).
cnf(s1338,plain,
spl3_1,
inference(rat,[],[s853,s1286,s1329]) ).
cnf(s1357,plain,
$false,
inference(rat,[],[s1,s1338]) ).
fof(f32072,plain,
$false,
inference(avatar_sat_refutation,[],[s1357]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ROB017-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.62 % Computer : n002.cluster.edu
% 0.13/0.62 % Model : x86_64 x86_64
% 0.13/0.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.62 % Memory : 8046.5625MB
% 0.13/0.62 % OS : Linux 6.8.0-71-generic
% 0.13/0.62 % CPULimit : 300
% 0.13/0.62 % WCLimit : 300
% 0.13/0.62 % DateTime : Sun Sep 27 23:29:37 UTC 2026
% 0.13/0.62 % CPUTime :
% 0.13/0.62 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.66 Running first-order theorem proving
% 0.17/0.66 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.33/2.70 % (4005366)Input is clausal, will run a generic CNF schedule.
% 11.33/2.70 % (4005371)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=1451224031:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.33/2.70 % (4005374)lrs+10_1_sil=8000:sp=occurrence:random_seed=2307423963:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.33/2.70 % (4005375)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1955879505:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.33/2.70 % (4005377)dis-21_1_sil=8000:lcm=predicate:random_seed=2548800198: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.33/2.70 % (4005376)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1118006250:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.33/2.70 % (4005372)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=385229132:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.33/2.70 % (4005373)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=399839483:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.33/2.70 % (4005377)Refutation not found, incomplete strategy
% 11.33/2.70 % (4005377)------------------------------
% 11.33/2.70 % (4005377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/2.70 % (4005377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/2.70 % (4005377)CaDiCaL version: 2.1.3
% 11.33/2.70 % (4005377)Termination reason: Refutation not found, incomplete strategy
% 11.33/2.70 % (4005377)Time elapsed: 0.001 s
% 11.33/2.70 % (4005377)Peak memory usage: 87 MB
% 11.33/2.70 % (4005374)Instruction limit reached!
% 11.33/2.70 % (4005374)------------------------------
% 11.33/2.70 % (4005374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/2.70 % (4005374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/2.70 % (4005374)CaDiCaL version: 2.1.3
% 11.33/2.70 % (4005374)Termination reason: Instruction limit
% 11.33/2.70 % (4005374)Termination phase: Saturation
% 11.33/2.70 % (4005374)Time elapsed: 0.061 s
% 11.33/2.70 % (4005374)Peak memory usage: 89 MB
% 11.33/2.70 % (4005374)Instructions burned: 109 (million)
% 11.33/2.70 % (4005375)Instruction limit reached!
% 11.33/2.70 % (4005375)------------------------------
% 11.33/2.70 % (4005375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/2.70 % (4005375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/2.70 % (4005375)CaDiCaL version: 2.1.3
% 11.33/2.70 % (4005375)Termination reason: Instruction limit
% 11.33/2.70 % (4005375)Termination phase: Saturation
% 11.33/2.70 % (4005375)Time elapsed: 0.068 s
% 11.33/2.70 % (4005375)Peak memory usage: 89 MB
% 11.33/2.70 % (4005375)Instructions burned: 114 (million)
% 11.33/2.70 % (4005376)Instruction limit reached!
% 11.33/2.70 % (4005376)------------------------------
% 11.33/2.70 % (4005376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/2.70 % (4005376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/2.70 % (4005376)CaDiCaL version: 2.1.3
% 11.33/2.70 % (4005376)Termination reason: Instruction limit
% 11.33/2.70 % (4005376)Termination phase: Saturation
% 11.33/2.70 % (4005376)Time elapsed: 0.093 s
% 11.33/2.70 % (4005376)Peak memory usage: 90 MB
% 11.33/2.70 % (4005376)Instructions burned: 180 (million)
% 11.33/2.70 % (4005386)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=125353145: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)
% 11.33/2.70 % (4005385)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=4005468366:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.33/2.70 % (4005377)------------------------------
% 11.33/2.70 % (4005377)------------------------------
% 11.33/2.70 % (4005387)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=905140704:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.33/2.70 % (4005385)Instruction limit reached!
% 11.33/2.70 % (4005385)------------------------------
% 11.33/2.70 % (4005385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005385)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005385)Termination reason: Instruction limit
% 18.54/3.75 % (4005385)Termination phase: Saturation
% 18.54/3.75 % (4005385)Time elapsed: 0.077 s
% 18.54/3.75 % (4005385)Peak memory usage: 89 MB
% 18.54/3.75 % (4005385)Instructions burned: 144 (million)
% 18.54/3.75 % (4005386)Instruction limit reached!
% 18.54/3.75 % (4005386)------------------------------
% 18.54/3.75 % (4005386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005386)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005386)Termination reason: Instruction limit
% 18.54/3.75 % (4005386)Termination phase: Saturation
% 18.54/3.75 % (4005386)Time elapsed: 0.106 s
% 18.54/3.75 % (4005386)Peak memory usage: 90 MB
% 18.54/3.75 % (4005386)Instructions burned: 189 (million)
% 18.54/3.75 % (4005387)Instruction limit reached!
% 18.54/3.75 % (4005387)------------------------------
% 18.54/3.75 % (4005387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005387)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005387)Termination reason: Instruction limit
% 18.54/3.75 % (4005387)Termination phase: Saturation
% 18.54/3.75 % (4005387)Time elapsed: 0.115 s
% 18.54/3.75 % (4005387)Peak memory usage: 91 MB
% 18.54/3.75 % (4005387)Instructions burned: 221 (million)
% 18.54/3.75 % (4005390)lrs+10_64_to=lpo:sil=8000:random_seed=2612385112:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 18.54/3.75 % (4005392)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2928238349:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.54/3.75 % (4005390)Instruction limit reached!
% 18.54/3.75 % (4005390)------------------------------
% 18.54/3.75 % (4005390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005390)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005390)Termination reason: Instruction limit
% 18.54/3.75 % (4005390)Termination phase: Saturation
% 18.54/3.75 % (4005390)Time elapsed: 0.065 s
% 18.54/3.75 % (4005390)Peak memory usage: 88 MB
% 18.54/3.75 % (4005390)Instructions burned: 127 (million)
% 18.54/3.75 % (4005393)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2212457192:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.54/3.75 % (4005393)Instruction limit reached!
% 18.54/3.75 % (4005393)------------------------------
% 18.54/3.75 % (4005393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005393)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005393)Termination reason: Instruction limit
% 18.54/3.75 % (4005393)Termination phase: Saturation
% 18.54/3.75 % (4005393)Time elapsed: 0.052 s
% 18.54/3.75 % (4005393)Peak memory usage: 90 MB
% 18.54/3.75 % (4005393)Instructions burned: 157 (million)
% 18.54/3.75 % (4005394)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4003879976:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.54/3.75 % (4005392)Instruction limit reached!
% 18.54/3.75 % (4005392)------------------------------
% 18.54/3.75 % (4005392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.54/3.75 % (4005392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.54/3.75 % (4005392)CaDiCaL version: 2.1.3
% 18.54/3.75 % (4005392)Termination reason: Instruction limit
% 18.54/3.75 % (4005392)Termination phase: Saturation
% 18.54/3.75 % (4005392)Time elapsed: 0.105 s
% 18.54/3.75 % (4005392)Peak memory usage: 91 MB
% 18.54/3.75 % (4005392)Instructions burned: 195 (million)
% 18.54/3.75 % (4005398)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=39918924:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.54/3.75 % (4005399)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3407317954:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 18.54/3.75 % (4005399)Instruction limit reached!
% 18.54/3.75 % (4005399)------------------------------
% 18.54/3.75 % (4005399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005399)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005399)Termination reason: Instruction limit
% 27.11/4.95 % (4005399)Termination phase: Saturation
% 27.11/4.95 % (4005399)Time elapsed: 0.034 s
% 27.11/4.95 % (4005399)Peak memory usage: 89 MB
% 27.11/4.95 % (4005399)Instructions burned: 109 (million)
% 27.11/4.95 % (4005398)Instruction limit reached!
% 27.11/4.95 % (4005398)------------------------------
% 27.11/4.95 % (4005398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005398)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005398)Termination reason: Instruction limit
% 27.11/4.95 % (4005398)Termination phase: Saturation
% 27.11/4.95 % (4005398)Time elapsed: 0.060 s
% 27.11/4.95 % (4005398)Peak memory usage: 89 MB
% 27.11/4.95 % (4005398)Instructions burned: 106 (million)
% 27.11/4.95 % (4005401)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2494755848:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 27.11/4.95 % (4005404)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4022192971:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 27.11/4.95 % (4005401)Instruction limit reached!
% 27.11/4.95 % (4005401)------------------------------
% 27.11/4.95 % (4005401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005401)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005401)Termination reason: Instruction limit
% 27.11/4.95 % (4005401)Termination phase: Saturation
% 27.11/4.95 % (4005401)Time elapsed: 0.125 s
% 27.11/4.95 % (4005401)Peak memory usage: 89 MB
% 27.11/4.95 % (4005401)Instructions burned: 244 (million)
% 27.11/4.95 % (4005405)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1186487868:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 27.11/4.95 % (4005405)Instruction limit reached!
% 27.11/4.95 % (4005405)------------------------------
% 27.11/4.95 % (4005405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005405)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005405)Termination reason: Instruction limit
% 27.11/4.95 % (4005405)Termination phase: Saturation
% 27.11/4.95 % (4005405)Time elapsed: 0.068 s
% 27.11/4.95 % (4005405)Peak memory usage: 89 MB
% 27.11/4.95 % (4005405)Instructions burned: 135 (million)
% 27.11/4.95 % (4005409)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3667206830:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 27.11/4.95 % (4005410)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1574646493:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 27.11/4.95 % (4005410)Instruction limit reached!
% 27.11/4.95 % (4005410)------------------------------
% 27.11/4.95 % (4005410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005410)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005410)Termination reason: Instruction limit
% 27.11/4.95 % (4005410)Termination phase: Saturation
% 27.11/4.95 % (4005410)Time elapsed: 0.098 s
% 27.11/4.95 % (4005410)Peak memory usage: 91 MB
% 27.11/4.95 % (4005410)Instructions burned: 192 (million)
% 27.11/4.95 % (4005409)Instruction limit reached!
% 27.11/4.95 % (4005409)------------------------------
% 27.11/4.95 % (4005409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.11/4.95 % (4005409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.11/4.95 % (4005409)CaDiCaL version: 2.1.3
% 27.11/4.95 % (4005409)Termination reason: Instruction limit
% 27.11/4.95 % (4005409)Termination phase: Saturation
% 27.11/4.95 % (4005409)Time elapsed: 0.269 s
% 27.11/4.95 % (4005409)Peak memory usage: 92 MB
% 27.11/4.95 % (4005409)Instructions burned: 500 (million)
% 27.11/4.95 % (4005413)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2641930571:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 27.11/4.95 % (4005414)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1731596925:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 57.71/9.22 % (4005413)Instruction limit reached!
% 57.71/9.22 % (4005413)------------------------------
% 57.71/9.22 % (4005413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005413)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005413)Termination reason: Instruction limit
% 57.71/9.22 % (4005413)Termination phase: Saturation
% 57.71/9.22 % (4005413)Time elapsed: 0.128 s
% 57.71/9.22 % (4005413)Peak memory usage: 89 MB
% 57.71/9.22 % (4005413)Instructions burned: 266 (million)
% 57.71/9.22 % (4005414)Instruction limit reached!
% 57.71/9.22 % (4005414)------------------------------
% 57.71/9.22 % (4005414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005414)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005414)Termination reason: Instruction limit
% 57.71/9.22 % (4005414)Termination phase: Saturation
% 57.71/9.22 % (4005414)Time elapsed: 0.081 s
% 57.71/9.22 % (4005414)Peak memory usage: 88 MB
% 57.71/9.22 % (4005414)Instructions burned: 158 (million)
% 57.71/9.22 % (4005417)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=2979549528:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 57.71/9.22 % (4005418)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2651060933:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 57.71/9.22 % (4005418)Instruction limit reached!
% 57.71/9.22 % (4005418)------------------------------
% 57.71/9.22 % (4005418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005418)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005418)Termination reason: Instruction limit
% 57.71/9.22 % (4005418)Termination phase: Saturation
% 57.71/9.22 % (4005418)Time elapsed: 0.266 s
% 57.71/9.22 % (4005418)Peak memory usage: 91 MB
% 57.71/9.22 % (4005418)Instructions burned: 538 (million)
% 57.71/9.22 % (4005421)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3408940697:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 57.71/9.22 % (4005421)Instruction limit reached!
% 57.71/9.22 % (4005421)------------------------------
% 57.71/9.22 % (4005421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005421)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005421)Termination reason: Instruction limit
% 57.71/9.22 % (4005421)Termination phase: Saturation
% 57.71/9.22 % (4005421)Time elapsed: 0.090 s
% 57.71/9.22 % (4005421)Peak memory usage: 88 MB
% 57.71/9.22 % (4005421)Instructions burned: 181 (million)
% 57.71/9.22 % (4005404)Instruction limit reached!
% 57.71/9.22 % (4005404)------------------------------
% 57.71/9.22 % (4005404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005404)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005404)Termination reason: Instruction limit
% 57.71/9.22 % (4005404)Termination phase: Saturation
% 57.71/9.22 % (4005404)Time elapsed: 1.546 s
% 57.71/9.22 % (4005404)Peak memory usage: 165 MB
% 57.71/9.22 % (4005404)Instructions burned: 5211 (million)
% 57.71/9.22 % (4005423)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=195242421:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 57.71/9.22 % (4005424)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=1448065227:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 57.71/9.22 % (4005394)Instruction limit reached!
% 57.71/9.22 % (4005394)------------------------------
% 57.71/9.22 % (4005394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.71/9.22 % (4005394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.71/9.22 % (4005394)CaDiCaL version: 2.1.3
% 57.71/9.22 % (4005394)Termination reason: Instruction limit
% 70.68/11.11 % (4005394)Termination phase: Saturation
% 70.68/11.11 % (4005394)Time elapsed: 1.944 s
% 70.68/11.11 % (4005394)Peak memory usage: 152 MB
% 70.68/11.11 % (4005394)Instructions burned: 3394 (million)
% 70.68/11.11 % (4005424)Instruction limit reached!
% 70.68/11.11 % (4005424)------------------------------
% 70.68/11.11 % (4005424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/11.11 % (4005424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/11.11 % (4005424)CaDiCaL version: 2.1.3
% 70.68/11.11 % (4005424)Termination reason: Instruction limit
% 70.68/11.11 % (4005424)Termination phase: Saturation
% 70.68/11.11 % (4005424)Time elapsed: 0.122 s
% 70.68/11.11 % (4005424)Peak memory usage: 93 MB
% 70.68/11.11 % (4005424)Instructions burned: 416 (million)
% 70.68/11.11 % (4005427)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=531409088:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 70.68/11.11 % (4005428)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=3857749500:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 70.68/11.11 % (4005428)Refutation not found, incomplete strategy
% 70.68/11.11 % (4005428)------------------------------
% 70.68/11.11 % (4005428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/11.11 % (4005428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/11.11 % (4005428)CaDiCaL version: 2.1.3
% 70.68/11.11 % (4005428)Termination reason: Refutation not found, incomplete strategy
% 70.68/11.11 % (4005428)Time elapsed: 0.001 s
% 70.68/11.11 % (4005428)Peak memory usage: 88 MB
% 70.68/11.11 % (4005428)Instructions burned: 1 (million)
% 70.68/11.11 % (4005428)------------------------------
% 70.68/11.11 % (4005428)------------------------------
% 70.68/11.11 % (4005431)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3497781436:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi)
% 70.68/11.11 % (4005431)Instruction limit reached!
% 70.68/11.11 % (4005431)------------------------------
% 70.68/11.11 % (4005431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/11.11 % (4005431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/11.11 % (4005431)CaDiCaL version: 2.1.3
% 70.68/11.11 % (4005431)Termination reason: Instruction limit
% 70.68/11.11 % (4005431)Termination phase: Saturation
% 70.68/11.11 % (4005431)Time elapsed: 0.206 s
% 70.68/11.11 % (4005431)Peak memory usage: 95 MB
% 70.68/11.11 % (4005431)Instructions burned: 723 (million)
% 70.68/11.11 % (4005433)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3768720162:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 70.68/11.11 % (4005433)Instruction limit reached!
% 70.68/11.11 % (4005433)------------------------------
% 70.68/11.11 % (4005433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/11.11 % (4005433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/11.11 % (4005433)CaDiCaL version: 2.1.3
% 70.68/11.11 % (4005433)Termination reason: Instruction limit
% 70.68/11.11 % (4005433)Termination phase: Saturation
% 70.68/11.11 % (4005433)Time elapsed: 0.189 s
% 70.68/11.11 % (4005433)Peak memory usage: 93 MB
% 70.68/11.11 % (4005433)Instructions burned: 601 (million)
% 70.68/11.11 % (4005417)Instruction limit reached!
% 70.68/11.11 % (4005417)------------------------------
% 70.68/11.11 % (4005417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.68/11.11 % (4005417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.68/11.11 % (4005417)CaDiCaL version: 2.1.3
% 70.68/11.11 % (4005417)Termination reason: Instruction limit
% 70.68/11.11 % (4005417)Termination phase: Saturation
% 70.68/11.11 % (4005417)Time elapsed: 1.919 s
% 70.68/11.11 % (4005417)Peak memory usage: 152 MB
% 70.68/11.11 % (4005417)Instructions burned: 3257 (million)
% 70.68/11.11 % (4005435)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=696774082:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi)
% 70.68/11.11 % (4005436)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=1267042913:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2963 on theBenchmark for (2963ds/1997Mi)
% 94.56/14.42 % (4005435)Instruction limit reached!
% 94.56/14.42 % (4005435)------------------------------
% 94.56/14.42 % (4005435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005435)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005435)Termination reason: Instruction limit
% 94.56/14.42 % (4005435)Termination phase: Saturation
% 94.56/14.42 % (4005435)Time elapsed: 0.926 s
% 94.56/14.42 % (4005435)Peak memory usage: 148 MB
% 94.56/14.42 % (4005435)Instructions burned: 2992 (million)
% 94.56/14.42 % (4005439)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=3433805568:i=2088:bd=preordered:av=off_2952 on theBenchmark for (2952ds/2088Mi)
% 94.56/14.42 % (4005436)Instruction limit reached!
% 94.56/14.42 % (4005436)------------------------------
% 94.56/14.42 % (4005436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005436)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005436)Termination reason: Instruction limit
% 94.56/14.42 % (4005436)Termination phase: Saturation
% 94.56/14.42 % (4005436)Time elapsed: 1.187 s
% 94.56/14.42 % (4005436)Peak memory usage: 139 MB
% 94.56/14.42 % (4005436)Instructions burned: 1998 (million)
% 94.56/14.42 % (4005441)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3959415213:i=1098:nicw=on_2949 on theBenchmark for (2949ds/1098Mi)
% 94.56/14.42 % (4005439)Instruction limit reached!
% 94.56/14.42 % (4005439)------------------------------
% 94.56/14.42 % (4005439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005439)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005439)Termination reason: Instruction limit
% 94.56/14.42 % (4005439)Termination phase: Saturation
% 94.56/14.42 % (4005439)Time elapsed: 0.702 s
% 94.56/14.42 % (4005439)Peak memory usage: 141 MB
% 94.56/14.42 % (4005439)Instructions burned: 2089 (million)
% 94.56/14.42 % (4005443)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=11959807:i=433:bd=preordered_2944 on theBenchmark for (2944ds/433Mi)
% 94.56/14.42 % (4005441)Instruction limit reached!
% 94.56/14.42 % (4005441)------------------------------
% 94.56/14.42 % (4005441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005441)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005441)Termination reason: Instruction limit
% 94.56/14.42 % (4005441)Termination phase: Saturation
% 94.56/14.42 % (4005441)Time elapsed: 0.590 s
% 94.56/14.42 % (4005441)Peak memory usage: 99 MB
% 94.56/14.42 % (4005441)Instructions burned: 1099 (million)
% 94.56/14.42 % (4005443)Instruction limit reached!
% 94.56/14.42 % (4005443)------------------------------
% 94.56/14.42 % (4005443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005443)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005443)Termination reason: Instruction limit
% 94.56/14.42 % (4005443)Termination phase: Saturation
% 94.56/14.42 % (4005443)Time elapsed: 0.133 s
% 94.56/14.42 % (4005443)Peak memory usage: 94 MB
% 94.56/14.42 % (4005443)Instructions burned: 434 (million)
% 94.56/14.42 % (4005446)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=122162763:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2941 on theBenchmark for (2941ds/6922Mi)
% 94.56/14.42 % (4005445)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3624577715:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2941 on theBenchmark for (2941ds/2942Mi)
% 94.56/14.42 % (4005445)Instruction limit reached!
% 94.56/14.42 % (4005445)------------------------------
% 94.56/14.42 % (4005445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.56/14.42 % (4005445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.56/14.42 % (4005445)CaDiCaL version: 2.1.3
% 94.56/14.42 % (4005445)Termination reason: Instruction limit
% 94.56/14.42 % (4005445)Termination phase: Saturation
% 123.24/18.52 % (4005445)Time elapsed: 2.168 s
% 123.24/18.52 % (4005445)Peak memory usage: 145 MB
% 123.24/18.52 % (4005445)Instructions burned: 2943 (million)
% 123.24/18.52 % (4005446)Instruction limit reached!
% 123.24/18.52 % (4005446)------------------------------
% 123.24/18.52 % (4005446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.24/18.52 % (4005446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.24/18.52 % (4005446)CaDiCaL version: 2.1.3
% 123.24/18.52 % (4005446)Termination reason: Instruction limit
% 123.24/18.52 % (4005446)Termination phase: Saturation
% 123.24/18.52 % (4005446)Time elapsed: 2.194 s
% 123.24/18.52 % (4005446)Peak memory usage: 184 MB
% 123.24/18.52 % (4005446)Instructions burned: 6924 (million)
% 123.24/18.52 % (4005450)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=1820620203:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2918 on theBenchmark for (2918ds/4123Mi)
% 123.24/18.52 % (4005449)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=3762910351:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2918 on theBenchmark for (2918ds/596Mi)
% 123.24/18.52 % (4005449)Refutation not found, incomplete strategy
% 123.24/18.52 % (4005449)------------------------------
% 123.24/18.52 % (4005449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.24/18.52 % (4005449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.24/18.52 % (4005449)CaDiCaL version: 2.1.3
% 123.24/18.52 % (4005449)Termination reason: Refutation not found, incomplete strategy
% 123.24/18.52 % (4005449)Time elapsed: 0.002 s
% 123.24/18.52 % (4005449)Peak memory usage: 87 MB
% 123.24/18.52 % (4005449)Instructions burned: 1 (million)
% 123.24/18.52 % (4005449)------------------------------
% 123.24/18.52 % (4005449)------------------------------
% 123.24/18.52 % (4005423)Instruction limit reached!
% 123.24/18.52 % (4005423)------------------------------
% 123.24/18.52 % (4005423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.24/18.52 % (4005423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.24/18.52 % (4005423)CaDiCaL version: 2.1.3
% 123.24/18.52 % (4005423)Termination reason: Instruction limit
% 123.24/18.52 % (4005423)Termination phase: Saturation
% 123.24/18.52 % (4005423)Time elapsed: 6.080 s
% 123.24/18.52 % (4005423)Peak memory usage: 209 MB
% 123.24/18.52 % (4005423)Instructions burned: 10308 (million)
% 123.24/18.52 % (4005453)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2282889466:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2914 on theBenchmark for (2914ds/16411Mi)
% 123.24/18.52 % (4005454)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2391926582:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi)
% 123.24/18.52 % (4005450)Instruction limit reached!
% 123.24/18.52 % (4005450)------------------------------
% 123.24/18.52 % (4005450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.24/18.52 % (4005450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.24/18.52 % (4005450)CaDiCaL version: 2.1.3
% 123.24/18.52 % (4005450)Termination reason: Instruction limit
% 123.24/18.52 % (4005450)Termination phase: Saturation
% 123.24/18.52 % (4005450)Time elapsed: 1.426 s
% 123.24/18.52 % (4005450)Peak memory usage: 162 MB
% 123.24/18.52 % (4005450)Instructions burned: 4126 (million)
% 123.24/18.52 % (4005454)Instruction limit reached!
% 123.24/18.52 % (4005454)------------------------------
% 123.24/18.52 % (4005454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.24/18.52 % (4005454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.24/18.52 % (4005454)CaDiCaL version: 2.1.3
% 123.24/18.52 % (4005454)Termination reason: Instruction limit
% 123.24/18.52 % (4005454)Termination phase: Saturation
% 123.24/18.52 % (4005454)Time elapsed: 1.023 s
% 123.24/18.52 % (4005454)Peak memory usage: 136 MB
% 123.24/18.52 % (4005454)Instructions burned: 1671 (million)
% 123.24/18.52 % (4005457)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=3062594515:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2902 on theBenchmark for (2902ds/1722Mi)
% 123.24/18.52 % (4005458)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=1796592264:cts=off:cond=on:i=9530:bs=on:fsd=on_2901 on theBenchmark for (2901ds/9530Mi)
% 138.18/20.67 % (4005427)Instruction limit reached!
% 138.18/20.67 % (4005427)------------------------------
% 138.18/20.67 % (4005427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.18/20.67 % (4005427)CaDiCaL version: 2.1.3
% 138.18/20.67 % (4005427)Termination reason: Instruction limit
% 138.18/20.67 % (4005427)Termination phase: Saturation
% 138.18/20.67 % (4005427)Time elapsed: 7.232 s
% 138.18/20.67 % (4005427)Peak memory usage: 163 MB
% 138.18/20.67 % (4005427)Instructions burned: 8478 (million)
% 138.18/20.67 % (4005461)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=738567461:st=2:i=4495:sd=10:ss=included_2899 on theBenchmark for (2899ds/4495Mi)
% 138.18/20.67 % (4005457)Instruction limit reached!
% 138.18/20.67 % (4005457)------------------------------
% 138.18/20.67 % (4005457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.18/20.67 % (4005457)CaDiCaL version: 2.1.3
% 138.18/20.67 % (4005457)Termination reason: Instruction limit
% 138.18/20.67 % (4005457)Termination phase: Saturation
% 138.18/20.67 % (4005457)Time elapsed: 0.599 s
% 138.18/20.67 % (4005457)Peak memory usage: 137 MB
% 138.18/20.67 % (4005457)Instructions burned: 1723 (million)
% 138.18/20.67 % (4005463)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=1666174281:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 138.18/20.67 % (4005463)Instruction limit reached!
% 138.18/20.67 % (4005463)------------------------------
% 138.18/20.67 % (4005463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.18/20.67 % (4005463)CaDiCaL version: 2.1.3
% 138.18/20.67 % (4005463)Termination reason: Instruction limit
% 138.18/20.67 % (4005463)Termination phase: Saturation
% 138.18/20.67 % (4005463)Time elapsed: 1.469 s
% 138.18/20.67 % (4005463)Peak memory usage: 168 MB
% 138.18/20.67 % (4005463)Instructions burned: 4923 (million)
% 138.18/20.67 % (4005465)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=3857767625:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2879 on theBenchmark for (2879ds/2083Mi)
% 138.18/20.67 % (4005461)Instruction limit reached!
% 138.18/20.67 % (4005461)------------------------------
% 138.18/20.67 % (4005461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.18/20.67 % (4005461)CaDiCaL version: 2.1.3
% 138.18/20.67 % (4005461)Termination reason: Instruction limit
% 138.18/20.67 % (4005461)Termination phase: Saturation
% 138.18/20.67 % (4005461)Time elapsed: 2.509 s
% 138.18/20.67 % (4005461)Peak memory usage: 163 MB
% 138.18/20.67 % (4005461)Instructions burned: 4496 (million)
% 138.18/20.67 % (4005465)Instruction limit reached!
% 138.18/20.67 % (4005465)------------------------------
% 138.18/20.67 % (4005465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.18/20.67 % (4005465)CaDiCaL version: 2.1.3
% 138.18/20.67 % (4005465)Termination reason: Instruction limit
% 138.18/20.67 % (4005465)Termination phase: Saturation
% 138.18/20.67 % (4005465)Time elapsed: 0.689 s
% 138.18/20.67 % (4005465)Peak memory usage: 139 MB
% 138.18/20.67 % (4005465)Instructions burned: 2086 (million)
% 138.18/20.67 % (4005469)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=1854601183:i=4629:av=off:gsp=on_2872 on theBenchmark for (2872ds/4629Mi)
% 138.18/20.67 % (4005487)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2267116822:i=1258:av=off_2871 on theBenchmark for (2871ds/1258Mi)
% 138.18/20.67 % (4005487)Instruction limit reached!
% 138.18/20.67 % (4005487)------------------------------
% 138.18/20.67 % (4005487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.18/20.67 % (4005487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005487)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005487)Termination reason: Instruction limit
% 164.42/24.39 % (4005487)Termination phase: Saturation
% 164.42/24.39 % (4005487)Time elapsed: 0.307 s
% 164.42/24.39 % (4005487)Peak memory usage: 94 MB
% 164.42/24.39 % (4005487)Instructions burned: 1261 (million)
% 164.42/24.39 % (4005517)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4277236122:i=7343:av=off:ss=included_2866 on theBenchmark for (2866ds/7343Mi)
% 164.42/24.39 % (4005458)Instruction limit reached!
% 164.42/24.39 % (4005458)------------------------------
% 164.42/24.39 % (4005458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.42/24.39 % (4005458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005458)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005458)Termination reason: Instruction limit
% 164.42/24.39 % (4005458)Termination phase: Saturation
% 164.42/24.39 % (4005458)Time elapsed: 5.373 s
% 164.42/24.39 % (4005458)Peak memory usage: 193 MB
% 164.42/24.39 % (4005458)Instructions burned: 9531 (million)
% 164.42/24.39 % (4005519)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4258355694:i=1325:sd=2:ss=axioms:sgt=16_2846 on theBenchmark for (2846ds/1325Mi)
% 164.42/24.39 % (4005469)Instruction limit reached!
% 164.42/24.39 % (4005469)------------------------------
% 164.42/24.39 % (4005469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.42/24.39 % (4005469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005469)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005469)Termination reason: Instruction limit
% 164.42/24.39 % (4005469)Termination phase: Saturation
% 164.42/24.39 % (4005469)Time elapsed: 2.789 s
% 164.42/24.39 % (4005469)Peak memory usage: 159 MB
% 164.42/24.39 % (4005469)Instructions burned: 4631 (million)
% 164.42/24.39 % (4005521)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=4173089477:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2842 on theBenchmark for (2842ds/2646Mi)
% 164.42/24.39 % (4005519)Instruction limit reached!
% 164.42/24.39 % (4005519)------------------------------
% 164.42/24.39 % (4005519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.42/24.39 % (4005519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005519)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005519)Termination reason: Instruction limit
% 164.42/24.39 % (4005519)Termination phase: Saturation
% 164.42/24.39 % (4005519)Time elapsed: 0.673 s
% 164.42/24.39 % (4005519)Peak memory usage: 100 MB
% 164.42/24.39 % (4005519)Instructions burned: 1327 (million)
% 164.42/24.39 % (4005523)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3745788447:i=1489:sd=2:ep=R:ss=axioms_2837 on theBenchmark for (2837ds/1489Mi)
% 164.42/24.39 % (4005523)Refutation not found, incomplete strategy
% 164.42/24.39 % (4005523)------------------------------
% 164.42/24.39 % (4005523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.42/24.39 % (4005523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005523)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005523)Termination reason: Refutation not found, incomplete strategy
% 164.42/24.39 % (4005523)Time elapsed: 0.571 s
% 164.42/24.39 % (4005523)Peak memory usage: 127 MB
% 164.42/24.39 % (4005523)Instructions burned: 857 (million)
% 164.42/24.39 % (4005517)Instruction limit reached!
% 164.42/24.39 % (4005517)------------------------------
% 164.42/24.39 % (4005517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.42/24.39 % (4005517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.42/24.39 % (4005517)CaDiCaL version: 2.1.3
% 164.42/24.39 % (4005517)Termination reason: Instruction limit
% 164.42/24.39 % (4005517)Termination phase: Saturation
% 164.42/24.39 % (4005517)Time elapsed: 3.723 s
% 164.42/24.39 % (4005517)Peak memory usage: 188 MB
% 164.42/24.39 % (4005517)Instructions burned: 7344 (million)
% 164.42/24.39 % (4005523)------------------------------
% 164.42/24.39 % (4005523)------------------------------
% 164.42/24.39 % (4005525)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=2352988538:i=1503_2828 on theBenchmark for (2828ds/1503Mi)
% 164.42/24.39 % (4005526)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2907834367:i=13942:kws=frequency_2827 on theBenchmark for (2827ds/13942Mi)
% 164.42/24.39 % (4005521)Instruction limit reached!
% 194.49/28.54 % (4005521)------------------------------
% 194.49/28.54 % (4005521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.49/28.54 % (4005521)CaDiCaL version: 2.1.3
% 194.49/28.54 % (4005521)Termination reason: Instruction limit
% 194.49/28.54 % (4005521)Termination phase: Saturation
% 194.49/28.54 % (4005521)Time elapsed: 1.532 s
% 194.49/28.54 % (4005521)Peak memory usage: 146 MB
% 194.49/28.54 % (4005521)Instructions burned: 2648 (million)
% 194.49/28.54 % (4005529)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=3688872275:i=3604:fsr=off:er=filter_2825 on theBenchmark for (2825ds/3604Mi)
% 194.49/28.54 % (4005453)Instruction limit reached!
% 194.49/28.54 % (4005453)------------------------------
% 194.49/28.54 % (4005453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.49/28.54 % (4005453)CaDiCaL version: 2.1.3
% 194.49/28.54 % (4005453)Termination reason: Instruction limit
% 194.49/28.54 % (4005453)Termination phase: Saturation
% 194.49/28.54 % (4005453)Time elapsed: 9.344 s
% 194.49/28.54 % (4005453)Peak memory usage: 285 MB
% 194.49/28.54 % (4005453)Instructions burned: 16411 (million)
% 194.49/28.54 % (4005531)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1585404956:i=1876:sd=1:ss=included:sgt=32_2819 on theBenchmark for (2819ds/1876Mi)
% 194.49/28.54 % (4005525)Instruction limit reached!
% 194.49/28.54 % (4005525)------------------------------
% 194.49/28.54 % (4005525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.49/28.54 % (4005525)CaDiCaL version: 2.1.3
% 194.49/28.54 % (4005525)Termination reason: Instruction limit
% 194.49/28.54 % (4005525)Termination phase: Saturation
% 194.49/28.54 % (4005525)Time elapsed: 0.946 s
% 194.49/28.54 % (4005525)Peak memory usage: 134 MB
% 194.49/28.54 % (4005525)Instructions burned: 1504 (million)
% 194.49/28.54 % (4005533)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2934404434:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2817 on theBenchmark for (2817ds/1932Mi)
% 194.49/28.54 % (4005533)Refutation not found, incomplete strategy
% 194.49/28.54 % (4005533)------------------------------
% 194.49/28.54 % (4005533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.49/28.54 % (4005533)CaDiCaL version: 2.1.3
% 194.49/28.54 % (4005533)Termination reason: Refutation not found, incomplete strategy
% 194.49/28.54 % (4005533)Time elapsed: 0.571 s
% 194.49/28.54 % (4005533)Peak memory usage: 127 MB
% 194.49/28.54 % (4005533)Instructions burned: 859 (million)
% 194.49/28.54 % (4005533)------------------------------
% 194.49/28.54 % (4005533)------------------------------
% 194.49/28.54 % (4005531)Instruction limit reached!
% 194.49/28.54 % (4005531)------------------------------
% 194.49/28.54 % (4005531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.49/28.54 % (4005531)CaDiCaL version: 2.1.3
% 194.49/28.54 % (4005531)Termination reason: Instruction limit
% 194.49/28.54 % (4005531)Termination phase: Saturation
% 194.49/28.54 % (4005531)Time elapsed: 1.136 s
% 194.49/28.54 % (4005531)Peak memory usage: 138 MB
% 194.49/28.54 % (4005531)Instructions burned: 1877 (million)
% 194.49/28.54 % (4005535)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=1557559859:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2807 on theBenchmark for (2807ds/1980Mi)
% 194.49/28.54 % (4005536)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=3715908608:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2806 on theBenchmark for (2806ds/3902Mi)
% 194.49/28.54 % (4005529)Instruction limit reached!
% 194.49/28.54 % (4005529)------------------------------
% 194.49/28.54 % (4005529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.49/28.54 % (4005529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005529)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005529)Termination reason: Instruction limit
% 220.65/32.28 % (4005529)Termination phase: Saturation
% 220.65/32.28 % (4005529)Time elapsed: 1.965 s
% 220.65/32.28 % (4005529)Peak memory usage: 143 MB
% 220.65/32.28 % (4005529)Instructions burned: 3605 (million)
% 220.65/32.28 % (4005539)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1034419618:avsq=on:i=3916:aac=none:amm=off_2804 on theBenchmark for (2804ds/3916Mi)
% 220.65/32.28 % (4005535)Instruction limit reached!
% 220.65/32.28 % (4005535)------------------------------
% 220.65/32.28 % (4005535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 220.65/32.28 % (4005535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005535)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005535)Termination reason: Instruction limit
% 220.65/32.28 % (4005535)Termination phase: Saturation
% 220.65/32.28 % (4005535)Time elapsed: 1.199 s
% 220.65/32.28 % (4005535)Peak memory usage: 138 MB
% 220.65/32.28 % (4005535)Instructions burned: 1980 (million)
% 220.65/32.28 % (4005541)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=560148453:cond=on:i=3940:av=off:er=known_2793 on theBenchmark for (2793ds/3940Mi)
% 220.65/32.28 % (4005539)Instruction limit reached!
% 220.65/32.28 % (4005539)------------------------------
% 220.65/32.28 % (4005539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 220.65/32.28 % (4005539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005539)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005539)Termination reason: Instruction limit
% 220.65/32.28 % (4005539)Termination phase: Saturation
% 220.65/32.28 % (4005539)Time elapsed: 1.906 s
% 220.65/32.28 % (4005539)Peak memory usage: 112 MB
% 220.65/32.28 % (4005539)Instructions burned: 3918 (million)
% 220.65/32.28 % (4005536)Instruction limit reached!
% 220.65/32.28 % (4005536)------------------------------
% 220.65/32.28 % (4005536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 220.65/32.28 % (4005536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005536)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005536)Termination reason: Instruction limit
% 220.65/32.28 % (4005536)Termination phase: Saturation
% 220.65/32.28 % (4005536)Time elapsed: 2.163 s
% 220.65/32.28 % (4005536)Peak memory usage: 154 MB
% 220.65/32.28 % (4005536)Instructions burned: 3902 (million)
% 220.65/32.28 % (4005543)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2456568117:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2783 on theBenchmark for (2783ds/3980Mi)
% 220.65/32.28 % (4005544)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=4226725766:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2783 on theBenchmark for (2783ds/2087Mi)
% 220.65/32.28 % (4005541)Instruction limit reached!
% 220.65/32.28 % (4005541)------------------------------
% 220.65/32.28 % (4005541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 220.65/32.28 % (4005541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005541)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005541)Termination reason: Instruction limit
% 220.65/32.28 % (4005541)Termination phase: Saturation
% 220.65/32.28 % (4005541)Time elapsed: 2.148 s
% 220.65/32.28 % (4005541)Peak memory usage: 156 MB
% 220.65/32.28 % (4005541)Instructions burned: 3941 (million)
% 220.65/32.28 % (4005544)Instruction limit reached!
% 220.65/32.28 % (4005544)------------------------------
% 220.65/32.28 % (4005544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 220.65/32.28 % (4005544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.65/32.28 % (4005544)CaDiCaL version: 2.1.3
% 220.65/32.28 % (4005544)Termination reason: Instruction limit
% 220.65/32.28 % (4005544)Termination phase: Saturation
% 220.65/32.28 % (4005544)Time elapsed: 1.271 s
% 220.65/32.28 % (4005544)Peak memory usage: 141 MB
% 220.65/32.28 % (4005544)Instructions burned: 2088 (million)
% 220.65/32.28 % (4005623)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=1699875039:cts=off:cond=on:i=4272:bs=on:fsd=on_2770 on theBenchmark for (2770ds/4272Mi)
% 220.65/32.28 % (4005624)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3356057643:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2768 on theBenchmark for (2768ds/2197Mi)
% 134.53/40.79 % (4005543)Instruction limit reached!
% 134.53/40.79 % (4005543)------------------------------
% 134.53/40.79 % (4005543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005543)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005543)Termination reason: Instruction limit
% 134.53/40.79 % (4005543)Termination phase: Saturation
% 134.53/40.79 % (4005543)Time elapsed: 2.281 s
% 134.53/40.79 % (4005543)Peak memory usage: 161 MB
% 134.53/40.79 % (4005543)Instructions burned: 3981 (million)
% 134.53/40.79 % (4005793)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2746691870:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2758 on theBenchmark for (2758ds/6508Mi)
% 134.53/40.79 % (4005624)Instruction limit reached!
% 134.53/40.79 % (4005624)------------------------------
% 134.53/40.79 % (4005624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005624)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005624)Termination reason: Instruction limit
% 134.53/40.79 % (4005624)Termination phase: Saturation
% 134.53/40.79 % (4005624)Time elapsed: 1.350 s
% 134.53/40.79 % (4005624)Peak memory usage: 140 MB
% 134.53/40.79 % (4005624)Instructions burned: 2199 (million)
% 134.53/40.79 % (4005797)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3160910674:i=2330:fgj=on:av=off:fsr=off_2753 on theBenchmark for (2753ds/2330Mi)
% 134.53/40.79 % (4005526)Instruction limit reached!
% 134.53/40.79 % (4005526)------------------------------
% 134.53/40.79 % (4005526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005526)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005526)Termination reason: Instruction limit
% 134.53/40.79 % (4005526)Termination phase: Saturation
% 134.53/40.79 % (4005526)Time elapsed: 7.670 s
% 134.53/40.79 % (4005526)Peak memory usage: 256 MB
% 134.53/40.79 % (4005526)Instructions burned: 13944 (million)
% 134.53/40.79 % (4005799)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=930457734:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2748 on theBenchmark for (2748ds/7592Mi)
% 134.53/40.79 % (4005623)Instruction limit reached!
% 134.53/40.79 % (4005623)------------------------------
% 134.53/40.79 % (4005623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005623)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005623)Termination reason: Instruction limit
% 134.53/40.79 % (4005623)Termination phase: Saturation
% 134.53/40.79 % (4005623)Time elapsed: 2.529 s
% 134.53/40.79 % (4005623)Peak memory usage: 156 MB
% 134.53/40.79 % (4005623)Instructions burned: 4273 (million)
% 134.53/40.79 % (4005801)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=2506516900:i=2693:kws=precedence:ins=1:av=off_2743 on theBenchmark for (2743ds/2693Mi)
% 134.53/40.79 % (4005797)Instruction limit reached!
% 134.53/40.79 % (4005797)------------------------------
% 134.53/40.79 % (4005797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005797)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005797)Termination reason: Instruction limit
% 134.53/40.79 % (4005797)Termination phase: Saturation
% 134.53/40.79 % (4005797)Time elapsed: 1.347 s
% 134.53/40.79 % (4005797)Peak memory usage: 141 MB
% 134.53/40.79 % (4005797)Instructions burned: 2331 (million)
% 134.53/40.79 % (4005803)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=544803056:i=28651:sd=4:ss=included:sgt=64_2738 on theBenchmark for (2738ds/28651Mi)
% 134.53/40.79 % (4005801)Instruction limit reached!
% 134.53/40.79 % (4005801)------------------------------
% 134.53/40.79 % (4005801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005801)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005801)Termination reason: Instruction limit
% 134.53/40.79 % (4005801)Termination phase: Saturation
% 134.53/40.79 % (4005801)Time elapsed: 1.591 s
% 134.53/40.79 % (4005801)Peak memory usage: 148 MB
% 134.53/40.79 % (4005801)Instructions burned: 2694 (million)
% 134.53/40.79 % (4005871)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2864079077:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2725 on theBenchmark for (2725ds/2700Mi)
% 134.53/40.79 % (4005793)Instruction limit reached!
% 134.53/40.79 % (4005793)------------------------------
% 134.53/40.79 % (4005793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005793)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005793)Termination reason: Instruction limit
% 134.53/40.79 % (4005793)Termination phase: Saturation
% 134.53/40.79 % (4005793)Time elapsed: 3.357 s
% 134.53/40.79 % (4005793)Peak memory usage: 170 MB
% 134.53/40.79 % (4005793)Instructions burned: 6508 (million)
% 134.53/40.79 % (4005920)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3482434342:i=3196:nm=4_2723 on theBenchmark for (2723ds/3196Mi)
% 134.53/40.79 % (4005799)Instruction limit reached!
% 134.53/40.79 % (4005799)------------------------------
% 134.53/40.79 % (4005799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005799)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005799)Termination reason: Instruction limit
% 134.53/40.79 % (4005799)Termination phase: Saturation
% 134.53/40.79 % (4005799)Time elapsed: 3.705 s
% 134.53/40.79 % (4005799)Peak memory usage: 161 MB
% 134.53/40.79 % (4005799)Instructions burned: 7594 (million)
% 134.53/40.79 % (4005922)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3037475524:cts=off:i=3254:av=off_2710 on theBenchmark for (2710ds/3254Mi)
% 134.53/40.79 % (4005871)Instruction limit reached!
% 134.53/40.79 % (4005871)------------------------------
% 134.53/40.79 % (4005871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005871)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005871)Termination reason: Instruction limit
% 134.53/40.79 % (4005871)Termination phase: Saturation
% 134.53/40.79 % (4005871)Time elapsed: 1.593 s
% 134.53/40.79 % (4005871)Peak memory usage: 148 MB
% 134.53/40.79 % (4005871)Instructions burned: 2701 (million)
% 134.53/40.79 % (4005924)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=583009008:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2708 on theBenchmark for (2708ds/3264Mi)
% 134.53/40.79 % (4005920)Instruction limit reached!
% 134.53/40.79 % (4005920)------------------------------
% 134.53/40.79 % (4005920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005920)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005920)Termination reason: Instruction limit
% 134.53/40.79 % (4005920)Termination phase: Saturation
% 134.53/40.79 % (4005920)Time elapsed: 1.896 s
% 134.53/40.79 % (4005920)Peak memory usage: 149 MB
% 134.53/40.79 % (4005920)Instructions burned: 3197 (million)
% 134.53/40.79 % (4005926)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=1196397079:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2702 on theBenchmark for (2702ds/9708Mi)
% 134.53/40.79 % (4005922)Instruction limit reached!
% 134.53/40.79 % (4005922)------------------------------
% 134.53/40.79 % (4005922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005922)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005922)Termination reason: Instruction limit
% 134.53/40.79 % (4005922)Termination phase: Saturation
% 134.53/40.79 % (4005922)Time elapsed: 1.853 s
% 134.53/40.79 % (4005922)Peak memory usage: 150 MB
% 134.53/40.79 % (4005922)Instructions burned: 3255 (million)
% 134.53/40.79 % (4005928)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=332746620:i=21997:s2at=5:gtg=all_2690 on theBenchmark for (2690ds/21997Mi)
% 134.53/40.79 % (4005924)Instruction limit reached!
% 134.53/40.79 % (4005924)------------------------------
% 134.53/40.79 % (4005924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005924)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005924)Termination reason: Instruction limit
% 134.53/40.79 % (4005924)Termination phase: Saturation
% 134.53/40.79 % (4005924)Time elapsed: 1.823 s
% 134.53/40.79 % (4005924)Peak memory usage: 151 MB
% 134.53/40.79 % (4005924)Instructions burned: 3265 (million)
% 134.53/40.79 % (4005930)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1614364453:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2688 on theBenchmark for (2688ds/7551Mi)
% 134.53/40.79 % (4005926)Instruction limit reached!
% 134.53/40.79 % (4005926)------------------------------
% 134.53/40.79 % (4005926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005926)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005926)Termination reason: Instruction limit
% 134.53/40.79 % (4005926)Termination phase: Saturation
% 134.53/40.79 % (4005926)Time elapsed: 5.356 s
% 134.53/40.79 % (4005926)Peak memory usage: 208 MB
% 134.53/40.79 % (4005926)Instructions burned: 9709 (million)
% 134.53/40.79 % (4005932)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4269413914:i=8924:sd=1:ss=included_2647 on theBenchmark for (2647ds/8924Mi)
% 134.53/40.79 % (4005930)Instruction limit reached!
% 134.53/40.79 % (4005930)------------------------------
% 134.53/40.79 % (4005930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.53/40.79 % (4005930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.53/40.79 % (4005930)CaDiCaL version: 2.1.3
% 134.53/40.79 % (4005930)Termination reason: Instruction limit
% 134.53/40.79 % (4005930)Termination phase: Saturation
% 134.53/40.79 % (4005930)Time elapsed: 4.262 s
% 134.53/40.79 % (4005930)Peak memory usage: 162 MB
% 134.53/40.79 % (4005930)Instructions burned: 7552 (million)
% 134.53/40.79 % (4005934)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=3710574458:i=9638:kws=frequency:bd=preordered_2643 on theBenchmark for (2643ds/9638Mi)
% 134.53/40.79 % (4005932)First to succeed.
% 134.53/40.79 % (4005932)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4005366"
% 134.53/40.79 % (4005932)Refutation found. Thanks to Tanya!
% 134.53/40.79 % SZS status Unsatisfiable for theBenchmark
% 134.53/40.79 % SZS output start Proof for theBenchmark
% See solution above
% 281.29/40.99 % (4005932)------------------------------
% 281.29/40.99 % (4005932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 281.29/40.99 % (4005932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 281.29/40.99 % (4005932)CaDiCaL version: 2.1.3
% 281.29/40.99 % (4005932)Termination reason: Refutation
% 281.29/40.99 % (4005932)Time elapsed: 3.842 s
% 281.29/40.99 % (4005932)Peak memory usage: 194 MB
% 281.29/40.99 % (4005932)Instructions burned: 6878 (million)
% 281.29/40.99 % (4005932)------------------------------
% 281.29/40.99 % (4005932)------------------------------
% 281.29/40.99 % (4005366)Success in time 39.688 s
% 281.29/40.99 % Vampire exiting
%------------------------------------------------------------------------------