%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO033-2 : 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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:51:16 AM UTC 2026
% Result : Unsatisfiable 18.65s 3.58s
% Output : Refutation 19.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 26
% Syntax : Number of formulae : 185 ( 52 unt; 10 def)
% Number of atoms : 445 ( 62 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 479 ( 219 ~; 250 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 11 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-5 aty)
% Number of variables : 275 ( 0 sgn 275 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : equidistant(X0,X1,X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction1) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction2) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ equidistant(X1,X6,X3,X7)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X0,X1,X4)
| ~ between(X2,X3,X5)
| X0 = X1
| equidistant(X4,X6,X5,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outer_five_segment) ).
fof(f7,axiom,
! [X0,X1] :
( ~ between(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',inner_pasch2) ).
fof(f19,axiom,
equidistant(u,v,u1,v1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_u1_to_v1) ).
fof(f20,axiom,
equidistant(v,w,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_to_w_equals_v1_to_w1) ).
fof(f21,axiom,
equidistant(u,x,u1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_x_equals_u1_to_x1) ).
fof(f22,axiom,
equidistant(w,x,w1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',w_to_x_equals_w1_to_x1) ).
fof(f23,axiom,
between(u,v,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_between_u_and_w) ).
fof(f24,axiom,
between(u1,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1_between_u1_and_w1) ).
fof(f25,negated_conjecture,
~ equidistant(v,x,v1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_v_to_x_equals_v1_to_x1) ).
fof(f26,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f27,plain,
! [X0,X1] :
( ~ equidistant(u,v,X0,X1)
| equidistant(X0,X1,u1,v1) ),
inference(resolution,[],[f2,f19]) ).
fof(f31,plain,
! [X0,X1] : equidistant(X0,X1,X0,X1),
inference(resolution,[],[f26,f1]) ).
fof(f32,plain,
equidistant(u1,v1,v,u),
inference(resolution,[],[f26,f19]) ).
fof(f33,plain,
equidistant(v1,w1,w,v),
inference(resolution,[],[f26,f20]) ).
fof(f37,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X0,X1) ),
inference(resolution,[],[f31,f2]) ).
fof(f40,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X0,X1),X3),
inference(resolution,[],[f5,f26]) ).
fof(f41,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X0,extension(X1,X0,X2,X3),X4,X5)
| equidistant(X4,X5,X2,X3) ),
inference(resolution,[],[f5,f2]) ).
fof(f42,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f5,f3]) ).
fof(f43,plain,
! [X2,X0] : equidistant(X0,X0,X2,X2),
inference(superposition,[],[f5,f42]) ).
fof(f44,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f4,f42]) ).
fof(f46,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X0,X1,X2)
| equidistant(X1,X2,X3,X3) ),
inference(resolution,[],[f43,f2]) ).
fof(f52,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X2,X3),
inference(resolution,[],[f41,f1]) ).
fof(f60,plain,
! [X2,X3,X0,X1] :
( ~ between(X3,X0,X2)
| inner_pasch(X0,X1,X2,X0,X3) = X0
| ~ between(X0,X1,X2) ),
inference(resolution,[],[f7,f9]) ).
fof(f61,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(f71,plain,
equidistant(w,v,w1,v1),
inference(resolution,[],[f33,f26]) ).
fof(f75,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X3,X4,X5,X4)
| ~ equidistant(X0,X1,X0,X2)
| ~ equidistant(X3,X0,X5,X0)
| ~ between(X3,X0,X1)
| ~ between(X5,X0,X2)
| X0 = X3
| equidistant(X1,X4,X2,X4) ),
inference(resolution,[],[f6,f31]) ).
fof(f78,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(v,X0,v1,X1)
| ~ equidistant(X2,w,X3,w1)
| ~ equidistant(X2,v,X3,v1)
| ~ between(X2,v,X0)
| ~ between(X3,v1,X1)
| v = X2
| equidistant(X0,w,X1,w1) ),
inference(resolution,[],[f6,f20]) ).
fof(f80,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(u,X0,u1,X1)
| ~ equidistant(X2,x,X3,x1)
| ~ equidistant(X2,u,X3,u1)
| ~ between(X2,u,X0)
| ~ between(X3,u1,X1)
| u = X2
| equidistant(X0,x,X1,x1) ),
inference(resolution,[],[f6,f21]) ).
fof(f127,definition,
( spl0_9
<=> equidistant(v,u,v1,u1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f128,plain,
( equidistant(v,u,v1,u1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f139,definition,
( spl0_12
<=> u = v ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f140,plain,
( u != v
| spl0_12 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f141,plain,
( u = v
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f158,plain,
! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,v)
| ~ between(X1,u1,v1)
| u = X0
| equidistant(v,x,v1,x1) ),
inference(resolution,[],[f80,f19]) ).
fof(f160,plain,
! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,v)
| ~ between(X1,u1,v1)
| u = X0 ),
inference(forward_subsumption_resolution,[],[f158,f25]) ).
fof(f192,definition,
( spl0_21
<=> u = w ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f193,plain,
( u != w
| spl0_21 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f194,plain,
( u = w
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f204,definition,
( spl0_24
<=> equidistant(w,u,w1,u1) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f205,plain,
( equidistant(w,u,w1,u1)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( ~ equidistant(w,u,w1,u1)
| spl0_24 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f240,plain,
equidistant(v,u,v1,u1),
inference(resolution,[],[f32,f26]) ).
fof(f241,plain,
! [X0,X1] :
( ~ equidistant(u1,v1,X0,X1)
| equidistant(X0,X1,v,u) ),
inference(resolution,[],[f32,f2]) ).
fof(f242,plain,
spl0_9,
inference(avatar_split_clause,[],[f240,f127]) ).
fof(f243,plain,
( ! [X0,X1] :
( ~ equidistant(X0,w,X1,w1)
| ~ equidistant(X0,v,X1,v1)
| ~ between(X0,v,u)
| ~ between(X1,v1,u1)
| v = X0
| equidistant(u,w,u1,w1) )
| ~ spl0_9 ),
inference(resolution,[],[f128,f78]) ).
fof(f248,definition,
( spl0_30
<=> equidistant(u,w,u1,w1) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f250,plain,
( equidistant(u,w,u1,w1)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl0_31
<=> ! [X0,X1] :
( ~ equidistant(X0,w,X1,w1)
| v = X0
| ~ between(X1,v1,u1)
| ~ between(X0,v,u)
| ~ equidistant(X0,v,X1,v1) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f253,plain,
( ! [X0,X1] :
( ~ equidistant(X0,w,X1,w1)
| v = X0
| ~ between(X1,v1,u1)
| ~ between(X0,v,u)
| ~ equidistant(X0,v,X1,v1) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( spl0_30
| spl0_31
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f243,f127,f252,f248]) ).
fof(f258,plain,
( equidistant(u1,w1,w,u)
| ~ spl0_30 ),
inference(resolution,[],[f250,f26]) ).
fof(f262,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X3,X2),
inference(resolution,[],[f40,f26]) ).
fof(f263,plain,
! [X2,X3,X0,X1,X4,X5] :
( equidistant(X2,X3,extension(X4,X5,X0,X1),X5)
| ~ equidistant(X0,X1,X2,X3) ),
inference(resolution,[],[f40,f2]) ).
fof(f268,plain,
! [X0,X1] : equidistant(extension(X0,X1,u,v),X1,u1,v1),
inference(resolution,[],[f40,f27]) ).
fof(f274,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(extension(X0,X1,X2,X3),X1,X4,X5)
| equidistant(X4,X5,X3,X2) ),
inference(resolution,[],[f262,f2]) ).
fof(f378,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,X2,extension(X3,X2,X0,X1)),
inference(resolution,[],[f37,f5]) ).
fof(f393,plain,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X3,X2),
inference(resolution,[],[f378,f26]) ).
fof(f421,plain,
! [X0] :
( ~ between(v,X0,w)
| v = inner_pasch(v,X0,w,v,u) ),
inference(resolution,[],[f60,f23]) ).
fof(f422,plain,
! [X0] :
( ~ between(v1,X0,w1)
| v1 = inner_pasch(v1,X0,w1,v1,u1) ),
inference(resolution,[],[f60,f24]) ).
fof(f423,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,extension(X2,X0,X3,X4))
| inner_pasch(X0,X1,extension(X2,X0,X3,X4),X0,X2) = X0 ),
inference(resolution,[],[f60,f4]) ).
fof(f427,plain,
v1 = inner_pasch(v1,w1,w1,v1,u1),
inference(resolution,[],[f422,f44]) ).
fof(f430,plain,
( between(w1,v1,u1)
| ~ between(u1,v1,w1)
| ~ between(v1,w1,w1) ),
inference(superposition,[],[f8,f427]) ).
fof(f432,plain,
( between(w1,v1,u1)
| ~ between(v1,w1,w1) ),
inference(forward_subsumption_resolution,[],[f430,f24]) ).
fof(f433,plain,
between(w1,v1,u1),
inference(forward_subsumption_resolution,[],[f432,f44]) ).
fof(f435,plain,
v = inner_pasch(v,w,w,v,u),
inference(resolution,[],[f421,f44]) ).
fof(f438,plain,
( between(w,v,u)
| ~ between(u,v,w)
| ~ between(v,w,w) ),
inference(superposition,[],[f8,f435]) ).
fof(f440,plain,
( between(w,v,u)
| ~ between(v,w,w) ),
inference(forward_subsumption_resolution,[],[f438,f23]) ).
fof(f441,plain,
between(w,v,u),
inference(forward_subsumption_resolution,[],[f440,f44]) ).
fof(f462,plain,
! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,X0,X2)
| ~ equidistant(X3,X0,X3,X0)
| ~ between(X3,X0,X1)
| ~ between(X3,X0,X2)
| X0 = X3
| equidistant(X1,X4,X2,X4) ),
inference(resolution,[],[f75,f31]) ).
fof(f471,plain,
! [X2,X3,X0,X1,X4] :
( ~ equidistant(X0,X1,X0,X2)
| ~ between(X3,X0,X1)
| ~ between(X3,X0,X2)
| X0 = X3
| equidistant(X1,X4,X2,X4) ),
inference(forward_subsumption_resolution,[],[f462,f31]) ).
fof(f477,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,extension(X2,X1,X1,X3))
| ~ between(X0,X1,X3)
| X0 = X1
| equidistant(extension(X2,X1,X1,X3),X4,X3,X4) ),
inference(resolution,[],[f471,f5]) ).
fof(f645,plain,
( between(u,v,u)
| ~ spl0_21 ),
inference(superposition,[],[f441,f194]) ).
fof(f763,plain,
( u = v
| ~ spl0_21 ),
inference(resolution,[],[f645,f7]) ).
fof(f766,plain,
( $false
| spl0_12
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f763,f140]) ).
fof(f767,plain,
( spl0_12
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f766]) ).
fof(f805,plain,
( ! [X0,X1] : equidistant(extension(X0,X1,v,v),X1,u1,v1)
| ~ spl0_12 ),
inference(superposition,[],[f268,f141]) ).
fof(f853,plain,
( ! [X1] : equidistant(X1,X1,u1,v1)
| ~ spl0_12 ),
inference(forward_demodulation,[],[f805,f42]) ).
fof(f888,plain,
( ! [X0] : equidistant(u1,v1,X0,X0)
| ~ spl0_12 ),
inference(resolution,[],[f853,f26]) ).
fof(f909,plain,
( u1 = v1
| ~ spl0_12 ),
inference(resolution,[],[f888,f3]) ).
fof(f920,plain,
( equidistant(u,x,v1,x1)
| ~ spl0_12 ),
inference(superposition,[],[f21,f909]) ).
fof(f967,plain,
( equidistant(v,x,v1,x1)
| ~ spl0_12 ),
inference(forward_demodulation,[],[f920,f141]) ).
fof(f978,plain,
( $false
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f967,f25]) ).
fof(f979,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f978]) ).
fof(f1036,plain,
( v = w
| ~ between(w1,v1,u1)
| ~ between(w,v,u)
| ~ equidistant(w,v,w1,v1)
| ~ spl0_31 ),
inference(resolution,[],[f253,f43]) ).
fof(f1058,plain,
( v = w
| ~ between(w,v,u)
| ~ equidistant(w,v,w1,v1)
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1036,f433]) ).
fof(f1059,plain,
( v = w
| ~ equidistant(w,v,w1,v1)
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1058,f441]) ).
fof(f1060,plain,
( v = w
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1059,f71]) ).
fof(f1068,plain,
( equidistant(v,v,w1,v1)
| ~ spl0_31 ),
inference(superposition,[],[f71,f1060]) ).
fof(f1098,plain,
( ! [X0] : equidistant(w1,v1,X0,X0)
| ~ spl0_31 ),
inference(resolution,[],[f1068,f46]) ).
fof(f1107,plain,
( v1 = w1
| ~ spl0_31 ),
inference(resolution,[],[f1098,f3]) ).
fof(f1124,plain,
( equidistant(w,x,v1,x1)
| ~ spl0_31 ),
inference(superposition,[],[f22,f1107]) ).
fof(f1166,plain,
( equidistant(v,x,v1,x1)
| ~ spl0_31 ),
inference(forward_demodulation,[],[f1124,f1060]) ).
fof(f1172,plain,
( $false
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f1166,f25]) ).
fof(f1173,plain,
~ spl0_31,
inference(avatar_contradiction_clause,[],[f1172]) ).
fof(f1207,plain,
( equidistant(w,u,w1,u1)
| ~ spl0_30 ),
inference(resolution,[],[f258,f26]) ).
fof(f1209,plain,
( $false
| spl0_24
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1207,f206]) ).
fof(f1210,plain,
( spl0_24
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1209]) ).
fof(f1316,plain,
! [X2,X3,X0,X1,X4,X5] :
( equidistant(extension(X4,X5,X0,X1),X5,X3,X2)
| ~ equidistant(X0,X1,X2,X3) ),
inference(resolution,[],[f263,f26]) ).
fof(f1317,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ equidistant(X2,X3,X4,X5)
| ~ equidistant(X0,X1,X2,X3)
| equidistant(X4,X5,extension(X6,X7,X0,X1),X7) ),
inference(resolution,[],[f263,f2]) ).
fof(f1580,plain,
! [X2,X3,X0,X1] : inner_pasch(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3),X0,X1) = X0,
inference(resolution,[],[f423,f44]) ).
fof(f1590,plain,
! [X2,X3,X0,X1] :
( between(extension(X1,X0,X2,X3),X0,X1)
| ~ between(X1,X0,extension(X1,X0,X2,X3))
| ~ between(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3)) ),
inference(superposition,[],[f8,f1580]) ).
fof(f1592,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)) ),
inference(forward_subsumption_resolution,[],[f1590,f4]) ).
fof(f1593,plain,
! [X2,X3,X0,X1] : between(extension(X1,X0,X2,X3),X0,X1),
inference(forward_subsumption_resolution,[],[f1592,f44]) ).
fof(f1594,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| inner_pasch(extension(X2,X0,X3,X4),X0,X2,X1,X0) = X0 ),
inference(resolution,[],[f1593,f61]) ).
fof(f1723,plain,
! [X0,X1] : u = inner_pasch(extension(w,u,X0,X1),u,w,v,u),
inference(resolution,[],[f1594,f23]) ).
fof(f1724,plain,
! [X0,X1] : u1 = inner_pasch(extension(w1,u1,X0,X1),u1,w1,v1,u1),
inference(resolution,[],[f1594,f24]) ).
fof(f1731,plain,
! [X0,X1] :
( between(v,u,extension(w,u,X0,X1))
| ~ between(u,v,w)
| ~ between(extension(w,u,X0,X1),u,w) ),
inference(superposition,[],[f9,f1723]) ).
fof(f1732,plain,
! [X0,X1] :
( between(v,u,extension(w,u,X0,X1))
| ~ between(extension(w,u,X0,X1),u,w) ),
inference(forward_subsumption_resolution,[],[f1731,f23]) ).
fof(f1733,plain,
! [X0,X1] : between(v,u,extension(w,u,X0,X1)),
inference(forward_subsumption_resolution,[],[f1732,f1593]) ).
fof(f1736,plain,
! [X0,X1] :
( between(v1,u1,extension(w1,u1,X0,X1))
| ~ between(u1,v1,w1)
| ~ between(extension(w1,u1,X0,X1),u1,w1) ),
inference(superposition,[],[f9,f1724]) ).
fof(f1737,plain,
! [X0,X1] :
( between(v1,u1,extension(w1,u1,X0,X1))
| ~ between(extension(w1,u1,X0,X1),u1,w1) ),
inference(forward_subsumption_resolution,[],[f1736,f24]) ).
fof(f1738,plain,
! [X0,X1] : between(v1,u1,extension(w1,u1,X0,X1)),
inference(forward_subsumption_resolution,[],[f1737,f1593]) ).
fof(f2218,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,u,extension(X2,u,X3,u1))
| ~ equidistant(X0,u,X1,u1)
| ~ equidistant(X0,x,X1,x1)
| ~ between(X1,u1,X3)
| u = X0
| equidistant(extension(X2,u,X3,u1),x,X3,x1) ),
inference(resolution,[],[f393,f80]) ).
fof(f2235,plain,
! [X2,X3,X0,X1] :
( equidistant(extension(X0,X1,X1,X2),X3,X2,X3)
| X0 = X1
| ~ between(X0,X1,X2) ),
inference(resolution,[],[f477,f4]) ).
fof(f2240,plain,
! [X0,X1] :
( ~ between(v1,u1,X0)
| u1 = v1
| equidistant(extension(w1,u1,u1,X0),X1,X0,X1) ),
inference(resolution,[],[f477,f1738]) ).
fof(f2260,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| X0 = X1
| extension(X0,X1,X1,X2) = X2 ),
inference(resolution,[],[f2235,f3]) ).
fof(f2273,plain,
! [X0,X1] :
( u = v
| extension(w,u,X0,X1) = extension(v,u,u,extension(w,u,X0,X1)) ),
inference(resolution,[],[f2260,f1733]) ).
fof(f2308,plain,
( ! [X0,X1] : extension(w,u,X0,X1) = extension(v,u,u,extension(w,u,X0,X1))
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f2273,f140]) ).
fof(f2324,definition,
( spl0_95
<=> u1 = v1 ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f2325,plain,
( u1 != v1
| spl0_95 ),
inference(avatar_component_clause,[],[f2324]) ).
fof(f2326,plain,
( u1 = v1
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f2324]) ).
fof(f2328,definition,
( spl0_96
<=> ! [X0,X1] :
( ~ between(v1,u1,X0)
| equidistant(extension(w1,u1,u1,X0),X1,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f2329,plain,
( ! [X0,X1] :
( equidistant(extension(w1,u1,u1,X0),X1,X0,X1)
| ~ between(v1,u1,X0) )
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f2328]) ).
fof(f2330,plain,
( spl0_95
| spl0_96 ),
inference(avatar_split_clause,[],[f2240,f2328,f2324]) ).
fof(f2774,plain,
( ! [X0] :
( ~ between(v1,u1,X0)
| extension(w1,u1,u1,X0) = X0 )
| ~ spl0_96 ),
inference(resolution,[],[f2329,f3]) ).
fof(f2791,plain,
( ! [X0,X1] : extension(v1,u1,X0,X1) = extension(w1,u1,u1,extension(v1,u1,X0,X1))
| ~ spl0_96 ),
inference(resolution,[],[f2774,f4]) ).
fof(f3128,plain,
( ! [X0,X1] : between(w1,u1,extension(v1,u1,X0,X1))
| ~ spl0_96 ),
inference(superposition,[],[f4,f2791]) ).
fof(f3296,plain,
( ! [X0,X1] : between(extension(w,u,X0,X1),u,v)
| spl0_12 ),
inference(superposition,[],[f1593,f2308]) ).
fof(f3351,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X3,X2,X1,X0) ),
inference(resolution,[],[f1316,f274]) ).
fof(f4004,plain,
! [X0,X1] : equidistant(extension(X0,X1,u1,v1),X1,v,u),
inference(resolution,[],[f241,f40]) ).
fof(f4493,plain,
! [X2,X3,X0,X1] :
( equidistant(u1,v1,extension(X2,X3,X0,X1),X3)
| ~ equidistant(X0,X1,u,v) ),
inference(resolution,[],[f1317,f19]) ).
fof(f4858,plain,
( ! [X0,X1] : equidistant(extension(X0,X1,v1,v1),X1,v,u)
| ~ spl0_95 ),
inference(superposition,[],[f4004,f2326]) ).
fof(f4861,plain,
( ! [X1] : equidistant(X1,X1,v,u)
| ~ spl0_95 ),
inference(forward_demodulation,[],[f4858,f42]) ).
fof(f5013,plain,
( ! [X0] : equidistant(u,v,X0,X0)
| ~ spl0_95 ),
inference(resolution,[],[f4861,f3351]) ).
fof(f5041,plain,
( u = v
| ~ spl0_95 ),
inference(resolution,[],[f5013,f3]) ).
fof(f5047,plain,
( $false
| spl0_12
| ~ spl0_95 ),
inference(forward_subsumption_resolution,[],[f5041,f140]) ).
fof(f5048,plain,
( spl0_12
| ~ spl0_95 ),
inference(avatar_contradiction_clause,[],[f5047]) ).
fof(f9475,plain,
! [X2,X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X1,u1,X2)
| u = X0
| equidistant(extension(X0,u,X2,u1),x,X2,x1) ),
inference(resolution,[],[f2218,f4]) ).
fof(f9502,plain,
! [X0] :
( ~ equidistant(w,u,w1,u1)
| ~ between(w1,u1,X0)
| u = w
| equidistant(extension(w,u,X0,u1),x,X0,x1) ),
inference(resolution,[],[f9475,f22]) ).
fof(f9515,plain,
( ! [X0] :
( ~ between(w1,u1,X0)
| u = w
| equidistant(extension(w,u,X0,u1),x,X0,x1) )
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f9502,f205]) ).
fof(f9524,plain,
( ! [X0] :
( equidistant(extension(w,u,X0,u1),x,X0,x1)
| ~ between(w1,u1,X0) )
| spl0_21
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f9515,f193]) ).
fof(f9527,plain,
( ! [X0] :
( ~ between(w1,u1,X0)
| ~ equidistant(extension(w,u,X0,u1),u,X0,u1)
| ~ between(extension(w,u,X0,u1),u,v)
| ~ between(X0,u1,v1)
| u = extension(w,u,X0,u1) )
| spl0_21
| ~ spl0_24 ),
inference(resolution,[],[f9524,f160]) ).
fof(f9551,plain,
( ! [X0] :
( ~ between(w1,u1,X0)
| ~ between(extension(w,u,X0,u1),u,v)
| ~ between(X0,u1,v1)
| u = extension(w,u,X0,u1) )
| spl0_21
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f9527,f52]) ).
fof(f9552,plain,
( ! [X0] :
( ~ between(w1,u1,X0)
| ~ between(X0,u1,v1)
| u = extension(w,u,X0,u1) )
| spl0_12
| spl0_21
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f9551,f3296]) ).
fof(f9553,plain,
( ! [X0,X1] :
( ~ between(extension(v1,u1,X0,X1),u1,v1)
| u = extension(w,u,extension(v1,u1,X0,X1),u1) )
| spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96 ),
inference(resolution,[],[f9552,f3128]) ).
fof(f9557,plain,
( ! [X0,X1] : u = extension(w,u,extension(v1,u1,X0,X1),u1)
| spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96 ),
inference(forward_subsumption_resolution,[],[f9553,f1593]) ).
fof(f9621,definition,
( spl0_329
<=> equidistant(u1,v1,u,u) ),
introduced(definition,[new_symbols(definition,[spl0_329])],[avatar_definition]) ).
fof(f9623,plain,
( equidistant(u1,v1,u,u)
| ~ spl0_329 ),
inference(avatar_component_clause,[],[f9621]) ).
fof(f9735,plain,
( ! [X0,X1] :
( equidistant(u1,v1,u,u)
| ~ equidistant(extension(v1,u1,X0,X1),u1,u,v) )
| spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96 ),
inference(superposition,[],[f4493,f9557]) ).
fof(f9747,definition,
( spl0_336
<=> ! [X0,X1] : ~ equidistant(extension(v1,u1,X0,X1),u1,u,v) ),
introduced(definition,[new_symbols(definition,[spl0_336])],[avatar_definition]) ).
fof(f9748,plain,
( ! [X0,X1] : ~ equidistant(extension(v1,u1,X0,X1),u1,u,v)
| ~ spl0_336 ),
inference(avatar_component_clause,[],[f9747]) ).
fof(f9749,plain,
( spl0_336
| spl0_329
| spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f9735,f2328,f204,f192,f139,f9621,f9747]) ).
fof(f10880,plain,
( u1 = v1
| ~ spl0_329 ),
inference(resolution,[],[f9623,f3]) ).
fof(f10881,plain,
( $false
| spl0_95
| ~ spl0_329 ),
inference(forward_subsumption_resolution,[],[f10880,f2325]) ).
fof(f10882,plain,
( spl0_95
| ~ spl0_329 ),
inference(avatar_contradiction_clause,[],[f10881]) ).
fof(f11113,plain,
( $false
| ~ spl0_336 ),
inference(resolution,[],[f9748,f52]) ).
fof(f11123,plain,
~ spl0_336,
inference(avatar_contradiction_clause,[],[f11113]) ).
cnf(s11,plain,
spl0_9,
inference(sat_conversion,[],[f242]) ).
cnf(s12,plain,
( ~ spl0_9
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f254]) ).
cnf(s29,plain,
( spl0_12
| ~ spl0_21 ),
inference(sat_conversion,[],[f767]) ).
cnf(s36,plain,
~ spl0_12,
inference(sat_conversion,[],[f979]) ).
cnf(s43,plain,
~ spl0_31,
inference(sat_conversion,[],[f1173]) ).
cnf(s45,plain,
( spl0_24
| ~ spl0_30 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s72,plain,
( spl0_95
| spl0_96 ),
inference(sat_conversion,[],[f2330]) ).
cnf(s157,plain,
( spl0_12
| ~ spl0_95 ),
inference(sat_conversion,[],[f5048]) ).
cnf(s298,plain,
( spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96
| spl0_329
| spl0_336 ),
inference(sat_conversion,[],[f9749]) ).
cnf(s355,plain,
( spl0_95
| ~ spl0_329 ),
inference(sat_conversion,[],[f10882]) ).
cnf(s369,plain,
~ spl0_336,
inference(sat_conversion,[],[f11123]) ).
cnf(s370,plain,
( spl0_12
| spl0_21
| ~ spl0_24
| ~ spl0_96
| spl0_329 ),
inference(rat,[],[s298,s369]) ).
cnf(s372,plain,
~ spl0_95,
inference(rat,[],[s157,s36]) ).
cnf(s373,plain,
~ spl0_329,
inference(rat,[],[s355,s372]) ).
cnf(s378,plain,
spl0_96,
inference(rat,[],[s72,s372]) ).
cnf(s379,plain,
~ spl0_21,
inference(rat,[],[s29,s36]) ).
cnf(s382,plain,
~ spl0_24,
inference(rat,[],[s370,s373,s378,s36,s379]) ).
cnf(s384,plain,
~ spl0_30,
inference(rat,[],[s45,s382]) ).
cnf(s387,plain,
~ spl0_9,
inference(rat,[],[s12,s43,s384]) ).
cnf(s388,plain,
$false,
inference(rat,[],[s11,s387]) ).
fof(f11124,plain,
$false,
inference(avatar_sat_refutation,[],[s388]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO033-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 06:44:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 9.86/2.27 % (3204706)Input is clausal, will run a generic CNF schedule.
% 9.86/2.27 % (3204713)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1310409860:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.86/2.27 % (3204714)lrs+10_1_sil=8000:sp=occurrence:random_seed=2479792266:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.86/2.27 % (3204712)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=571641554:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.86/2.27 % (3204717)dis-21_1_sil=8000:lcm=predicate:random_seed=121904404: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)
% 9.86/2.27 % (3204711)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=2345964219:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.86/2.27 % (3204715)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=70912002:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.86/2.27 % (3204716)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3477851806:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.86/2.27 % (3204714)Refutation not found, incomplete strategy
% 9.86/2.27 % (3204714)------------------------------
% 9.86/2.27 % (3204714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.27 % (3204714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.27 % (3204714)CaDiCaL version: 2.1.3
% 9.86/2.27 % (3204714)Termination reason: Refutation not found, incomplete strategy
% 9.86/2.27 % (3204714)Time elapsed: 0.003 s
% 9.86/2.27 % (3204714)Peak memory usage: 87 MB
% 9.86/2.27 % (3204714)Instructions burned: 5 (million)
% 9.86/2.27 % (3204715)Instruction limit reached!
% 9.86/2.27 % (3204715)------------------------------
% 9.86/2.27 % (3204715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.27 % (3204715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.27 % (3204715)CaDiCaL version: 2.1.3
% 9.86/2.27 % (3204715)Termination reason: Instruction limit
% 9.86/2.27 % (3204715)Termination phase: Saturation
% 9.86/2.27 % (3204715)Time elapsed: 0.045 s
% 9.86/2.27 % (3204715)Peak memory usage: 87 MB
% 9.86/2.27 % (3204715)Instructions burned: 116 (million)
% 9.86/2.27 % (3204717)Instruction limit reached!
% 9.86/2.27 % (3204717)------------------------------
% 9.86/2.27 % (3204717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.27 % (3204717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.27 % (3204717)CaDiCaL version: 2.1.3
% 9.86/2.27 % (3204717)Termination reason: Instruction limit
% 9.86/2.27 % (3204717)Termination phase: Saturation
% 9.86/2.27 % (3204717)Time elapsed: 0.068 s
% 9.86/2.27 % (3204717)Peak memory usage: 88 MB
% 9.86/2.27 % (3204717)Instructions burned: 117 (million)
% 9.86/2.27 % (3204716)Instruction limit reached!
% 9.86/2.27 % (3204716)------------------------------
% 9.86/2.27 % (3204716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.86/2.27 % (3204716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.86/2.27 % (3204716)CaDiCaL version: 2.1.3
% 9.86/2.27 % (3204716)Termination reason: Instruction limit
% 9.86/2.27 % (3204716)Termination phase: Saturation
% 9.86/2.27 % (3204716)Time elapsed: 0.124 s
% 9.86/2.27 % (3204716)Peak memory usage: 89 MB
% 9.86/2.27 % (3204716)Instructions burned: 181 (million)
% 9.86/2.27 % (3204725)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=2447328930:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.86/2.27 % (3204726)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1634599032: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)
% 9.86/2.27 % (3204714)------------------------------
% 9.86/2.27 % (3204714)------------------------------
% 9.86/2.27 % (3204727)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=770889576:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.86/2.27 % (3204725)Instruction limit reached!
% 9.86/2.27 % (3204725)------------------------------
% 18.65/3.57 % (3204725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204725)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204725)Termination reason: Instruction limit
% 18.65/3.57 % (3204725)Termination phase: Saturation
% 18.65/3.57 % (3204725)Time elapsed: 0.107 s
% 18.65/3.57 % (3204725)Peak memory usage: 89 MB
% 18.65/3.57 % (3204725)Instructions burned: 144 (million)
% 18.65/3.57 % (3204726)Instruction limit reached!
% 18.65/3.57 % (3204726)------------------------------
% 18.65/3.57 % (3204726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204726)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204726)Termination reason: Instruction limit
% 18.65/3.57 % (3204726)Termination phase: Saturation
% 18.65/3.57 % (3204726)Time elapsed: 0.102 s
% 18.65/3.57 % (3204726)Peak memory usage: 89 MB
% 18.65/3.57 % (3204726)Instructions burned: 189 (million)
% 18.65/3.57 % (3204727)Instruction limit reached!
% 18.65/3.57 % (3204727)------------------------------
% 18.65/3.57 % (3204727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204727)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204727)Termination reason: Instruction limit
% 18.65/3.57 % (3204727)Termination phase: Saturation
% 18.65/3.57 % (3204727)Time elapsed: 0.113 s
% 18.65/3.57 % (3204727)Peak memory usage: 89 MB
% 18.65/3.57 % (3204727)Instructions burned: 220 (million)
% 18.65/3.57 % (3204731)lrs+10_64_to=lpo:sil=8000:random_seed=2587313497:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.65/3.57 % (3204732)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1684312916:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.65/3.57 % (3204733)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2925062302:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.65/3.57 % (3204731)Instruction limit reached!
% 18.65/3.57 % (3204731)------------------------------
% 18.65/3.57 % (3204731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204731)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204731)Termination reason: Instruction limit
% 18.65/3.57 % (3204731)Termination phase: Saturation
% 18.65/3.57 % (3204731)Time elapsed: 0.080 s
% 18.65/3.57 % (3204731)Peak memory usage: 89 MB
% 18.65/3.57 % (3204731)Instructions burned: 127 (million)
% 18.65/3.57 % (3204734)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3488099621:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.65/3.57 % (3204733)Instruction limit reached!
% 18.65/3.57 % (3204733)------------------------------
% 18.65/3.57 % (3204733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204733)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204733)Termination reason: Instruction limit
% 18.65/3.57 % (3204733)Termination phase: Saturation
% 18.65/3.57 % (3204733)Time elapsed: 0.108 s
% 18.65/3.57 % (3204733)Peak memory usage: 90 MB
% 18.65/3.57 % (3204733)Instructions burned: 158 (million)
% 18.65/3.57 % (3204732)Instruction limit reached!
% 18.65/3.57 % (3204732)------------------------------
% 18.65/3.57 % (3204732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204732)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204732)Termination reason: Instruction limit
% 18.65/3.57 % (3204732)Termination phase: Saturation
% 18.65/3.57 % (3204732)Time elapsed: 0.109 s
% 18.65/3.57 % (3204732)Peak memory usage: 88 MB
% 18.65/3.57 % (3204732)Instructions burned: 195 (million)
% 18.65/3.57 % (3204738)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=305380113:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.65/3.57 % (3204738)Instruction limit reached!
% 18.65/3.57 % (3204738)------------------------------
% 18.65/3.57 % (3204738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204738)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204738)Termination reason: Instruction limit
% 18.65/3.57 % (3204738)Termination phase: Saturation
% 18.65/3.57 % (3204738)Time elapsed: 0.059 s
% 18.65/3.57 % (3204738)Peak memory usage: 88 MB
% 18.65/3.57 % (3204738)Instructions burned: 106 (million)
% 18.65/3.57 % (3204740)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4165420272:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.65/3.57 % (3204741)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3078711069:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 18.65/3.57 % (3204740)Instruction limit reached!
% 18.65/3.57 % (3204740)------------------------------
% 18.65/3.57 % (3204740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204740)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204740)Termination reason: Instruction limit
% 18.65/3.57 % (3204740)Termination phase: Saturation
% 18.65/3.57 % (3204740)Time elapsed: 0.074 s
% 18.65/3.57 % (3204740)Peak memory usage: 89 MB
% 18.65/3.57 % (3204740)Instructions burned: 108 (million)
% 18.65/3.57 % (3204741)Instruction limit reached!
% 18.65/3.57 % (3204741)------------------------------
% 18.65/3.57 % (3204741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204741)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204741)Termination reason: Instruction limit
% 18.65/3.57 % (3204741)Termination phase: Saturation
% 18.65/3.57 % (3204741)Time elapsed: 0.089 s
% 18.65/3.57 % (3204741)Peak memory usage: 87 MB
% 18.65/3.57 % (3204741)Instructions burned: 245 (million)
% 18.65/3.57 % (3204743)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2601420174:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 18.65/3.57 % (3204746)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2312434666:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 18.65/3.57 % (3204747)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1065738683:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 18.65/3.57 % (3204746)Instruction limit reached!
% 18.65/3.57 % (3204746)------------------------------
% 18.65/3.57 % (3204746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204746)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204746)Termination reason: Instruction limit
% 18.65/3.57 % (3204746)Termination phase: Saturation
% 18.65/3.57 % (3204746)Time elapsed: 0.089 s
% 18.65/3.57 % (3204746)Peak memory usage: 89 MB
% 18.65/3.57 % (3204746)Instructions burned: 134 (million)
% 18.65/3.57 % (3204751)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=970503359:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 18.65/3.57 % (3204747)Instruction limit reached!
% 18.65/3.57 % (3204747)------------------------------
% 18.65/3.57 % (3204747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204747)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204747)Termination reason: Instruction limit
% 18.65/3.57 % (3204747)Termination phase: Saturation
% 18.65/3.57 % (3204747)Time elapsed: 0.285 s
% 18.65/3.57 % (3204747)Peak memory usage: 91 MB
% 18.65/3.57 % (3204747)Instructions burned: 501 (million)
% 18.65/3.57 % (3204751)Instruction limit reached!
% 18.65/3.57 % (3204751)------------------------------
% 18.65/3.57 % (3204751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204751)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204751)Termination reason: Instruction limit
% 18.65/3.57 % (3204751)Termination phase: Saturation
% 18.65/3.57 % (3204751)Time elapsed: 0.130 s
% 18.65/3.57 % (3204751)Peak memory usage: 92 MB
% 18.65/3.57 % (3204751)Instructions burned: 193 (million)
% 18.65/3.57 % (3204753)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3829989165:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 18.65/3.57 % (3204754)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2535277715:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 18.65/3.57 % (3204753)Instruction limit reached!
% 18.65/3.57 % (3204753)------------------------------
% 18.65/3.57 % (3204753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204753)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204753)Termination reason: Instruction limit
% 18.65/3.57 % (3204753)Termination phase: Saturation
% 18.65/3.57 % (3204753)Time elapsed: 0.161 s
% 18.65/3.57 % (3204753)Peak memory usage: 91 MB
% 18.65/3.57 % (3204753)Instructions burned: 264 (million)
% 18.65/3.57 % (3204754)Instruction limit reached!
% 18.65/3.57 % (3204754)------------------------------
% 18.65/3.57 % (3204754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204754)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204754)Termination reason: Instruction limit
% 18.65/3.57 % (3204754)Termination phase: Saturation
% 18.65/3.57 % (3204754)Time elapsed: 0.106 s
% 18.65/3.57 % (3204754)Peak memory usage: 88 MB
% 18.65/3.57 % (3204754)Instructions burned: 156 (million)
% 18.65/3.57 % (3204757)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=2651738941:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 18.65/3.57 % (3204758)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2955907711:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 18.65/3.57 % (3204758)Instruction limit reached!
% 18.65/3.57 % (3204758)------------------------------
% 18.65/3.57 % (3204758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.57 % (3204758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.57 % (3204758)CaDiCaL version: 2.1.3
% 18.65/3.57 % (3204758)Termination reason: Instruction limit
% 18.65/3.57 % (3204758)Termination phase: Saturation
% 18.65/3.57 % (3204758)Time elapsed: 0.187 s
% 18.65/3.58 % (3204758)Peak memory usage: 87 MB
% 18.65/3.58 % (3204758)Instructions burned: 537 (million)
% 18.65/3.58 % (3204761)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4953995:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 18.65/3.58 % (3204761)Instruction limit reached!
% 18.65/3.58 % (3204761)------------------------------
% 18.65/3.58 % (3204761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.58 % (3204761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.58 % (3204761)CaDiCaL version: 2.1.3
% 18.65/3.58 % (3204761)Termination reason: Instruction limit
% 18.65/3.58 % (3204761)Termination phase: Saturation
% 18.65/3.58 % (3204761)Time elapsed: 0.100 s
% 18.65/3.58 % (3204761)Peak memory usage: 88 MB
% 18.65/3.58 % (3204761)Instructions burned: 181 (million)
% 18.65/3.58 % (3204763)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=3012224470:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 18.65/3.58 % (3204734)First to succeed.
% 18.65/3.58 % (3204734)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3204706"
% 18.65/3.58 % (3204734)Refutation found. Thanks to Tanya!
% 18.65/3.58 % SZS status Unsatisfiable for theBenchmark
% 18.65/3.58 % SZS output start Proof for theBenchmark
% See solution above
% 19.81/3.77 % (3204734)------------------------------
% 19.81/3.77 % (3204734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.81/3.77 % (3204734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.81/3.77 % (3204734)CaDiCaL version: 2.1.3
% 19.81/3.77 % (3204734)Termination reason: Refutation
% 19.81/3.77 % (3204734)Time elapsed: 1.799 s
% 19.81/3.77 % (3204734)Peak memory usage: 145 MB
% 19.81/3.77 % (3204734)Instructions burned: 2696 (million)
% 19.81/3.77 % (3204734)------------------------------
% 19.81/3.77 % (3204734)------------------------------
% 19.81/3.77 % (3204706)Success in time 2.72 s
% 19.81/3.77 % Vampire exiting
%------------------------------------------------------------------------------