%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO070-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:51:26 AM UTC 2026
% Result : Unsatisfiable 67.90s 18.43s
% Output : Refutation 124.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 25
% Syntax : Number of formulae : 243 ( 46 unt; 7 def)
% Number of atoms : 754 ( 90 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 938 ( 427 ~; 504 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-5 aty)
% Number of variables : 340 ( 0 sgn 340 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : equidistant(X0,X1,X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X0,X1,X4,X5)
| ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction1) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction2) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ between(X2,X3,X5)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X1,X6,X3,X7)
| ~ between(X0,X1,X4)
| ~ equidistant(X0,X1,X2,X3)
| X0 = X1
| equidistant(X4,X6,X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outer_five_segment) ).
fof(f7,axiom,
! [X0,X1] :
( ~ between(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_betweeness) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4] :
( between(X1,inner_pasch(X0,X1,X2,X4,X3),X3)
| ~ between(X3,X4,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch1) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4] :
( between(X4,inner_pasch(X0,X1,X2,X4,X3),X0)
| ~ between(X3,X4,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch2) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| between(X0,X1,X2)
| between(X1,X2,X0)
| between(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',colinearity4) ).
fof(f23,axiom,
equidistant(u,v,w,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_to_v_equals_w_to_x) ).
fof(f24,axiom,
equidistant(v,w,x,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_to_w_equals_x_to_u) ).
fof(f25,axiom,
equidistant(u,w,v,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_to_w_equals_v_to_x) ).
fof(f26,axiom,
between(u,y,w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',y_between_u_and_w) ).
fof(f27,axiom,
between(v,y,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',y_between_v_and_x) ).
fof(f28,axiom,
u != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_not_v) ).
fof(f29,axiom,
x != u,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_not_u) ).
fof(f30,plain,
u != x,
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
colinear(u,v,w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_uvw_not_colinear) ).
fof(f32,plain,
( between(u,v,w)
| between(v,w,u)
| between(w,u,v) ),
inference(resolution,[],[f22,f31]) ).
fof(f34,definition,
( spl0_1
<=> between(w,u,v) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f35,plain,
( ~ between(w,u,v)
| spl0_1 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f36,plain,
( between(w,u,v)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f34]) ).
fof(f38,definition,
( spl0_2
<=> between(v,w,u) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f40,plain,
( between(v,w,u)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f38]) ).
fof(f42,definition,
( spl0_3
<=> between(u,v,w) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f44,plain,
( between(u,v,w)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f42]) ).
fof(f45,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f32,f42,f38,f34]) ).
fof(f46,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f5,f3]) ).
fof(f49,plain,
! [X0,X1] :
( ~ equidistant(u,w,X0,X1)
| equidistant(X0,X1,v,x) ),
inference(resolution,[],[f2,f25]) ).
fof(f51,plain,
! [X0,X1] :
( ~ equidistant(v,w,X0,X1)
| equidistant(X0,X1,x,u) ),
inference(resolution,[],[f2,f24]) ).
fof(f53,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f54,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f4,f46]) ).
fof(f57,plain,
equidistant(v,x,w,u),
inference(resolution,[],[f53,f25]) ).
fof(f58,plain,
equidistant(w,x,v,u),
inference(resolution,[],[f53,f23]) ).
fof(f59,plain,
equidistant(x,u,w,v),
inference(resolution,[],[f53,f24]) ).
fof(f60,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X0,X1),X3),
inference(resolution,[],[f53,f5]) ).
fof(f61,plain,
! [X0,X1] : equidistant(X0,X1,X0,X1),
inference(resolution,[],[f53,f1]) ).
fof(f65,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X0,X1) ),
inference(resolution,[],[f61,f2]) ).
fof(f69,plain,
equidistant(w,u,x,v),
inference(resolution,[],[f57,f53]) ).
fof(f73,plain,
equidistant(w,v,u,x),
inference(resolution,[],[f59,f53]) ).
fof(f80,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ equidistant(X0,X1,X2,extension(X3,X2,X4,X5))
| ~ equidistant(X6,X7,X3,X8)
| ~ equidistant(X0,X7,X2,X8)
| ~ between(X6,X0,X1)
| ~ equidistant(X6,X0,X3,X2)
| X0 = X6
| equidistant(X1,X7,extension(X3,X2,X4,X5),X8) ),
inference(resolution,[],[f6,f4]) ).
fof(f84,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X2,X0,v,w)
| ~ equidistant(X2,X3,v,X4)
| ~ equidistant(X0,X3,w,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X0,X1,w,u)
| X0 = X2
| equidistant(X1,X3,u,X4) )
| ~ spl0_2 ),
inference(resolution,[],[f6,f40]) ).
fof(f91,definition,
( spl0_4
<=> v = y ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f92,plain,
( v != y
| spl0_4 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f93,plain,
( v = y
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f201,plain,
! [X0,X1] : equidistant(extension(X0,X1,v,w),X1,x,u),
inference(resolution,[],[f51,f60]) ).
fof(f203,plain,
! [X2,X3,X0,X1] :
( ~ between(X1,X0,X2)
| ~ between(X0,X3,X2)
| inner_pasch(X1,X0,X2,X3,X0) = X0 ),
inference(resolution,[],[f7,f8]) ).
fof(f204,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X2)
| ~ between(X3,X0,X2)
| inner_pasch(X0,X1,X2,X0,X3) = X0 ),
inference(resolution,[],[f7,f9]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| inner_pasch(X1,X2,X2,X1,X0) = X1 ),
inference(resolution,[],[f204,f54]) ).
fof(f212,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,extension(X2,X0,X3,X4))
| inner_pasch(X2,X0,extension(X2,X0,X3,X4),X1,X0) = X0 ),
inference(resolution,[],[f203,f4]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X0)
| inner_pasch(X2,X0,X0,X1,X0) = X0 ),
inference(resolution,[],[f203,f54]) ).
fof(f227,plain,
! [X2,X3,X0,X1] : inner_pasch(X0,X1,extension(X0,X1,X2,X3),extension(X0,X1,X2,X3),X1) = X1,
inference(resolution,[],[f212,f54]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( between(extension(X1,X0,X2,X3),X0,X1)
| ~ between(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3))
| ~ between(X1,X0,extension(X1,X0,X2,X3)) ),
inference(superposition,[],[f9,f227]) ).
fof(f234,plain,
! [X2,X3,X0,X1] :
( between(extension(X1,X0,X2,X3),X0,X1)
| ~ between(X1,X0,extension(X1,X0,X2,X3)) ),
inference(forward_subsumption_resolution,[],[f232,f54]) ).
fof(f235,plain,
! [X2,X3,X0,X1] : between(extension(X1,X0,X2,X3),X0,X1),
inference(forward_subsumption_resolution,[],[f234,f4]) ).
fof(f236,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| inner_pasch(extension(X2,X0,X3,X4),X0,X2,X1,X0) = X0 ),
inference(resolution,[],[f235,f203]) ).
fof(f243,plain,
equidistant(w,u,v,x),
inference(resolution,[],[f49,f1]) ).
fof(f251,plain,
! [X2,X3,X0,X1,X4,X5] : inner_pasch(extension(extension(X0,X1,X2,X3),X0,X4,X5),X0,extension(X0,X1,X2,X3),X1,X0) = X0,
inference(resolution,[],[f236,f4]) ).
fof(f263,plain,
equidistant(u,x,v,w),
inference(resolution,[],[f73,f53]) ).
fof(f467,plain,
! [X2,X3,X0,X1,X4,X5] :
( between(X1,X0,extension(extension(X0,X1,X2,X3),X0,X4,X5))
| ~ between(X0,X1,extension(X0,X1,X2,X3))
| ~ between(extension(extension(X0,X1,X2,X3),X0,X4,X5),X0,extension(X0,X1,X2,X3)) ),
inference(superposition,[],[f9,f251]) ).
fof(f469,plain,
! [X2,X3,X0,X1,X4,X5] :
( between(X1,X0,extension(extension(X0,X1,X2,X3),X0,X4,X5))
| ~ between(extension(extension(X0,X1,X2,X3),X0,X4,X5),X0,extension(X0,X1,X2,X3)) ),
inference(forward_subsumption_resolution,[],[f467,f4]) ).
fof(f470,plain,
! [X2,X3,X0,X1,X4,X5] : between(X1,X0,extension(extension(X0,X1,X2,X3),X0,X4,X5)),
inference(forward_subsumption_resolution,[],[f469,f235]) ).
fof(f523,definition,
( spl0_11
<=> ! [X0] : equidistant(x,u,X0,X0) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f524,plain,
( ! [X0] : equidistant(x,u,X0,X0)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f559,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ between(X0,X4,extension(X6,X4,X5,extension(X2,X5,X7,X8)))
| ~ equidistant(X4,X1,X5,X3)
| ~ equidistant(X0,X1,X2,X3)
| ~ equidistant(X0,X4,X2,X5)
| X0 = X4
| equidistant(extension(X6,X4,X5,extension(X2,X5,X7,X8)),X1,extension(X2,X5,X7,X8),X3) ),
inference(resolution,[],[f80,f5]) ).
fof(f574,plain,
equidistant(v,x,u,w),
inference(resolution,[],[f243,f53]) ).
fof(f743,plain,
( ! [X2,X0,X1] :
( ~ equidistant(v,X0,v,X1)
| ~ equidistant(w,X0,w,X1)
| ~ between(v,w,X2)
| ~ equidistant(w,X2,w,u)
| v = w
| equidistant(X2,X0,u,X1) )
| ~ spl0_2 ),
inference(resolution,[],[f84,f61]) ).
fof(f750,definition,
( spl0_16
<=> v = w ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f751,plain,
( v != w
| spl0_16 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f752,plain,
( v = w
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f758,definition,
( spl0_18
<=> ! [X2,X0,X1] :
( ~ equidistant(v,X0,v,X1)
| equidistant(X2,X0,u,X1)
| ~ between(v,w,X2)
| ~ equidistant(w,X2,w,u)
| ~ equidistant(w,X0,w,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f759,plain,
( ! [X2,X0,X1] :
( ~ equidistant(w,X2,w,u)
| equidistant(X2,X0,u,X1)
| ~ between(v,w,X2)
| ~ equidistant(v,X0,v,X1)
| ~ equidistant(w,X0,w,X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f760,plain,
( spl0_16
| spl0_18
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f743,f38,f758,f750]) ).
fof(f765,plain,
( v = inner_pasch(v,w,w,v,u)
| ~ spl0_3 ),
inference(resolution,[],[f44,f206]) ).
fof(f785,plain,
( between(w,v,u)
| ~ between(u,v,w)
| ~ between(v,w,w)
| ~ spl0_3 ),
inference(superposition,[],[f8,f765]) ).
fof(f786,plain,
( between(w,v,u)
| ~ between(v,w,w)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f785,f44]) ).
fof(f787,plain,
( between(w,v,u)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f786,f54]) ).
fof(f860,plain,
! [X0,X1] : equidistant(x,u,X0,extension(X1,X0,v,w)),
inference(resolution,[],[f201,f53]) ).
fof(f888,plain,
( u = inner_pasch(u,v,v,u,w)
| ~ spl0_1 ),
inference(resolution,[],[f36,f206]) ).
fof(f923,plain,
( between(v,u,w)
| ~ between(w,u,v)
| ~ between(u,v,v)
| ~ spl0_1 ),
inference(superposition,[],[f8,f888]) ).
fof(f924,plain,
( between(v,u,w)
| ~ between(u,v,v)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f923,f36]) ).
fof(f925,plain,
( between(v,u,w)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f924,f54]) ).
fof(f1070,plain,
( ! [X0,X1] : equidistant(x,u,X0,extension(X1,X0,v,v))
| ~ spl0_16 ),
inference(backward_demodulation,[],[f860,f752]) ).
fof(f1093,plain,
( ! [X0] : equidistant(x,u,X0,X0)
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1070,f46]) ).
fof(f1118,plain,
( spl0_11
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1093,f750,f523]) ).
fof(f1168,plain,
( ! [X0] :
( ~ between(X0,v,u)
| v = inner_pasch(v,w,u,v,X0) )
| ~ spl0_2 ),
inference(resolution,[],[f40,f204]) ).
fof(f1266,plain,
( ! [X0,X1] : v = inner_pasch(v,w,u,v,extension(u,v,X0,X1))
| ~ spl0_2 ),
inference(resolution,[],[f1168,f235]) ).
fof(f1291,plain,
( ! [X0,X1] :
( between(w,v,extension(u,v,X0,X1))
| ~ between(extension(u,v,X0,X1),v,u)
| ~ between(v,w,u) )
| ~ spl0_2 ),
inference(superposition,[],[f8,f1266]) ).
fof(f1292,plain,
( ! [X0,X1] :
( between(w,v,extension(u,v,X0,X1))
| ~ between(extension(u,v,X0,X1),v,u) )
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f1291,f40]) ).
fof(f1293,plain,
( ! [X0,X1] : between(w,v,extension(u,v,X0,X1))
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f1292,f235]) ).
fof(f1294,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(v,X0,X1,X2)
| ~ equidistant(w,X0,X3,X2)
| ~ equidistant(w,v,X3,X1)
| v = w
| equidistant(extension(u,v,X1,extension(X3,X1,X4,X5)),X0,extension(X3,X1,X4,X5),X2) )
| ~ spl0_2 ),
inference(resolution,[],[f1293,f559]) ).
fof(f1303,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(w,v,X3,X1)
| ~ equidistant(w,X0,X3,X2)
| ~ equidistant(v,X0,X1,X2)
| equidistant(extension(u,v,X1,extension(X3,X1,X4,X5)),X0,extension(X3,X1,X4,X5),X2) )
| ~ spl0_2
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f1294,f751]) ).
fof(f1882,plain,
( ! [X2,X3,X0,X1] :
( equidistant(extension(u,v,w,extension(v,w,X2,X3)),X0,extension(v,w,X2,X3),X1)
| ~ equidistant(v,X0,w,X1)
| ~ equidistant(w,X0,v,X1) )
| ~ spl0_2
| spl0_16 ),
inference(resolution,[],[f1303,f1]) ).
fof(f2163,plain,
equidistant(x,v,w,u),
inference(resolution,[],[f65,f69]) ).
fof(f2515,plain,
! [X0] :
( ~ between(y,X0,w)
| y = inner_pasch(u,y,w,X0,y) ),
inference(resolution,[],[f26,f203]) ).
fof(f2516,plain,
! [X0] :
( ~ between(X0,u,w)
| u = inner_pasch(u,y,w,u,X0) ),
inference(resolution,[],[f26,f204]) ).
fof(f2526,plain,
! [X0] :
( ~ between(X0,v,x)
| v = inner_pasch(v,y,x,v,X0) ),
inference(resolution,[],[f27,f204]) ).
fof(f2623,plain,
y = inner_pasch(u,y,w,w,y),
inference(resolution,[],[f2515,f54]) ).
fof(f2626,plain,
( between(w,y,u)
| ~ between(y,w,w)
| ~ between(u,y,w) ),
inference(superposition,[],[f9,f2623]) ).
fof(f2628,plain,
( between(w,y,u)
| ~ between(u,y,w) ),
inference(forward_subsumption_resolution,[],[f2626,f54]) ).
fof(f2629,plain,
between(w,y,u),
inference(forward_subsumption_resolution,[],[f2628,f26]) ).
fof(f2633,plain,
! [X2,X3,X0,X1,X4] :
( ~ equidistant(X2,X0,w,y)
| ~ equidistant(X2,X3,w,X4)
| ~ equidistant(X0,X3,y,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X0,X1,y,u)
| X0 = X2
| equidistant(X1,X3,u,X4) ),
inference(resolution,[],[f2629,f6]) ).
fof(f2639,plain,
! [X0,X1] : w = inner_pasch(extension(u,w,X0,X1),w,u,y,w),
inference(resolution,[],[f2629,f236]) ).
fof(f2884,plain,
! [X0,X1] :
( between(y,w,extension(u,w,X0,X1))
| ~ between(w,y,u)
| ~ between(extension(u,w,X0,X1),w,u) ),
inference(superposition,[],[f9,f2639]) ).
fof(f2886,plain,
! [X0,X1] :
( between(y,w,extension(u,w,X0,X1))
| ~ between(extension(u,w,X0,X1),w,u) ),
inference(forward_subsumption_resolution,[],[f2884,f2629]) ).
fof(f2887,plain,
! [X0,X1] : between(y,w,extension(u,w,X0,X1)),
inference(forward_subsumption_resolution,[],[f2886,f235]) ).
fof(f4840,plain,
( ! [X2,X0,X1] :
( ~ between(v,w,extension(X0,w,w,u))
| equidistant(extension(X0,w,w,u),X1,u,X2)
| ~ equidistant(v,X1,v,X2)
| ~ equidistant(w,X1,w,X2) )
| ~ spl0_18 ),
inference(resolution,[],[f759,f5]) ).
fof(f4845,plain,
( ! [X0,X1] :
( ~ equidistant(w,X0,w,X1)
| ~ equidistant(v,X0,v,X1)
| equidistant(extension(v,w,w,u),X0,u,X1) )
| ~ spl0_18 ),
inference(resolution,[],[f4840,f4]) ).
fof(f4852,plain,
( ! [X0] :
( ~ equidistant(v,X0,v,X0)
| equidistant(extension(v,w,w,u),X0,u,X0) )
| ~ spl0_18 ),
inference(resolution,[],[f4845,f61]) ).
fof(f4861,plain,
( ! [X0] : equidistant(extension(v,w,w,u),X0,u,X0)
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f4852,f61]) ).
fof(f4866,plain,
( u = extension(v,w,w,u)
| ~ spl0_18 ),
inference(resolution,[],[f4861,f3]) ).
fof(f4904,plain,
( ! [X0,X1] :
( equidistant(extension(u,v,w,u),X0,u,X1)
| ~ equidistant(v,X0,w,X1)
| ~ equidistant(w,X0,v,X1) )
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f1882,f4866]) ).
fof(f5168,plain,
( ! [X0] :
( ~ equidistant(w,X0,v,u)
| ~ equidistant(v,X0,w,u)
| extension(u,v,w,u) = X0 )
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f4904,f3]) ).
fof(f5197,plain,
( ~ equidistant(v,x,w,u)
| x = extension(u,v,w,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f5168,f58]) ).
fof(f5201,plain,
( x = extension(u,v,w,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5197,f57]) ).
fof(f5235,plain,
( between(w,v,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f1293,f5201]) ).
fof(f5236,plain,
( between(u,v,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f4,f5201]) ).
fof(f5651,plain,
( v = inner_pasch(v,y,x,v,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f2526,f5236]) ).
fof(f5652,plain,
( v = inner_pasch(v,y,x,v,w)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f2526,f5235]) ).
fof(f5656,plain,
( between(y,v,u)
| ~ between(u,v,x)
| ~ between(v,y,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f8,f5651]) ).
fof(f5657,plain,
( between(y,v,u)
| ~ between(v,y,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5656,f5236]) ).
fof(f5658,plain,
( between(y,v,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5657,f27]) ).
fof(f5662,plain,
( ! [X0] :
( ~ between(v,X0,u)
| v = inner_pasch(y,v,u,X0,v) )
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f5658,f203]) ).
fof(f5722,plain,
( between(y,v,w)
| ~ between(w,v,x)
| ~ between(v,y,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f8,f5652]) ).
fof(f5723,plain,
( between(y,v,w)
| ~ between(v,y,x)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5722,f5235]) ).
fof(f5724,plain,
( between(y,v,w)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5723,f27]) ).
fof(f5832,plain,
( y = inner_pasch(u,y,w,v,y)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f2515,f5724]) ).
fof(f5833,plain,
( between(v,y,u)
| ~ between(y,v,w)
| ~ between(u,y,w)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f9,f5832]) ).
fof(f5835,plain,
( between(v,y,u)
| ~ between(u,y,w)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5833,f5724]) ).
fof(f5836,plain,
( between(v,y,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5835,f26]) ).
fof(f5837,plain,
( v = inner_pasch(y,v,u,y,v)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f5836,f5662]) ).
fof(f5849,plain,
( between(y,v,y)
| ~ between(v,y,u)
| ~ between(y,v,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(superposition,[],[f9,f5837]) ).
fof(f5851,plain,
( between(y,v,y)
| ~ between(y,v,u)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5849,f5836]) ).
fof(f5852,plain,
( between(y,v,y)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5851,f5658]) ).
fof(f5853,plain,
( ! [X0] : y = inner_pasch(X0,y,y,v,y)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f5852,f213]) ).
fof(f5858,plain,
( v = inner_pasch(v,y,y,v,y)
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(resolution,[],[f5852,f206]) ).
fof(f5868,plain,
( v = y
| ~ spl0_2
| spl0_16
| ~ spl0_18 ),
inference(backward_demodulation,[],[f5858,f5853]) ).
fof(f5869,plain,
( $false
| ~ spl0_2
| spl0_4
| spl0_16
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f5868,f92]) ).
fof(f5870,plain,
( ~ spl0_2
| spl0_4
| spl0_16
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f5869]) ).
fof(f7266,plain,
( u = x
| ~ spl0_11 ),
inference(resolution,[],[f524,f3]) ).
fof(f7271,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f7266,f30]) ).
fof(f7272,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f7271]) ).
fof(f7410,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,v,u)
| ~ equidistant(X2,X3,w,X4)
| ~ equidistant(X0,X3,y,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X2,X0,w,y)
| X0 = X2
| equidistant(X1,X3,u,X4) )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2633,f93]) ).
fof(f7481,plain,
( ! [X0,X1] : between(v,w,extension(u,w,X0,X1))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2887,f93]) ).
fof(f7601,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X3,v,X4)
| ~ equidistant(X0,X1,v,u)
| ~ equidistant(X2,X3,w,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X2,X0,w,y)
| X0 = X2
| equidistant(X1,X3,u,X4) )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f7410,f93]) ).
fof(f7661,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,v,u)
| ~ equidistant(X0,X3,v,X4)
| ~ equidistant(X2,X0,w,v)
| ~ equidistant(X2,X3,w,X4)
| ~ between(X2,X0,X1)
| X0 = X2
| equidistant(X1,X3,u,X4) )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f7601,f93]) ).
fof(f8889,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ between(X3,X0,extension(X4,X0,v,u))
| ~ equidistant(X3,X0,w,v)
| ~ equidistant(X3,X1,w,X2)
| ~ equidistant(X0,X1,v,X2)
| X0 = X3
| equidistant(extension(X4,X0,v,u),X1,u,X2) )
| ~ spl0_4 ),
inference(resolution,[],[f7661,f5]) ).
fof(f8989,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,w,v)
| ~ equidistant(X0,X2,w,X3)
| ~ equidistant(X1,X2,v,X3)
| X0 = X1
| equidistant(extension(X0,X1,v,u),X2,u,X3) )
| ~ spl0_4 ),
inference(resolution,[],[f8889,f4]) ).
fof(f8993,plain,
( ! [X0,X1] :
( ~ equidistant(v,w,w,v)
| ~ equidistant(v,X0,w,X1)
| ~ equidistant(w,X0,v,X1)
| v = w
| equidistant(extension(u,w,v,u),X0,u,X1) )
| ~ spl0_4 ),
inference(resolution,[],[f8889,f7481]) ).
fof(f8994,plain,
( ! [X0,X1] :
( ~ equidistant(v,X0,w,X1)
| ~ equidistant(w,X0,v,X1)
| v = w
| equidistant(extension(u,w,v,u),X0,u,X1) )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f8993,f1]) ).
fof(f8995,plain,
( ! [X0,X1] :
( ~ equidistant(w,X0,v,X1)
| ~ equidistant(v,X0,w,X1)
| equidistant(extension(u,w,v,u),X0,u,X1) )
| ~ spl0_4
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f8994,f751]) ).
fof(f9481,plain,
( ~ equidistant(v,x,w,u)
| equidistant(extension(u,w,v,u),x,u,u)
| ~ spl0_4
| spl0_16 ),
inference(resolution,[],[f8995,f58]) ).
fof(f9493,plain,
( equidistant(extension(u,w,v,u),x,u,u)
| ~ spl0_4
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f9481,f57]) ).
fof(f9828,plain,
( ! [X0,X1] :
( ~ equidistant(x,X0,w,X1)
| ~ equidistant(u,X0,v,X1)
| u = x
| equidistant(extension(x,u,v,u),X0,u,X1) )
| ~ spl0_4 ),
inference(resolution,[],[f8989,f59]) ).
fof(f9829,plain,
( ! [X0,X1] :
( ~ equidistant(u,X0,v,X1)
| ~ equidistant(x,X0,w,X1)
| equidistant(extension(x,u,v,u),X0,u,X1) )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f9828,f30]) ).
fof(f9918,plain,
( x = extension(u,w,v,u)
| ~ spl0_4
| spl0_16 ),
inference(resolution,[],[f9493,f3]) ).
fof(f9979,plain,
( ! [X0,X1] : between(w,u,extension(x,u,X0,X1))
| ~ spl0_4
| spl0_16 ),
inference(superposition,[],[f470,f9918]) ).
fof(f11796,plain,
( ~ equidistant(x,v,w,u)
| equidistant(extension(x,u,v,u),v,u,u)
| ~ spl0_4 ),
inference(resolution,[],[f9829,f1]) ).
fof(f11804,plain,
( equidistant(extension(x,u,v,u),v,u,u)
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f11796,f2163]) ).
fof(f11813,plain,
( v = extension(x,u,v,u)
| ~ spl0_4 ),
inference(resolution,[],[f11804,f3]) ).
fof(f11843,plain,
( between(w,u,v)
| ~ spl0_4
| spl0_16 ),
inference(superposition,[],[f9979,f11813]) ).
fof(f11887,plain,
( $false
| spl0_1
| ~ spl0_4
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f11843,f35]) ).
fof(f11888,plain,
( spl0_1
| ~ spl0_4
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f11887]) ).
fof(f11903,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,u,w)
| ~ equidistant(X2,X3,v,X4)
| ~ equidistant(X0,X3,u,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X2,X0,v,u)
| X0 = X2
| equidistant(X1,X3,w,X4) )
| ~ spl0_1 ),
inference(resolution,[],[f925,f6]) ).
fof(f12072,plain,
( u = inner_pasch(u,y,w,u,v)
| ~ spl0_1 ),
inference(resolution,[],[f2516,f925]) ).
fof(f12076,plain,
( between(y,u,v)
| ~ between(v,u,w)
| ~ between(u,y,w)
| ~ spl0_1 ),
inference(superposition,[],[f8,f12072]) ).
fof(f12077,plain,
( between(y,u,v)
| ~ between(u,y,w)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f12076,f925]) ).
fof(f12078,plain,
( between(y,u,v)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f12077,f26]) ).
fof(f12082,plain,
( u = inner_pasch(u,v,v,u,y)
| ~ spl0_1 ),
inference(resolution,[],[f12078,f206]) ).
fof(f12153,plain,
( between(v,u,y)
| ~ between(y,u,v)
| ~ between(u,v,v)
| ~ spl0_1 ),
inference(superposition,[],[f8,f12082]) ).
fof(f12154,plain,
( between(v,u,y)
| ~ between(u,v,v)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f12153,f12078]) ).
fof(f12155,plain,
( between(v,u,y)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f12154,f54]) ).
fof(f12157,plain,
( ! [X0] :
( ~ between(u,X0,y)
| u = inner_pasch(v,u,y,X0,u) )
| ~ spl0_1 ),
inference(resolution,[],[f12155,f203]) ).
fof(f12158,plain,
( ! [X0] :
( ~ between(X0,v,y)
| v = inner_pasch(v,u,y,v,X0) )
| ~ spl0_1 ),
inference(resolution,[],[f12155,f204]) ).
fof(f21202,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X3,v,u)
| ~ equidistant(X3,X1,u,X2)
| ~ between(X0,X3,extension(X4,X3,u,w))
| ~ equidistant(X0,X1,v,X2)
| X0 = X3
| equidistant(extension(X4,X3,u,w),X1,w,X2) )
| ~ spl0_1 ),
inference(resolution,[],[f11903,f5]) ).
fof(f21216,plain,
( ! [X2,X0,X1] :
( ~ equidistant(v,X0,u,X1)
| ~ between(u,v,extension(X2,v,u,w))
| ~ equidistant(u,X0,v,X1)
| u = v
| equidistant(extension(X2,v,u,w),X0,w,X1) )
| ~ spl0_1 ),
inference(resolution,[],[f21202,f1]) ).
fof(f21225,plain,
( ! [X2,X0,X1] :
( ~ between(u,v,extension(X2,v,u,w))
| ~ equidistant(v,X0,u,X1)
| ~ equidistant(u,X0,v,X1)
| equidistant(extension(X2,v,u,w),X0,w,X1) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21216,f28]) ).
fof(f21230,plain,
( ! [X0,X1] :
( equidistant(extension(u,v,u,w),X0,w,X1)
| ~ equidistant(u,X0,v,X1)
| ~ equidistant(v,X0,u,X1) )
| ~ spl0_1 ),
inference(resolution,[],[f21225,f4]) ).
fof(f21237,plain,
( ! [X0] :
( ~ equidistant(v,X0,u,w)
| ~ equidistant(u,X0,v,w)
| extension(u,v,u,w) = X0 )
| ~ spl0_1 ),
inference(resolution,[],[f21230,f3]) ).
fof(f21247,plain,
( ~ equidistant(u,x,v,w)
| x = extension(u,v,u,w)
| ~ spl0_1 ),
inference(resolution,[],[f21237,f574]) ).
fof(f21251,plain,
( x = extension(u,v,u,w)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21247,f263]) ).
fof(f21288,plain,
( between(u,v,x)
| ~ spl0_1 ),
inference(superposition,[],[f4,f21251]) ).
fof(f21333,plain,
( v = inner_pasch(v,y,x,v,u)
| ~ spl0_1 ),
inference(resolution,[],[f21288,f2526]) ).
fof(f21406,plain,
( between(y,v,u)
| ~ between(u,v,x)
| ~ between(v,y,x)
| ~ spl0_1 ),
inference(superposition,[],[f8,f21333]) ).
fof(f21407,plain,
( between(y,v,u)
| ~ between(v,y,x)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21406,f21288]) ).
fof(f21408,plain,
( between(y,v,u)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21407,f27]) ).
fof(f21421,plain,
( v = inner_pasch(v,u,u,v,y)
| ~ spl0_1 ),
inference(resolution,[],[f21408,f206]) ).
fof(f21432,plain,
( between(u,v,y)
| ~ between(y,v,u)
| ~ between(v,u,u)
| ~ spl0_1 ),
inference(superposition,[],[f8,f21421]) ).
fof(f21433,plain,
( between(u,v,y)
| ~ between(v,u,u)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21432,f21408]) ).
fof(f21434,plain,
( between(u,v,y)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21433,f54]) ).
fof(f21437,plain,
( u = inner_pasch(v,u,y,v,u)
| ~ spl0_1 ),
inference(resolution,[],[f21434,f12157]) ).
fof(f21438,plain,
( v = inner_pasch(v,u,y,v,u)
| ~ spl0_1 ),
inference(resolution,[],[f21434,f12158]) ).
fof(f21449,plain,
( u = v
| ~ spl0_1 ),
inference(backward_demodulation,[],[f21438,f21437]) ).
fof(f21450,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f21449,f28]) ).
fof(f21451,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f21450]) ).
fof(f21475,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,v,u)
| ~ equidistant(X2,X3,w,X4)
| ~ equidistant(X0,X3,v,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X2,X0,w,v)
| X0 = X2
| equidistant(X1,X3,u,X4) )
| ~ spl0_3 ),
inference(resolution,[],[f787,f6]) ).
fof(f21490,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,v,w)
| ~ equidistant(X2,X3,u,X4)
| ~ equidistant(X0,X3,v,X4)
| ~ between(X2,X0,X1)
| ~ equidistant(X2,X0,u,v)
| X0 = X2
| equidistant(X1,X3,w,X4) )
| ~ spl0_3 ),
inference(resolution,[],[f44,f6]) ).
fof(f21694,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X3,u,v)
| ~ equidistant(X3,X1,v,X2)
| ~ between(X0,X3,extension(X4,X3,v,w))
| ~ equidistant(X0,X1,u,X2)
| X0 = X3
| equidistant(extension(X4,X3,v,w),X1,w,X2) )
| ~ spl0_3 ),
inference(resolution,[],[f21490,f5]) ).
fof(f21733,plain,
( ! [X2,X0,X1] :
( ~ equidistant(v,X0,v,X1)
| ~ between(u,v,extension(X2,v,v,w))
| ~ equidistant(u,X0,u,X1)
| u = v
| equidistant(extension(X2,v,v,w),X0,w,X1) )
| ~ spl0_3 ),
inference(resolution,[],[f21694,f61]) ).
fof(f21734,plain,
( ! [X2,X0,X1] :
( ~ equidistant(u,X0,v,X1)
| ~ between(v,u,extension(X2,u,v,w))
| ~ equidistant(v,X0,u,X1)
| u = v
| equidistant(extension(X2,u,v,w),X0,w,X1) )
| ~ spl0_3 ),
inference(resolution,[],[f21694,f1]) ).
fof(f21743,plain,
( ! [X2,X0,X1] :
( ~ between(v,u,extension(X2,u,v,w))
| ~ equidistant(u,X0,v,X1)
| ~ equidistant(v,X0,u,X1)
| equidistant(extension(X2,u,v,w),X0,w,X1) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f21734,f28]) ).
fof(f21744,plain,
( ! [X2,X0,X1] :
( ~ between(u,v,extension(X2,v,v,w))
| ~ equidistant(v,X0,v,X1)
| ~ equidistant(u,X0,u,X1)
| equidistant(extension(X2,v,v,w),X0,w,X1) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f21733,f28]) ).
fof(f21746,plain,
( ! [X0,X1] :
( equidistant(extension(v,u,v,w),X0,w,X1)
| ~ equidistant(v,X0,u,X1)
| ~ equidistant(u,X0,v,X1) )
| ~ spl0_3 ),
inference(resolution,[],[f21743,f4]) ).
fof(f21752,plain,
( ! [X0] :
( ~ equidistant(v,X0,u,w)
| ~ equidistant(u,X0,v,w)
| extension(v,u,v,w) = X0 )
| ~ spl0_3 ),
inference(resolution,[],[f21746,f3]) ).
fof(f21762,plain,
( ~ equidistant(u,x,v,w)
| x = extension(v,u,v,w)
| ~ spl0_3 ),
inference(resolution,[],[f21752,f574]) ).
fof(f21766,plain,
( x = extension(v,u,v,w)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f21762,f263]) ).
fof(f22465,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(v,X0,v,X1)
| ~ equidistant(u,X0,u,X1)
| equidistant(extension(extension(v,u,X2,X3),v,v,w),X0,w,X1) )
| ~ spl0_3 ),
inference(resolution,[],[f21744,f470]) ).
fof(f23831,plain,
( ! [X2,X0,X1] :
( ~ equidistant(u,X0,u,X0)
| equidistant(extension(extension(v,u,X1,X2),v,v,w),X0,w,X0) )
| ~ spl0_3 ),
inference(resolution,[],[f22465,f61]) ).
fof(f23841,plain,
( ! [X2,X0,X1] : equidistant(extension(extension(v,u,X1,X2),v,v,w),X0,w,X0)
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f23831,f61]) ).
fof(f23846,plain,
( ! [X0,X1] : w = extension(extension(v,u,X0,X1),v,v,w)
| ~ spl0_3 ),
inference(resolution,[],[f23841,f3]) ).
fof(f23891,plain,
( w = extension(x,v,v,w)
| ~ spl0_3 ),
inference(superposition,[],[f23846,f21766]) ).
fof(f59193,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X3,w,v)
| ~ equidistant(X3,X1,v,X2)
| ~ between(X0,X3,extension(X4,X3,v,u))
| ~ equidistant(X0,X1,w,X2)
| X0 = X3
| equidistant(extension(X4,X3,v,u),X1,u,X2) )
| ~ spl0_3 ),
inference(resolution,[],[f21475,f5]) ).
fof(f59225,plain,
( ! [X2,X0,X1] :
( ~ equidistant(w,X0,v,X1)
| ~ between(v,w,extension(X2,w,v,u))
| ~ equidistant(v,X0,w,X1)
| v = w
| equidistant(extension(X2,w,v,u),X0,u,X1) )
| ~ spl0_3 ),
inference(resolution,[],[f59193,f1]) ).
fof(f59242,plain,
( ! [X2,X0,X1] :
( ~ between(v,w,extension(X2,w,v,u))
| ~ equidistant(w,X0,v,X1)
| ~ equidistant(v,X0,w,X1)
| equidistant(extension(X2,w,v,u),X0,u,X1) )
| ~ spl0_3
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f59225,f751]) ).
fof(f59246,plain,
( ! [X0,X1] :
( ~ equidistant(w,X0,v,X1)
| ~ equidistant(v,X0,w,X1)
| equidistant(extension(v,w,v,u),X0,u,X1) )
| ~ spl0_3
| spl0_16 ),
inference(resolution,[],[f59242,f4]) ).
fof(f59249,plain,
( ~ equidistant(v,x,w,u)
| equidistant(extension(v,w,v,u),x,u,u)
| ~ spl0_3
| spl0_16 ),
inference(resolution,[],[f59246,f58]) ).
fof(f59265,plain,
( equidistant(extension(v,w,v,u),x,u,u)
| ~ spl0_3
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f59249,f57]) ).
fof(f59427,plain,
( x = extension(v,w,v,u)
| ~ spl0_3
| spl0_16 ),
inference(resolution,[],[f59265,f3]) ).
fof(f59513,plain,
( ! [X0,X1] : between(w,v,extension(x,v,X0,X1))
| ~ spl0_3
| spl0_16 ),
inference(superposition,[],[f470,f59427]) ).
fof(f59587,plain,
( between(w,v,w)
| ~ spl0_3
| spl0_16 ),
inference(superposition,[],[f59513,f23891]) ).
fof(f59597,plain,
( ! [X0] : w = inner_pasch(X0,w,w,v,w)
| ~ spl0_3
| spl0_16 ),
inference(resolution,[],[f59587,f213]) ).
fof(f59602,plain,
( v = inner_pasch(v,w,w,v,w)
| ~ spl0_3
| spl0_16 ),
inference(resolution,[],[f59587,f206]) ).
fof(f59612,plain,
( v = w
| ~ spl0_3
| spl0_16 ),
inference(backward_demodulation,[],[f59602,f59597]) ).
fof(f59613,plain,
( $false
| ~ spl0_3
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f59612,f751]) ).
fof(f59614,plain,
( ~ spl0_3
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f59613]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f45]) ).
cnf(s11,plain,
( ~ spl0_2
| spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f760]) ).
cnf(s16,plain,
( spl0_11
| ~ spl0_16 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s63,plain,
( ~ spl0_2
| spl0_4
| spl0_16
| ~ spl0_18 ),
inference(sat_conversion,[],[f5870]) ).
cnf(s76,plain,
~ spl0_11,
inference(sat_conversion,[],[f7272]) ).
cnf(s185,plain,
( spl0_1
| ~ spl0_4
| spl0_16 ),
inference(sat_conversion,[],[f11888]) ).
cnf(s381,plain,
~ spl0_1,
inference(sat_conversion,[],[f21451]) ).
cnf(s545,plain,
( ~ spl0_3
| spl0_16 ),
inference(sat_conversion,[],[f59614]) ).
cnf(s560,plain,
( ~ spl0_4
| spl0_16 ),
inference(rat,[],[s185,s381]) ).
cnf(s568,plain,
~ spl0_16,
inference(rat,[],[s16,s76]) ).
cnf(s569,plain,
~ spl0_3,
inference(rat,[],[s545,s568]) ).
cnf(s570,plain,
~ spl0_4,
inference(rat,[],[s560,s568]) ).
cnf(s572,plain,
( ~ spl0_2
| spl0_18 ),
inference(rat,[],[s11,s568]) ).
cnf(s578,plain,
spl0_2,
inference(rat,[],[s1,s569,s381]) ).
cnf(s579,plain,
~ spl0_18,
inference(rat,[],[s63,s570,s568,s578]) ).
cnf(s583,plain,
$false,
inference(rat,[],[s572,s579,s578]) ).
fof(f59615,plain,
$false,
inference(avatar_sat_refutation,[],[s583]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO070-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 % Computer : n020.cluster.edu
% 0.10/0.42 % Model : x86_64 x86_64
% 0.10/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.42 % Memory : 8046.5625MB
% 0.10/0.42 % OS : Linux 6.8.0-71-generic
% 0.10/0.42 % CPULimit : 300
% 0.10/0.42 % WCLimit : 300
% 0.10/0.42 % DateTime : Sun Sep 27 06:50:04 UTC 2026
% 0.10/0.42 % CPUTime :
% 0.10/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.46 Running first-order theorem proving
% 0.10/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.60/2.57 % (3055210)Input is clausal, will run a generic CNF schedule.
% 11.60/2.57 % (3055216)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2015992367:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.60/2.57 % (3055215)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=399742665:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.60/2.57 % (3055217)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1259378518:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.60/2.57 % (3055218)lrs+10_1_sil=8000:sp=occurrence:random_seed=679407582:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.60/2.57 % (3055219)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1872493299:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.60/2.57 % (3055221)dis-21_1_sil=8000:lcm=predicate:random_seed=1640928500: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.60/2.57 % (3055220)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1574142281:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.60/2.57 % (3055218)Refutation not found, incomplete strategy
% 11.60/2.57 % (3055218)------------------------------
% 11.60/2.57 % (3055218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/2.57 % (3055218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/2.57 % (3055218)CaDiCaL version: 2.1.3
% 11.60/2.57 % (3055218)Termination reason: Refutation not found, incomplete strategy
% 11.60/2.57 % (3055218)Time elapsed: 0.040 s
% 11.60/2.57 % (3055218)Peak memory usage: 88 MB
% 11.60/2.57 % (3055218)Instructions burned: 61 (million)
% 11.60/2.57 % (3055221)Instruction limit reached!
% 11.60/2.57 % (3055221)------------------------------
% 11.60/2.57 % (3055221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/2.57 % (3055221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/2.57 % (3055221)CaDiCaL version: 2.1.3
% 11.60/2.57 % (3055221)Termination reason: Instruction limit
% 11.60/2.57 % (3055221)Termination phase: Saturation
% 11.60/2.57 % (3055221)Time elapsed: 0.063 s
% 11.60/2.57 % (3055221)Peak memory usage: 88 MB
% 11.60/2.57 % (3055221)Instructions burned: 118 (million)
% 11.60/2.57 % (3055219)Instruction limit reached!
% 11.60/2.57 % (3055219)------------------------------
% 11.60/2.57 % (3055219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/2.57 % (3055219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/2.57 % (3055219)CaDiCaL version: 2.1.3
% 11.60/2.57 % (3055219)Termination reason: Instruction limit
% 11.60/2.57 % (3055219)Termination phase: Saturation
% 11.60/2.57 % (3055219)Time elapsed: 0.070 s
% 11.60/2.57 % (3055219)Peak memory usage: 88 MB
% 11.60/2.57 % (3055219)Instructions burned: 114 (million)
% 11.60/2.57 % (3055220)Instruction limit reached!
% 11.60/2.57 % (3055220)------------------------------
% 11.60/2.57 % (3055220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.60/2.57 % (3055220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.60/2.57 % (3055220)CaDiCaL version: 2.1.3
% 11.60/2.57 % (3055220)Termination reason: Instruction limit
% 11.60/2.57 % (3055220)Termination phase: Saturation
% 11.60/2.57 % (3055220)Time elapsed: 0.115 s
% 11.60/2.57 % (3055220)Peak memory usage: 89 MB
% 11.60/2.57 % (3055220)Instructions burned: 180 (million)
% 11.60/2.57 % (3055229)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=429584244:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.60/2.57 % (3055230)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2808266855: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.60/2.57 % (3055231)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3742667179:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.60/2.57 % (3055231)Refutation not found, incomplete strategy
% 11.60/2.57 % (3055231)------------------------------
% 11.60/2.57 % (3055231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055231)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055231)Termination reason: Refutation not found, incomplete strategy
% 24.44/4.34 % (3055231)Time elapsed: 0.001 s
% 24.44/4.34 % (3055231)Peak memory usage: 88 MB
% 24.44/4.34 % (3055231)Instructions burned: 1 (million)
% 24.44/4.34 % (3055218)------------------------------
% 24.44/4.34 % (3055218)------------------------------
% 24.44/4.34 % (3055229)Instruction limit reached!
% 24.44/4.34 % (3055229)------------------------------
% 24.44/4.34 % (3055229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055229)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055229)Termination reason: Instruction limit
% 24.44/4.34 % (3055229)Termination phase: Saturation
% 24.44/4.34 % (3055229)Time elapsed: 0.102 s
% 24.44/4.34 % (3055229)Peak memory usage: 89 MB
% 24.44/4.34 % (3055229)Instructions burned: 144 (million)
% 24.44/4.34 % (3055230)Instruction limit reached!
% 24.44/4.34 % (3055230)------------------------------
% 24.44/4.34 % (3055230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055230)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055230)Termination reason: Instruction limit
% 24.44/4.34 % (3055230)Termination phase: Saturation
% 24.44/4.34 % (3055230)Time elapsed: 0.096 s
% 24.44/4.34 % (3055230)Peak memory usage: 88 MB
% 24.44/4.34 % (3055230)Instructions burned: 189 (million)
% 24.44/4.34 % (3055235)lrs+10_64_to=lpo:sil=8000:random_seed=3348231095:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 24.44/4.34 % (3055237)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1466385642:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 24.44/4.34 % (3055236)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2417140490:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 24.44/4.34 % (3055231)------------------------------
% 24.44/4.34 % (3055231)------------------------------
% 24.44/4.34 % (3055235)Instruction limit reached!
% 24.44/4.34 % (3055235)------------------------------
% 24.44/4.34 % (3055235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055235)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055235)Termination reason: Instruction limit
% 24.44/4.34 % (3055235)Termination phase: Saturation
% 24.44/4.34 % (3055235)Time elapsed: 0.072 s
% 24.44/4.34 % (3055235)Peak memory usage: 88 MB
% 24.44/4.34 % (3055235)Instructions burned: 127 (million)
% 24.44/4.34 % (3055237)Instruction limit reached!
% 24.44/4.34 % (3055237)------------------------------
% 24.44/4.34 % (3055237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055237)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055237)Termination reason: Instruction limit
% 24.44/4.34 % (3055237)Termination phase: Saturation
% 24.44/4.34 % (3055237)Time elapsed: 0.107 s
% 24.44/4.34 % (3055237)Peak memory usage: 90 MB
% 24.44/4.34 % (3055237)Instructions burned: 158 (million)
% 24.44/4.34 % (3055236)Instruction limit reached!
% 24.44/4.34 % (3055236)------------------------------
% 24.44/4.34 % (3055236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.44/4.34 % (3055236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.44/4.34 % (3055236)CaDiCaL version: 2.1.3
% 24.44/4.34 % (3055236)Termination reason: Instruction limit
% 24.44/4.34 % (3055236)Termination phase: Saturation
% 24.44/4.34 % (3055236)Time elapsed: 0.119 s
% 24.44/4.34 % (3055236)Peak memory usage: 89 MB
% 24.44/4.34 % (3055236)Instructions burned: 195 (million)
% 24.44/4.34 % (3055242)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=2721238308:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 24.44/4.34 % (3055241)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2840394345:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 24.44/4.34 % (3055242)Instruction limit reached!
% 24.44/4.34 % (3055242)------------------------------
% 24.44/4.34 % (3055242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055242)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055242)Termination reason: Instruction limit
% 33.18/5.64 % (3055242)Termination phase: Saturation
% 33.18/5.64 % (3055242)Time elapsed: 0.057 s
% 33.18/5.64 % (3055242)Peak memory usage: 88 MB
% 33.18/5.64 % (3055242)Instructions burned: 107 (million)
% 33.18/5.64 % (3055243)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2271201735:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 33.18/5.64 % (3055244)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3810545979:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 33.18/5.64 % (3055243)Instruction limit reached!
% 33.18/5.64 % (3055243)------------------------------
% 33.18/5.64 % (3055243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055243)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055243)Termination reason: Instruction limit
% 33.18/5.64 % (3055243)Termination phase: Saturation
% 33.18/5.64 % (3055243)Time elapsed: 0.072 s
% 33.18/5.64 % (3055243)Peak memory usage: 89 MB
% 33.18/5.64 % (3055243)Instructions burned: 108 (million)
% 33.18/5.64 % (3055247)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1407258703:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 33.18/5.64 % (3055244)Instruction limit reached!
% 33.18/5.64 % (3055244)------------------------------
% 33.18/5.64 % (3055244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055244)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055244)Termination reason: Instruction limit
% 33.18/5.64 % (3055244)Termination phase: Saturation
% 33.18/5.64 % (3055244)Time elapsed: 0.156 s
% 33.18/5.64 % (3055244)Peak memory usage: 90 MB
% 33.18/5.64 % (3055244)Instructions burned: 242 (million)
% 33.18/5.64 % (3055250)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3054180613:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 33.18/5.64 % (3055250)Instruction limit reached!
% 33.18/5.64 % (3055250)------------------------------
% 33.18/5.64 % (3055250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055250)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055250)Termination reason: Instruction limit
% 33.18/5.64 % (3055250)Termination phase: Saturation
% 33.18/5.64 % (3055250)Time elapsed: 0.097 s
% 33.18/5.64 % (3055250)Peak memory usage: 89 MB
% 33.18/5.64 % (3055250)Instructions burned: 136 (million)
% 33.18/5.64 % (3055252)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1362651613:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 33.18/5.64 % (3055255)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1584196620:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 33.18/5.64 % (3055255)Instruction limit reached!
% 33.18/5.64 % (3055255)------------------------------
% 33.18/5.64 % (3055255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055255)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055255)Termination reason: Instruction limit
% 33.18/5.64 % (3055255)Termination phase: Saturation
% 33.18/5.64 % (3055255)Time elapsed: 0.107 s
% 33.18/5.64 % (3055255)Peak memory usage: 89 MB
% 33.18/5.64 % (3055255)Instructions burned: 192 (million)
% 33.18/5.64 % (3055252)Instruction limit reached!
% 33.18/5.64 % (3055252)------------------------------
% 33.18/5.64 % (3055252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.18/5.64 % (3055252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.18/5.64 % (3055252)CaDiCaL version: 2.1.3
% 33.18/5.64 % (3055252)Termination reason: Instruction limit
% 33.18/5.64 % (3055252)Termination phase: Saturation
% 33.18/5.64 % (3055252)Time elapsed: 0.281 s
% 33.18/5.64 % (3055252)Peak memory usage: 92 MB
% 33.18/5.64 % (3055252)Instructions burned: 500 (million)
% 33.18/5.64 % (3055257)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3198610099:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 58.03/9.08 % (3055258)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2415231418:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 58.03/9.08 % (3055258)Instruction limit reached!
% 58.03/9.08 % (3055258)------------------------------
% 58.03/9.08 % (3055258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.03/9.08 % (3055258)CaDiCaL version: 2.1.3
% 58.03/9.08 % (3055258)Termination reason: Instruction limit
% 58.03/9.08 % (3055258)Termination phase: Saturation
% 58.03/9.08 % (3055258)Time elapsed: 0.103 s
% 58.03/9.08 % (3055258)Peak memory usage: 89 MB
% 58.03/9.08 % (3055258)Instructions burned: 157 (million)
% 58.03/9.08 % (3055257)Instruction limit reached!
% 58.03/9.08 % (3055257)------------------------------
% 58.03/9.08 % (3055257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.03/9.08 % (3055257)CaDiCaL version: 2.1.3
% 58.03/9.08 % (3055257)Termination reason: Instruction limit
% 58.03/9.08 % (3055257)Termination phase: Saturation
% 58.03/9.08 % (3055257)Time elapsed: 0.168 s
% 58.03/9.08 % (3055257)Peak memory usage: 90 MB
% 58.03/9.08 % (3055257)Instructions burned: 264 (million)
% 58.03/9.08 % (3055261)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=2599040604:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 58.03/9.08 % (3055262)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=510226204:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 58.03/9.08 % (3055262)Instruction limit reached!
% 58.03/9.08 % (3055262)------------------------------
% 58.03/9.08 % (3055262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.03/9.08 % (3055262)CaDiCaL version: 2.1.3
% 58.03/9.08 % (3055262)Termination reason: Instruction limit
% 58.03/9.08 % (3055262)Termination phase: Saturation
% 58.03/9.08 % (3055262)Time elapsed: 0.230 s
% 58.03/9.08 % (3055262)Peak memory usage: 87 MB
% 58.03/9.08 % (3055262)Instructions burned: 538 (million)
% 58.03/9.08 % (3055265)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=958595084:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 58.03/9.08 % (3055265)Instruction limit reached!
% 58.03/9.08 % (3055265)------------------------------
% 58.03/9.08 % (3055265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.03/9.08 % (3055265)CaDiCaL version: 2.1.3
% 58.03/9.08 % (3055265)Termination reason: Instruction limit
% 58.03/9.08 % (3055265)Termination phase: Saturation
% 58.03/9.08 % (3055265)Time elapsed: 0.102 s
% 58.03/9.08 % (3055265)Peak memory usage: 89 MB
% 58.03/9.08 % (3055265)Instructions burned: 180 (million)
% 58.03/9.08 % (3055267)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=3614508035:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 58.03/9.08 % (3055241)Instruction limit reached!
% 58.03/9.08 % (3055241)------------------------------
% 58.03/9.08 % (3055241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.03/9.08 % (3055241)CaDiCaL version: 2.1.3
% 58.03/9.08 % (3055241)Termination reason: Instruction limit
% 58.03/9.08 % (3055241)Termination phase: Saturation
% 58.03/9.08 % (3055241)Time elapsed: 2.236 s
% 58.03/9.08 % (3055241)Peak memory usage: 147 MB
% 58.03/9.08 % (3055241)Instructions burned: 3395 (million)
% 58.03/9.08 % (3055269)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=14116227:i=412:gtgl=4:gtg=exists_all_2969 on theBenchmark for (2969ds/412Mi)
% 58.03/9.08 % (3055269)Instruction limit reached!
% 58.03/9.08 % (3055269)------------------------------
% 58.03/9.08 % (3055269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.03/9.08 % (3055269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055269)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055269)Termination reason: Instruction limit
% 70.43/10.85 % (3055269)Termination phase: Saturation
% 70.43/10.85 % (3055269)Time elapsed: 0.187 s
% 70.43/10.85 % (3055269)Peak memory usage: 90 MB
% 70.43/10.85 % (3055269)Instructions burned: 414 (million)
% 70.43/10.85 % (3055271)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=3129471818:s2pl=no:i=8478:s2at=4:nm=6_2965 on theBenchmark for (2965ds/8478Mi)
% 70.43/10.85 % (3055261)Instruction limit reached!
% 70.43/10.85 % (3055261)------------------------------
% 70.43/10.85 % (3055261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.85 % (3055261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055261)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055261)Termination reason: Instruction limit
% 70.43/10.85 % (3055261)Termination phase: Saturation
% 70.43/10.85 % (3055261)Time elapsed: 1.829 s
% 70.43/10.85 % (3055261)Peak memory usage: 148 MB
% 70.43/10.85 % (3055261)Instructions burned: 3257 (million)
% 70.43/10.85 % (3055247)Instruction limit reached!
% 70.43/10.85 % (3055247)------------------------------
% 70.43/10.85 % (3055247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.85 % (3055247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055247)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055247)Termination reason: Instruction limit
% 70.43/10.85 % (3055247)Termination phase: Saturation
% 70.43/10.85 % (3055247)Time elapsed: 2.744 s
% 70.43/10.85 % (3055247)Peak memory usage: 143 MB
% 70.43/10.85 % (3055247)Instructions burned: 5209 (million)
% 70.43/10.85 % (3055273)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=3364833983:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi)
% 70.43/10.85 % (3055274)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=568033369:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 70.43/10.85 % (3055274)Refutation not found, incomplete strategy
% 70.43/10.85 % (3055274)------------------------------
% 70.43/10.85 % (3055274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.85 % (3055274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055274)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055274)Termination reason: Refutation not found, incomplete strategy
% 70.43/10.85 % (3055274)Time elapsed: 0.084 s
% 70.43/10.85 % (3055274)Peak memory usage: 89 MB
% 70.43/10.85 % (3055274)Instructions burned: 164 (million)
% 70.43/10.85 % (3055273)Instruction limit reached!
% 70.43/10.85 % (3055273)------------------------------
% 70.43/10.85 % (3055273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.85 % (3055273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055273)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055273)Termination reason: Instruction limit
% 70.43/10.85 % (3055273)Termination phase: Saturation
% 70.43/10.85 % (3055273)Time elapsed: 0.149 s
% 70.43/10.85 % (3055273)Peak memory usage: 89 MB
% 70.43/10.85 % (3055273)Instructions burned: 303 (million)
% 70.43/10.85 % (3055277)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3641565084:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 70.43/10.85 % (3055274)------------------------------
% 70.43/10.85 % (3055274)------------------------------
% 70.43/10.85 % (3055279)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3896270131:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 70.43/10.85 % (3055277)Instruction limit reached!
% 70.43/10.85 % (3055277)------------------------------
% 70.43/10.85 % (3055277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.85 % (3055277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.85 % (3055277)CaDiCaL version: 2.1.3
% 70.43/10.85 % (3055277)Termination reason: Instruction limit
% 70.43/10.85 % (3055277)Termination phase: Saturation
% 70.43/10.85 % (3055277)Time elapsed: 0.310 s
% 70.43/10.85 % (3055277)Peak memory usage: 89 MB
% 70.43/10.85 % (3055277)Instructions burned: 600 (million)
% 70.43/10.85 % (3055281)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=1510066988:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2954 on theBenchmark for (2954ds/1997Mi)
% 95.98/14.50 % (3055279)Instruction limit reached!
% 95.98/14.50 % (3055279)------------------------------
% 95.98/14.50 % (3055279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.50 % (3055279)CaDiCaL version: 2.1.3
% 95.98/14.50 % (3055279)Termination reason: Instruction limit
% 95.98/14.50 % (3055279)Termination phase: Saturation
% 95.98/14.50 % (3055279)Time elapsed: 1.389 s
% 95.98/14.50 % (3055279)Peak memory usage: 140 MB
% 95.98/14.50 % (3055279)Instructions burned: 2990 (million)
% 95.98/14.50 % (3055283)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=1972771851:i=2088:bd=preordered:av=off_2941 on theBenchmark for (2941ds/2088Mi)
% 95.98/14.50 % (3055281)Instruction limit reached!
% 95.98/14.50 % (3055281)------------------------------
% 95.98/14.50 % (3055281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.50 % (3055281)CaDiCaL version: 2.1.3
% 95.98/14.50 % (3055281)Termination reason: Instruction limit
% 95.98/14.50 % (3055281)Termination phase: Saturation
% 95.98/14.50 % (3055281)Time elapsed: 1.338 s
% 95.98/14.50 % (3055281)Peak memory usage: 136 MB
% 95.98/14.50 % (3055281)Instructions burned: 1997 (million)
% 95.98/14.50 % (3055285)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1863475433:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi)
% 95.98/14.50 % (3055283)Instruction limit reached!
% 95.98/14.50 % (3055283)------------------------------
% 95.98/14.50 % (3055283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.50 % (3055283)CaDiCaL version: 2.1.3
% 95.98/14.50 % (3055283)Termination reason: Instruction limit
% 95.98/14.50 % (3055283)Termination phase: Saturation
% 95.98/14.50 % (3055283)Time elapsed: 0.710 s
% 95.98/14.50 % (3055283)Peak memory usage: 135 MB
% 95.98/14.50 % (3055283)Instructions burned: 2091 (million)
% 95.98/14.50 % (3055285)Instruction limit reached!
% 95.98/14.50 % (3055285)------------------------------
% 95.98/14.50 % (3055285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.50 % (3055285)CaDiCaL version: 2.1.3
% 95.98/14.50 % (3055285)Termination reason: Instruction limit
% 95.98/14.50 % (3055285)Termination phase: Saturation
% 95.98/14.50 % (3055285)Time elapsed: 0.584 s
% 95.98/14.50 % (3055285)Peak memory usage: 98 MB
% 95.98/14.50 % (3055285)Instructions burned: 1099 (million)
% 95.98/14.50 % (3055287)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1235777230:i=433:bd=preordered_2933 on theBenchmark for (2933ds/433Mi)
% 95.98/14.50 % (3055287)Instruction limit reached!
% 95.98/14.50 % (3055287)------------------------------
% 95.98/14.50 % (3055287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.50 % (3055287)CaDiCaL version: 2.1.3
% 95.98/14.50 % (3055287)Termination reason: Instruction limit
% 95.98/14.50 % (3055287)Termination phase: Saturation
% 95.98/14.50 % (3055287)Time elapsed: 0.140 s
% 95.98/14.50 % (3055287)Peak memory usage: 92 MB
% 95.98/14.50 % (3055287)Instructions burned: 434 (million)
% 95.98/14.50 % (3055288)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1278024172:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2931 on theBenchmark for (2931ds/2942Mi)
% 95.98/14.50 % (3055290)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2944581455:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2930 on theBenchmark for (2930ds/6922Mi)
% 95.98/14.50 % (3055271)Instruction limit reached!
% 95.98/14.50 % (3055271)------------------------------
% 95.98/14.50 % (3055271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.50 % (3055271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055271)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055271)Termination reason: Instruction limit
% 110.54/16.54 % (3055271)Termination phase: Saturation
% 110.54/16.54 % (3055271)Time elapsed: 4.569 s
% 110.54/16.54 % (3055271)Peak memory usage: 194 MB
% 110.54/16.54 % (3055271)Instructions burned: 8478 (million)
% 110.54/16.54 % (3055293)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=3375189178:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2918 on theBenchmark for (2918ds/596Mi)
% 110.54/16.54 % (3055293)Instruction limit reached!
% 110.54/16.54 % (3055293)------------------------------
% 110.54/16.54 % (3055293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.54/16.54 % (3055293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055293)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055293)Termination reason: Instruction limit
% 110.54/16.54 % (3055293)Termination phase: Saturation
% 110.54/16.54 % (3055293)Time elapsed: 0.305 s
% 110.54/16.54 % (3055293)Peak memory usage: 91 MB
% 110.54/16.54 % (3055293)Instructions burned: 597 (million)
% 110.54/16.54 % (3055267)Instruction limit reached!
% 110.54/16.54 % (3055267)------------------------------
% 110.54/16.54 % (3055267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.54/16.54 % (3055267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055267)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055267)Termination reason: Instruction limit
% 110.54/16.54 % (3055267)Termination phase: Saturation
% 110.54/16.54 % (3055267)Time elapsed: 6.150 s
% 110.54/16.54 % (3055267)Peak memory usage: 157 MB
% 110.54/16.54 % (3055267)Instructions burned: 10308 (million)
% 110.54/16.54 % (3055288)Instruction limit reached!
% 110.54/16.54 % (3055288)------------------------------
% 110.54/16.54 % (3055288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.54/16.54 % (3055288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055288)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055288)Termination reason: Instruction limit
% 110.54/16.54 % (3055288)Termination phase: Saturation
% 110.54/16.54 % (3055288)Time elapsed: 1.816 s
% 110.54/16.54 % (3055288)Peak memory usage: 136 MB
% 110.54/16.54 % (3055288)Instructions burned: 2942 (million)
% 110.54/16.54 % (3055295)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=257374015:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2913 on theBenchmark for (2913ds/4123Mi)
% 110.54/16.54 % (3055297)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1286531290:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2911 on theBenchmark for (2911ds/1670Mi)
% 110.54/16.54 % (3055296)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3912571835:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2911 on theBenchmark for (2911ds/16411Mi)
% 110.54/16.54 % (3055290)Instruction limit reached!
% 110.54/16.54 % (3055290)------------------------------
% 110.54/16.54 % (3055290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.54/16.54 % (3055290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055290)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055290)Termination reason: Instruction limit
% 110.54/16.54 % (3055290)Termination phase: Saturation
% 110.54/16.54 % (3055290)Time elapsed: 1.999 s
% 110.54/16.54 % (3055290)Peak memory usage: 171 MB
% 110.54/16.54 % (3055290)Instructions burned: 6923 (million)
% 110.54/16.54 % (3055301)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=2934702828:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2908 on theBenchmark for (2908ds/1722Mi)
% 110.54/16.54 % (3055301)Instruction limit reached!
% 110.54/16.54 % (3055301)------------------------------
% 110.54/16.54 % (3055301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.54/16.54 % (3055301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.54/16.54 % (3055301)CaDiCaL version: 2.1.3
% 110.54/16.54 % (3055301)Termination reason: Instruction limit
% 110.54/16.54 % (3055301)Termination phase: Saturation
% 110.54/16.54 % (3055301)Time elapsed: 0.593 s
% 110.54/16.54 % (3055301)Peak memory usage: 133 MB
% 110.54/16.54 % (3055301)Instructions burned: 1725 (million)
% 110.54/16.54 % (3055303)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=3051882417:cts=off:cond=on:i=9530:bs=on:fsd=on_2901 on theBenchmark for (2901ds/9530Mi)
% 67.90/18.43 % (3055297)Instruction limit reached!
% 67.90/18.43 % (3055297)------------------------------
% 67.90/18.43 % (3055297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055297)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055297)Termination reason: Instruction limit
% 67.90/18.43 % (3055297)Termination phase: Saturation
% 67.90/18.43 % (3055297)Time elapsed: 1.091 s
% 67.90/18.43 % (3055297)Peak memory usage: 134 MB
% 67.90/18.43 % (3055297)Instructions burned: 1672 (million)
% 67.90/18.43 % (3055305)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=339754509:st=2:i=4495:sd=10:ss=included_2899 on theBenchmark for (2899ds/4495Mi)
% 67.90/18.43 % (3055305)Refutation not found, incomplete strategy
% 67.90/18.43 % (3055305)------------------------------
% 67.90/18.43 % (3055305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055305)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055305)Termination reason: Refutation not found, incomplete strategy
% 67.90/18.43 % (3055305)Time elapsed: 0.708 s
% 67.90/18.43 % (3055305)Peak memory usage: 129 MB
% 67.90/18.43 % (3055305)Instructions burned: 1033 (million)
% 67.90/18.43 % (3055295)Instruction limit reached!
% 67.90/18.43 % (3055295)------------------------------
% 67.90/18.43 % (3055295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055295)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055295)Termination reason: Instruction limit
% 67.90/18.43 % (3055295)Termination phase: Saturation
% 67.90/18.43 % (3055295)Time elapsed: 2.307 s
% 67.90/18.43 % (3055295)Peak memory usage: 160 MB
% 67.90/18.43 % (3055295)Instructions burned: 4123 (million)
% 67.90/18.43 % (3055305)------------------------------
% 67.90/18.43 % (3055305)------------------------------
% 67.90/18.43 % (3055307)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=7032521:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2888 on theBenchmark for (2888ds/4920Mi)
% 67.90/18.43 % (3055308)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=459719354:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2887 on theBenchmark for (2887ds/2083Mi)
% 67.90/18.43 % (3055308)Instruction limit reached!
% 67.90/18.43 % (3055308)------------------------------
% 67.90/18.43 % (3055308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055308)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055308)Termination reason: Instruction limit
% 67.90/18.43 % (3055308)Termination phase: Saturation
% 67.90/18.43 % (3055308)Time elapsed: 1.308 s
% 67.90/18.43 % (3055308)Peak memory usage: 136 MB
% 67.90/18.43 % (3055308)Instructions burned: 2083 (million)
% 67.90/18.43 % (3055311)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=344864564:i=4629:av=off:gsp=on_2873 on theBenchmark for (2873ds/4629Mi)
% 67.90/18.43 % (3055303)Instruction limit reached!
% 67.90/18.43 % (3055303)------------------------------
% 67.90/18.43 % (3055303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055303)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055303)Termination reason: Instruction limit
% 67.90/18.43 % (3055303)Termination phase: Saturation
% 67.90/18.43 % (3055303)Time elapsed: 3.103 s
% 67.90/18.43 % (3055303)Peak memory usage: 167 MB
% 67.90/18.43 % (3055303)Instructions burned: 9531 (million)
% 67.90/18.43 % (3055313)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3019774132:i=1258:av=off_2869 on theBenchmark for (2869ds/1258Mi)
% 67.90/18.43 % (3055313)Instruction limit reached!
% 67.90/18.43 % (3055313)------------------------------
% 67.90/18.43 % (3055313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055313)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055313)Termination reason: Instruction limit
% 67.90/18.43 % (3055313)Termination phase: Saturation
% 67.90/18.43 % (3055313)Time elapsed: 0.403 s
% 67.90/18.43 % (3055313)Peak memory usage: 100 MB
% 67.90/18.43 % (3055313)Instructions burned: 1260 (million)
% 67.90/18.43 % (3055315)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4277877526:i=7343:av=off:ss=included_2864 on theBenchmark for (2864ds/7343Mi)
% 67.90/18.43 % (3055315)Refutation not found, incomplete strategy
% 67.90/18.43 % (3055315)------------------------------
% 67.90/18.43 % (3055315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055315)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055315)Termination reason: Refutation not found, incomplete strategy
% 67.90/18.43 % (3055315)Time elapsed: 0.381 s
% 67.90/18.43 % (3055315)Peak memory usage: 128 MB
% 67.90/18.43 % (3055315)Instructions burned: 1040 (million)
% 67.90/18.43 % (3055315)------------------------------
% 67.90/18.43 % (3055315)------------------------------
% 67.90/18.43 % (3055317)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2212259193:i=1325:sd=2:ss=axioms:sgt=16_2857 on theBenchmark for (2857ds/1325Mi)
% 67.90/18.43 % (3055317)Refutation not found, incomplete strategy
% 67.90/18.43 % (3055317)------------------------------
% 67.90/18.43 % (3055317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055317)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055317)Termination reason: Refutation not found, incomplete strategy
% 67.90/18.43 % (3055317)Time elapsed: 0.001 s
% 67.90/18.43 % (3055317)Peak memory usage: 88 MB
% 67.90/18.43 % (3055317)Instructions burned: 1 (million)
% 67.90/18.43 % (3055307)Instruction limit reached!
% 67.90/18.43 % (3055307)------------------------------
% 67.90/18.43 % (3055307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055307)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055307)Termination reason: Instruction limit
% 67.90/18.43 % (3055307)Termination phase: Saturation
% 67.90/18.43 % (3055307)Time elapsed: 3.131 s
% 67.90/18.43 % (3055307)Peak memory usage: 147 MB
% 67.90/18.43 % (3055307)Instructions burned: 4921 (million)
% 67.90/18.43 % (3055317)------------------------------
% 67.90/18.43 % (3055317)------------------------------
% 67.90/18.43 % (3055319)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=3906041726:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2855 on theBenchmark for (2855ds/2646Mi)
% 67.90/18.43 % (3055320)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=954517710:i=1489:sd=2:ep=R:ss=axioms_2854 on theBenchmark for (2854ds/1489Mi)
% 67.90/18.43 % (3055320)Instruction limit reached!
% 67.90/18.43 % (3055320)------------------------------
% 67.90/18.43 % (3055320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055320)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055320)Termination reason: Instruction limit
% 67.90/18.43 % (3055320)Termination phase: Saturation
% 67.90/18.43 % (3055320)Time elapsed: 0.553 s
% 67.90/18.43 % (3055320)Peak memory usage: 130 MB
% 67.90/18.43 % (3055320)Instructions burned: 1492 (million)
% 67.90/18.43 % (3055323)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=1970401121:i=1503_2847 on theBenchmark for (2847ds/1503Mi)
% 67.90/18.43 % (3055311)Instruction limit reached!
% 67.90/18.43 % (3055311)------------------------------
% 67.90/18.43 % (3055311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055311)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055311)Termination reason: Instruction limit
% 67.90/18.43 % (3055311)Termination phase: Saturation
% 67.90/18.43 % (3055311)Time elapsed: 2.796 s
% 67.90/18.43 % (3055311)Peak memory usage: 156 MB
% 67.90/18.43 % (3055311)Instructions burned: 4630 (million)
% 67.90/18.43 % (3055325)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1914971558:i=13942:kws=frequency_2843 on theBenchmark for (2843ds/13942Mi)
% 67.90/18.43 % (3055323)Instruction limit reached!
% 67.90/18.43 % (3055323)------------------------------
% 67.90/18.43 % (3055323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055323)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055323)Termination reason: Instruction limit
% 67.90/18.43 % (3055323)Termination phase: Saturation
% 67.90/18.43 % (3055323)Time elapsed: 0.554 s
% 67.90/18.43 % (3055323)Peak memory usage: 132 MB
% 67.90/18.43 % (3055323)Instructions burned: 1503 (million)
% 67.90/18.43 % (3055327)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=2117582004:i=3604:fsr=off:er=filter_2840 on theBenchmark for (2840ds/3604Mi)
% 67.90/18.43 % (3055319)Instruction limit reached!
% 67.90/18.43 % (3055319)------------------------------
% 67.90/18.43 % (3055319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055319)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055319)Termination reason: Instruction limit
% 67.90/18.43 % (3055319)Termination phase: Saturation
% 67.90/18.43 % (3055319)Time elapsed: 1.656 s
% 67.90/18.43 % (3055319)Peak memory usage: 135 MB
% 67.90/18.43 % (3055319)Instructions burned: 2646 (million)
% 67.90/18.43 % (3055329)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2264535190:i=1876:sd=1:ss=included:sgt=32_2837 on theBenchmark for (2837ds/1876Mi)
% 67.90/18.43 % (3055327)Instruction limit reached!
% 67.90/18.43 % (3055327)------------------------------
% 67.90/18.43 % (3055327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.90/18.43 % (3055327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.90/18.43 % (3055327)CaDiCaL version: 2.1.3
% 67.90/18.43 % (3055327)Termination reason: Instruction limit
% 67.90/18.43 % (3055327)Termination phase: Saturation
% 67.90/18.43 % (3055327)Time elapsed: 1.119 s
% 67.90/18.43 % (3055327)Peak memory usage: 146 MB
% 67.90/18.43 % (3055327)Instructions burned: 3607 (million)
% 67.90/18.43 % (3055296)First to succeed.
% 67.90/18.43 % (3055296)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3055210"
% 67.90/18.43 % (3055331)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2014556937:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2828 on theBenchmark for (2828ds/1932Mi)
% 67.90/18.43 % (3055296)Refutation found. Thanks to Tanya!
% 67.90/18.43 % SZS status Unsatisfiable for theBenchmark
% 67.90/18.43 % SZS output start Proof for theBenchmark
% See solution above
% 124.60/18.64 % (3055296)------------------------------
% 124.60/18.64 % (3055296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.60/18.64 % (3055296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.60/18.64 % (3055296)CaDiCaL version: 2.1.3
% 124.60/18.64 % (3055296)Termination reason: Refutation
% 124.60/18.64 % (3055296)Time elapsed: 8.242 s
% 124.60/18.64 % (3055296)Peak memory usage: 190 MB
% 124.60/18.64 % (3055296)Instructions burned: 12554 (million)
% 124.60/18.64 % (3055296)------------------------------
% 124.60/18.64 % (3055296)------------------------------
% 124.60/18.64 % (3055210)Success in time 17.529 s
% 124.60/18.64 % Vampire exiting
%------------------------------------------------------------------------------