%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO031-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 : n016.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 12.48s 2.79s
% Output : Refutation 13.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 28
% Syntax : Number of formulae : 248 ( 54 unt; 12 def)
% Number of atoms : 722 ( 110 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 867 ( 393 ~; 462 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 13 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-5 aty)
% Number of variables : 403 ( 0 sgn 403 !; 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(u,w,u1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_w_equals_u1_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(f27,plain,
! [X0,X1] :
( ~ equidistant(u,v,X0,X1)
| equidistant(X0,X1,u1,v1) ),
inference(resolution,[],[f2,f19]) ).
fof(f30,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f31,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(f33,plain,
equidistant(u1,v1,v,u),
inference(resolution,[],[f30,f19]) ).
fof(f34,plain,
equidistant(u1,w1,w,u),
inference(resolution,[],[f30,f20]) ).
fof(f36,plain,
! [X0,X1] : equidistant(X0,X1,X0,X1),
inference(resolution,[],[f30,f1]) ).
fof(f37,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X0,X1),X3),
inference(resolution,[],[f30,f5]) ).
fof(f42,plain,
equidistant(v,u,v1,u1),
inference(resolution,[],[f33,f30]) ).
fof(f48,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f3,f5]) ).
fof(f49,plain,
! [X2,X0] : equidistant(X0,X0,X2,X2),
inference(superposition,[],[f5,f48]) ).
fof(f51,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X0,X1,X2)
| equidistant(X1,X2,X3,X3) ),
inference(resolution,[],[f49,f2]) ).
fof(f53,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f4,f48]) ).
fof(f54,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X3,X2),
inference(resolution,[],[f37,f30]) ).
fof(f63,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X2,X3),
inference(resolution,[],[f31,f1]) ).
fof(f74,plain,
! [X0,X1] : equidistant(extension(X0,X1,u,v),X1,u1,v1),
inference(resolution,[],[f27,f37]) ).
fof(f83,plain,
equidistant(w,u,w1,u1),
inference(resolution,[],[f34,f30]) ).
fof(f85,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(f86,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(f88,plain,
! [X0] :
( ~ between(v,X0,w)
| v = inner_pasch(v,X0,w,v,u) ),
inference(resolution,[],[f85,f23]) ).
fof(f89,plain,
! [X0] :
( ~ between(v1,X0,w1)
| v1 = inner_pasch(v1,X0,w1,v1,u1) ),
inference(resolution,[],[f85,f24]) ).
fof(f96,plain,
v1 = inner_pasch(v1,w1,w1,v1,u1),
inference(resolution,[],[f89,f53]) ).
fof(f97,plain,
( between(w1,v1,u1)
| ~ between(u1,v1,w1)
| ~ between(v1,w1,w1) ),
inference(superposition,[],[f8,f96]) ).
fof(f99,plain,
( between(w1,v1,u1)
| ~ between(v1,w1,w1) ),
inference(forward_subsumption_resolution,[],[f97,f24]) ).
fof(f100,plain,
between(w1,v1,u1),
inference(forward_subsumption_resolution,[],[f99,f53]) ).
fof(f104,plain,
v = inner_pasch(v,w,w,v,u),
inference(resolution,[],[f88,f53]) ).
fof(f105,plain,
( between(w,v,u)
| ~ between(u,v,w)
| ~ between(v,w,w) ),
inference(superposition,[],[f8,f104]) ).
fof(f107,plain,
( between(w,v,u)
| ~ between(v,w,w) ),
inference(forward_subsumption_resolution,[],[f105,f23]) ).
fof(f108,plain,
between(w,v,u),
inference(forward_subsumption_resolution,[],[f107,f53]) ).
fof(f112,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,[],[f86,f4]) ).
fof(f131,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,f36]) ).
fof(f138,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(f139,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(u,X0,u1,X1)
| ~ equidistant(X2,v,X3,v1)
| ~ equidistant(X2,u,X3,u1)
| ~ between(X2,u,X0)
| ~ between(X3,u1,X1)
| u = X2
| equidistant(X0,v,X1,v1) ),
inference(resolution,[],[f6,f19]) ).
fof(f144,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(w,X0,w1,X1)
| ~ equidistant(X2,x,X3,x1)
| ~ equidistant(X2,w,X3,w1)
| ~ between(X2,w,X0)
| ~ between(X3,w1,X1)
| w = X2
| equidistant(X0,x,X1,x1) ),
inference(resolution,[],[f6,f22]) ).
fof(f148,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,[],[f138,f19]) ).
fof(f161,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,[],[f148,f25]) ).
fof(f197,definition,
( spl0_9
<=> u = w ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f198,plain,
( u != w
| spl0_9 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f199,plain,
( u = w
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f220,plain,
! [X0,X1] :
( ~ equidistant(X0,v,X1,v1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,w)
| ~ between(X1,u1,w1)
| u = X0
| equidistant(w,v,w1,v1) ),
inference(resolution,[],[f139,f20]) ).
fof(f233,definition,
( spl0_16
<=> equidistant(w,v,w1,v1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f235,plain,
( equidistant(w,v,w1,v1)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f237,definition,
( spl0_17
<=> ! [X0,X1] :
( ~ equidistant(X0,v,X1,v1)
| u = X0
| ~ between(X1,u1,w1)
| ~ between(X0,u,w)
| ~ equidistant(X0,u,X1,u1) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f238,plain,
( ! [X0,X1] :
( ~ equidistant(X0,v,X1,v1)
| u = X0
| ~ between(X1,u1,w1)
| ~ between(X0,u,w)
| ~ equidistant(X0,u,X1,u1) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f220,f237,f233]) ).
fof(f305,definition,
( spl0_28
<=> u = v ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f306,plain,
( u != v
| spl0_28 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f307,plain,
( u = v
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f390,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,[],[f131,f36]) ).
fof(f397,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,[],[f390,f36]) ).
fof(f401,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,[],[f397,f5]) ).
fof(f492,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(extension(X0,X1,X2,X3),X1,X4,X5)
| equidistant(X4,X5,X3,X2) ),
inference(resolution,[],[f54,f2]) ).
fof(f504,plain,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X3,X2),
inference(resolution,[],[f492,f1]) ).
fof(f510,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X1,X0),X3),
inference(resolution,[],[f504,f30]) ).
fof(f550,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,X2,extension(X3,X2,X0,X1)),
inference(resolution,[],[f63,f30]) ).
fof(f564,plain,
! [X2,X3,X0,X1] : inner_pasch(X0,X1,extension(X0,X1,X2,X3),extension(X0,X1,X2,X3),X1) = X1,
inference(resolution,[],[f112,f53]) ).
fof(f580,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,extension(X3,X1,X1,X2))
| ~ between(X0,X1,X2)
| X0 = X1
| equidistant(X2,X4,extension(X3,X1,X1,X2),X4) ),
inference(resolution,[],[f550,f397]) ).
fof(f587,plain,
! [X2,X3,X0,X1] :
( ~ between(X1,u1,extension(X3,u1,u,X2))
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,X2)
| ~ equidistant(X0,v,X1,v1)
| u = X0
| equidistant(X2,v,extension(X3,u1,u,X2),v1) ),
inference(resolution,[],[f550,f139]) ).
fof(f588,plain,
! [X2,X3,X0,X1] :
( ~ between(X1,u1,extension(X3,u1,u,X2))
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,X2)
| ~ equidistant(X0,x,X1,x1)
| u = X0
| equidistant(X2,x,extension(X3,u1,u,X2),x1) ),
inference(resolution,[],[f550,f138]) ).
fof(f591,plain,
! [X2,X3,X0,X1] :
( ~ between(X1,w1,extension(X3,w1,w,X2))
| ~ equidistant(X0,w,X1,w1)
| ~ between(X0,w,X2)
| ~ equidistant(X0,x,X1,x1)
| w = X0
| equidistant(X2,x,extension(X3,w1,w,X2),x1) ),
inference(resolution,[],[f550,f144]) ).
fof(f595,plain,
! [X2,X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ between(X0,u,X2)
| ~ equidistant(X0,u,X1,u1)
| u = X0
| equidistant(X2,x,extension(X1,u1,u,X2),x1) ),
inference(resolution,[],[f588,f4]) ).
fof(f606,plain,
! [X0] :
( ~ between(w,u,X0)
| ~ equidistant(w,u,w1,u1)
| u = w
| equidistant(X0,x,extension(w1,u1,u,X0),x1) ),
inference(resolution,[],[f595,f22]) ).
fof(f607,plain,
! [X0] :
( ~ between(w,u,X0)
| u = w
| equidistant(X0,x,extension(w1,u1,u,X0),x1) ),
inference(forward_subsumption_resolution,[],[f606,f83]) ).
fof(f614,definition,
( spl0_50
<=> ! [X0] :
( ~ between(w,u,X0)
| equidistant(X0,x,extension(w1,u1,u,X0),x1) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f615,plain,
( ! [X0] :
( equidistant(X0,x,extension(w1,u1,u,X0),x1)
| ~ between(w,u,X0) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f616,plain,
( spl0_9
| spl0_50 ),
inference(avatar_split_clause,[],[f607,f614,f197]) ).
fof(f621,plain,
( equidistant(u,u,u1,w1)
| ~ spl0_9 ),
inference(superposition,[],[f20,f199]) ).
fof(f654,plain,
( ! [X0] : equidistant(u1,w1,X0,X0)
| ~ spl0_9 ),
inference(resolution,[],[f621,f51]) ).
fof(f664,plain,
( u1 = w1
| ~ spl0_9 ),
inference(resolution,[],[f654,f3]) ).
fof(f757,plain,
( between(u1,v1,u1)
| ~ spl0_9 ),
inference(superposition,[],[f100,f664]) ).
fof(f796,plain,
( u1 = v1
| ~ spl0_9 ),
inference(resolution,[],[f757,f7]) ).
fof(f799,plain,
( equidistant(u,v,u1,u1)
| ~ spl0_9 ),
inference(superposition,[],[f19,f796]) ).
fof(f846,plain,
( u = v
| ~ spl0_9 ),
inference(resolution,[],[f799,f3]) ).
fof(f847,plain,
( spl0_28
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f846,f197,f305]) ).
fof(f865,plain,
( ! [X0,X1] : equidistant(extension(X0,X1,u,u),X1,u1,v1)
| ~ spl0_28 ),
inference(superposition,[],[f74,f307]) ).
fof(f935,plain,
( ! [X1] : equidistant(X1,X1,u1,v1)
| ~ spl0_28 ),
inference(forward_demodulation,[],[f865,f48]) ).
fof(f938,plain,
( ! [X0] :
( ~ between(w,u,X0)
| ~ equidistant(X0,u,extension(w1,u1,u,X0),u1)
| ~ between(X0,u,v)
| ~ between(extension(w1,u1,u,X0),u1,v1)
| u = X0 )
| ~ spl0_50 ),
inference(resolution,[],[f615,f161]) ).
fof(f957,plain,
( ! [X0] :
( ~ between(extension(w1,u1,u,X0),u1,v1)
| ~ between(X0,u,v)
| ~ between(w,u,X0)
| u = X0 )
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f938,f510]) ).
fof(f965,plain,
( ! [X0] : equidistant(u1,v1,X0,X0)
| ~ spl0_28 ),
inference(resolution,[],[f935,f30]) ).
fof(f1051,plain,
! [X2,X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ between(X0,w,X2)
| ~ equidistant(X0,w,X1,w1)
| w = X0
| equidistant(X2,x,extension(X1,w1,w,X2),x1) ),
inference(resolution,[],[f591,f4]) ).
fof(f1063,plain,
! [X0] :
( ~ between(u,w,X0)
| ~ equidistant(u,w,u1,w1)
| u = w
| equidistant(X0,x,extension(u1,w1,w,X0),x1) ),
inference(resolution,[],[f1051,f21]) ).
fof(f1065,plain,
! [X0] :
( ~ between(u,w,X0)
| u = w
| equidistant(X0,x,extension(u1,w1,w,X0),x1) ),
inference(forward_subsumption_resolution,[],[f1063,f20]) ).
fof(f1071,plain,
( ! [X0] :
( equidistant(X0,x,extension(u1,w1,w,X0),x1)
| ~ between(u,w,X0) )
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1065,f198]) ).
fof(f1275,plain,
( u1 = v1
| ~ spl0_28 ),
inference(resolution,[],[f965,f3]) ).
fof(f1285,plain,
( ~ equidistant(v,x,u1,x1)
| ~ spl0_28 ),
inference(superposition,[],[f25,f1275]) ).
fof(f1336,plain,
( ~ equidistant(u,x,u1,x1)
| ~ spl0_28 ),
inference(forward_demodulation,[],[f1285,f307]) ).
fof(f1344,plain,
( $false
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1336,f21]) ).
fof(f1345,plain,
~ spl0_28,
inference(avatar_contradiction_clause,[],[f1344]) ).
fof(f1408,plain,
! [X2,X0,X1] :
( ~ equidistant(X0,v,X1,v1)
| ~ between(X0,u,X2)
| ~ equidistant(X0,u,X1,u1)
| u = X0
| equidistant(X2,v,extension(X1,u1,u,X2),v1) ),
inference(resolution,[],[f587,f4]) ).
fof(f1410,plain,
! [X0] :
( ~ between(v,u,X0)
| ~ equidistant(v,u,v1,u1)
| u = v
| equidistant(X0,v,extension(v1,u1,u,X0),v1) ),
inference(resolution,[],[f1408,f49]) ).
fof(f1418,plain,
! [X0] :
( ~ between(v,u,X0)
| u = v
| equidistant(X0,v,extension(v1,u1,u,X0),v1) ),
inference(forward_subsumption_resolution,[],[f1410,f42]) ).
fof(f1419,plain,
( ! [X0] :
( equidistant(X0,v,extension(v1,u1,u,X0),v1)
| ~ between(v,u,X0) )
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1418,f306]) ).
fof(f1421,plain,
( ! [X0] :
( ~ between(v,u,X0)
| u = X0
| ~ between(extension(v1,u1,u,X0),u1,w1)
| ~ between(X0,u,w)
| ~ equidistant(X0,u,extension(v1,u1,u,X0),u1) )
| ~ spl0_17
| spl0_28 ),
inference(resolution,[],[f1419,f238]) ).
fof(f1440,plain,
( ! [X0] :
( ~ between(extension(v1,u1,u,X0),u1,w1)
| u = X0
| ~ between(v,u,X0)
| ~ between(X0,u,w) )
| ~ spl0_17
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1421,f510]) ).
fof(f1590,plain,
! [X2,X3,X0,X1] :
( equidistant(extension(X0,X1,X1,X2),X3,X2,X3)
| X0 = X1
| ~ between(X0,X1,X2) ),
inference(resolution,[],[f401,f4]) ).
fof(f1598,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| X0 = X1
| extension(X0,X1,X1,X2) = X2 ),
inference(resolution,[],[f1590,f3]) ).
fof(f1616,definition,
( spl0_79
<=> v1 = w1 ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f1618,plain,
( v1 = w1
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1625,definition,
( spl0_81
<=> v = w ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f1627,plain,
( v = w
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1634,definition,
( spl0_83
<=> u1 = v1 ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f1636,plain,
( u1 = v1
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f1634]) ).
fof(f1786,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,f564]) ).
fof(f1787,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,[],[f1786,f53]) ).
fof(f1788,plain,
! [X2,X3,X0,X1] : between(extension(X1,X0,X2,X3),X0,X1),
inference(forward_subsumption_resolution,[],[f1787,f4]) ).
fof(f1790,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| inner_pasch(extension(X2,X0,X3,X4),X0,X2,X1,X0) = X0 ),
inference(resolution,[],[f1788,f86]) ).
fof(f1971,plain,
! [X0,X1] : u = inner_pasch(extension(w,u,X0,X1),u,w,v,u),
inference(resolution,[],[f1790,f23]) ).
fof(f1972,plain,
! [X0,X1] : u1 = inner_pasch(extension(w1,u1,X0,X1),u1,w1,v1,u1),
inference(resolution,[],[f1790,f24]) ).
fof(f1973,plain,
! [X0,X1] : w = inner_pasch(extension(u,w,X0,X1),w,u,v,w),
inference(resolution,[],[f1790,f108]) ).
fof(f1974,plain,
! [X0,X1] : w1 = inner_pasch(extension(u1,w1,X0,X1),w1,u1,v1,w1),
inference(resolution,[],[f1790,f100]) ).
fof(f1978,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,f1972]) ).
fof(f1979,plain,
! [X0,X1] :
( between(v1,u1,extension(w1,u1,X0,X1))
| ~ between(extension(w1,u1,X0,X1),u1,w1) ),
inference(forward_subsumption_resolution,[],[f1978,f24]) ).
fof(f1980,plain,
! [X0,X1] : between(v1,u1,extension(w1,u1,X0,X1)),
inference(forward_subsumption_resolution,[],[f1979,f1788]) ).
fof(f1984,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,f1971]) ).
fof(f1985,plain,
! [X0,X1] :
( between(v,u,extension(w,u,X0,X1))
| ~ between(extension(w,u,X0,X1),u,w) ),
inference(forward_subsumption_resolution,[],[f1984,f23]) ).
fof(f1986,plain,
! [X0,X1] : between(v,u,extension(w,u,X0,X1)),
inference(forward_subsumption_resolution,[],[f1985,f1788]) ).
fof(f1991,plain,
! [X0,X1] :
( ~ between(v,u,X0)
| u = v
| equidistant(extension(w,u,u,X0),X1,X0,X1) ),
inference(resolution,[],[f1986,f401]) ).
fof(f1993,plain,
! [X0,X1] :
( u = v
| extension(w,u,X0,X1) = extension(v,u,u,extension(w,u,X0,X1)) ),
inference(resolution,[],[f1986,f1598]) ).
fof(f1998,plain,
( ! [X0,X1] : extension(w,u,X0,X1) = extension(v,u,u,extension(w,u,X0,X1))
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1993,f306]) ).
fof(f1999,plain,
( ! [X0,X1] :
( equidistant(extension(w,u,u,X0),X1,X0,X1)
| ~ between(v,u,X0) )
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f1991,f306]) ).
fof(f2024,plain,
( ! [X0,X1] : between(extension(w,u,X0,X1),u,v)
| spl0_28 ),
inference(superposition,[],[f1788,f1998]) ).
fof(f2029,plain,
! [X0,X1] :
( ~ between(v1,u1,X0)
| u1 = v1
| equidistant(X0,X1,extension(w1,u1,u1,X0),X1) ),
inference(resolution,[],[f1980,f580]) ).
fof(f2032,plain,
! [X0,X1] :
( u1 = v1
| extension(w1,u1,X0,X1) = extension(v1,u1,u1,extension(w1,u1,X0,X1)) ),
inference(resolution,[],[f1980,f1598]) ).
fof(f2038,definition,
( spl0_89
<=> ! [X0,X1] : extension(w1,u1,X0,X1) = extension(v1,u1,u1,extension(w1,u1,X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f2039,plain,
( ! [X0,X1] : extension(w1,u1,X0,X1) = extension(v1,u1,u1,extension(w1,u1,X0,X1))
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f2038]) ).
fof(f2040,plain,
( spl0_89
| spl0_83 ),
inference(avatar_split_clause,[],[f2032,f1634,f2038]) ).
fof(f2046,definition,
( spl0_91
<=> ! [X0,X1] :
( ~ between(v1,u1,X0)
| equidistant(X0,X1,extension(w1,u1,u1,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f2047,plain,
( ! [X0,X1] :
( equidistant(X0,X1,extension(w1,u1,u1,X0),X1)
| ~ between(v1,u1,X0) )
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f2046]) ).
fof(f2048,plain,
( spl0_83
| spl0_91 ),
inference(avatar_split_clause,[],[f2029,f2046,f1634]) ).
fof(f2079,plain,
( ! [X0] :
( ~ between(v,u,X0)
| extension(w,u,u,X0) = X0 )
| spl0_28 ),
inference(resolution,[],[f1999,f3]) ).
fof(f2112,plain,
! [X0,X1] :
( between(v1,w1,extension(u1,w1,X0,X1))
| ~ between(w1,v1,u1)
| ~ between(extension(u1,w1,X0,X1),w1,u1) ),
inference(superposition,[],[f9,f1974]) ).
fof(f2113,plain,
! [X0,X1] :
( between(v1,w1,extension(u1,w1,X0,X1))
| ~ between(extension(u1,w1,X0,X1),w1,u1) ),
inference(forward_subsumption_resolution,[],[f2112,f100]) ).
fof(f2115,plain,
! [X0,X1] : between(v1,w1,extension(u1,w1,X0,X1)),
inference(forward_subsumption_resolution,[],[f2113,f1788]) ).
fof(f2120,plain,
! [X0,X1] :
( between(v,w,extension(u,w,X0,X1))
| ~ between(w,v,u)
| ~ between(extension(u,w,X0,X1),w,u) ),
inference(superposition,[],[f9,f1973]) ).
fof(f2121,plain,
! [X0,X1] :
( between(v,w,extension(u,w,X0,X1))
| ~ between(extension(u,w,X0,X1),w,u) ),
inference(forward_subsumption_resolution,[],[f2120,f108]) ).
fof(f2122,plain,
! [X0,X1] : between(v,w,extension(u,w,X0,X1)),
inference(forward_subsumption_resolution,[],[f2121,f1788]) ).
fof(f2124,plain,
! [X0,X1] :
( ~ between(v,w,X0)
| v = w
| equidistant(X0,X1,extension(u,w,w,X0),X1) ),
inference(resolution,[],[f2122,f580]) ).
fof(f2141,definition,
( spl0_94
<=> ! [X0,X1] :
( ~ between(v,w,X0)
| equidistant(X0,X1,extension(u,w,w,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f2142,plain,
( ! [X0,X1] :
( equidistant(X0,X1,extension(u,w,w,X0),X1)
| ~ between(v,w,X0) )
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f2141]) ).
fof(f2143,plain,
( spl0_81
| spl0_94 ),
inference(avatar_split_clause,[],[f2124,f2141,f1625]) ).
fof(f2148,plain,
( equidistant(u,w,u1,v1)
| ~ spl0_81 ),
inference(superposition,[],[f19,f1627]) ).
fof(f2150,plain,
( ~ equidistant(w,x,v1,x1)
| ~ spl0_81 ),
inference(superposition,[],[f25,f1627]) ).
fof(f2233,plain,
( ! [X0] :
( ~ between(extension(w1,u1,u,X0),u1,u1)
| ~ between(X0,u,v)
| ~ between(w,u,X0)
| u = X0 )
| ~ spl0_50
| ~ spl0_83 ),
inference(superposition,[],[f957,f1636]) ).
fof(f2234,plain,
( ! [X0] :
( ~ between(w,u,X0)
| ~ between(X0,u,v)
| u = X0 )
| ~ spl0_50
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2233,f53]) ).
fof(f2237,plain,
( ! [X0,X1] : extension(v,u,X0,X1) = extension(w,u,u,extension(v,u,X0,X1))
| spl0_28 ),
inference(resolution,[],[f2079,f4]) ).
fof(f2476,plain,
( ! [X0] :
( ~ between(v1,u1,X0)
| extension(w1,u1,u1,X0) = X0 )
| ~ spl0_91 ),
inference(resolution,[],[f2047,f3]) ).
fof(f2536,plain,
( ! [X0,X1] : between(extension(w1,u1,X0,X1),u1,v1)
| ~ spl0_89 ),
inference(superposition,[],[f1788,f2039]) ).
fof(f2553,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,w)
| ~ between(X1,u1,v1)
| u = X0
| equidistant(w,x,v1,x1) )
| ~ spl0_81 ),
inference(resolution,[],[f2148,f138]) ).
fof(f2559,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,u,X1,u1)
| ~ between(X0,u,w)
| ~ between(X1,u1,v1)
| u = X0 )
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2553,f2150]) ).
fof(f2564,plain,
( ! [X0] :
( ~ equidistant(X0,u,extension(w1,u1,u,X0),u1)
| ~ between(X0,u,w)
| ~ between(extension(w1,u1,u,X0),u1,v1)
| u = X0
| ~ between(w,u,X0) )
| ~ spl0_50
| ~ spl0_81 ),
inference(resolution,[],[f2559,f615]) ).
fof(f2581,plain,
( ! [X0] :
( ~ between(X0,u,w)
| ~ between(extension(w1,u1,u,X0),u1,v1)
| u = X0
| ~ between(w,u,X0) )
| ~ spl0_50
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2564,f510]) ).
fof(f2584,plain,
( ! [X0] :
( ~ between(w,u,X0)
| u = X0
| ~ between(X0,u,w) )
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f2581,f2536]) ).
fof(f2585,plain,
( ! [X0,X1] :
( u = extension(w,u,X0,X1)
| ~ between(extension(w,u,X0,X1),u,w) )
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(resolution,[],[f2584,f4]) ).
fof(f2587,plain,
( ! [X0,X1] : u = extension(w,u,X0,X1)
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f2585,f1788]) ).
fof(f2612,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(u,u,X2,X3)
| equidistant(X2,X3,X1,X0) )
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(superposition,[],[f492,f2587]) ).
fof(f2613,plain,
( ! [X0,X1] : equidistant(u,u,X1,X0)
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(superposition,[],[f504,f2587]) ).
fof(f2623,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X1,X0)
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(forward_subsumption_resolution,[],[f2612,f2613]) ).
fof(f2661,plain,
( $false
| ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(resolution,[],[f2623,f25]) ).
fof(f2670,plain,
( ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(avatar_contradiction_clause,[],[f2661]) ).
fof(f2709,plain,
( ! [X0] :
( ~ between(v,w,X0)
| extension(u,w,w,X0) = X0 )
| ~ spl0_94 ),
inference(resolution,[],[f2142,f3]) ).
fof(f2753,plain,
( ! [X0,X1] : between(w,u,extension(v,u,X0,X1))
| spl0_28 ),
inference(superposition,[],[f4,f2237]) ).
fof(f2768,plain,
( ! [X0,X1] : between(extension(v,u,X0,X1),u,w)
| spl0_28 ),
inference(superposition,[],[f1788,f2237]) ).
fof(f2824,plain,
( ! [X0,X1] : extension(v1,u1,X0,X1) = extension(w1,u1,u1,extension(v1,u1,X0,X1))
| ~ spl0_91 ),
inference(resolution,[],[f2476,f4]) ).
fof(f2853,plain,
( ! [X0,X1] : between(extension(v1,u1,X0,X1),u1,w1)
| ~ spl0_91 ),
inference(superposition,[],[f1788,f2824]) ).
fof(f4141,plain,
( ! [X0,X1] : extension(v,w,X0,X1) = extension(u,w,w,extension(v,w,X0,X1))
| ~ spl0_94 ),
inference(resolution,[],[f2709,f4]) ).
fof(f4155,plain,
( ! [X0,X1] : between(u,w,extension(v,w,X0,X1))
| ~ spl0_94 ),
inference(superposition,[],[f4,f4141]) ).
fof(f4612,plain,
( ! [X0,X1] :
( ~ between(extension(w,u,X0,X1),u,v)
| u = extension(w,u,X0,X1) )
| ~ spl0_50
| ~ spl0_83 ),
inference(resolution,[],[f2234,f4]) ).
fof(f4614,plain,
( ! [X0,X1] : u = extension(w,u,X0,X1)
| spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f4612,f2024]) ).
fof(f4643,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(u,u,X2,X3)
| equidistant(X2,X3,X1,X0) )
| spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(superposition,[],[f492,f4614]) ).
fof(f4644,plain,
( ! [X0,X1] : equidistant(u,u,X1,X0)
| spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(superposition,[],[f504,f4614]) ).
fof(f4657,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X1,X0)
| spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f4643,f4644]) ).
fof(f4693,plain,
( $false
| spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(resolution,[],[f4657,f25]) ).
fof(f4700,plain,
( spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f4693]) ).
fof(f5099,plain,
! [X0,X1] :
( v1 = w1
| extension(u1,w1,X0,X1) = extension(v1,w1,w1,extension(u1,w1,X0,X1)) ),
inference(resolution,[],[f2115,f1598]) ).
fof(f5105,definition,
( spl0_125
<=> ! [X0,X1] : extension(u1,w1,X0,X1) = extension(v1,w1,w1,extension(u1,w1,X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f5106,plain,
( ! [X0,X1] : extension(u1,w1,X0,X1) = extension(v1,w1,w1,extension(u1,w1,X0,X1))
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f5105]) ).
fof(f5107,plain,
( spl0_125
| spl0_79 ),
inference(avatar_split_clause,[],[f5099,f1616,f5105]) ).
fof(f5133,plain,
( ! [X0] :
( ~ between(extension(w1,u1,u,X0),u1,w1)
| ~ between(X0,u,v)
| ~ between(w,u,X0)
| u = X0 )
| ~ spl0_50
| ~ spl0_79 ),
inference(superposition,[],[f957,f1618]) ).
fof(f5158,plain,
( ! [X0] :
( ~ between(w,u,X0)
| ~ between(X0,u,v)
| u = X0 )
| ~ spl0_50
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f5133,f1788]) ).
fof(f5451,plain,
( ! [X0,X1] :
( ~ between(extension(v,u,X0,X1),u,v)
| u = extension(v,u,X0,X1) )
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(resolution,[],[f5158,f2753]) ).
fof(f5455,plain,
( ! [X0,X1] : u = extension(v,u,X0,X1)
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f5451,f1788]) ).
fof(f5479,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(u,u,X2,X3)
| equidistant(X2,X3,X1,X0) )
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(superposition,[],[f492,f5455]) ).
fof(f5480,plain,
( ! [X0,X1] : equidistant(u,u,X1,X0)
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(superposition,[],[f504,f5455]) ).
fof(f5491,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X1,X0)
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f5479,f5480]) ).
fof(f5528,plain,
( $false
| spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(resolution,[],[f5491,f25]) ).
fof(f5537,plain,
( spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f5528]) ).
fof(f5564,plain,
( ! [X0,X1] : between(extension(u1,w1,X0,X1),w1,v1)
| ~ spl0_125 ),
inference(superposition,[],[f1788,f5106]) ).
fof(f7741,plain,
( ! [X0] :
( ~ between(v,u,X0)
| u = X0
| ~ between(X0,u,w) )
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(resolution,[],[f1440,f2853]) ).
fof(f7743,plain,
( ! [X0,X1] :
( u = extension(v,u,X0,X1)
| ~ between(extension(v,u,X0,X1),u,w) )
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(resolution,[],[f7741,f4]) ).
fof(f7746,plain,
( ! [X0,X1] : u = extension(v,u,X0,X1)
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(forward_subsumption_resolution,[],[f7743,f2768]) ).
fof(f7779,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(u,u,X2,X3)
| equidistant(X2,X3,X1,X0) )
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(superposition,[],[f492,f7746]) ).
fof(f7780,plain,
( ! [X0,X1] : equidistant(u,u,X1,X0)
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(superposition,[],[f504,f7746]) ).
fof(f7800,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X1,X0)
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(forward_subsumption_resolution,[],[f7779,f7780]) ).
fof(f7839,plain,
( $false
| ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(resolution,[],[f7800,f25]) ).
fof(f7848,plain,
( ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(avatar_contradiction_clause,[],[f7839]) ).
fof(f7857,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,w,X1,w1)
| ~ between(X0,w,v)
| ~ between(X1,w1,v1)
| w = X0
| equidistant(v,x,v1,x1) )
| ~ spl0_16 ),
inference(resolution,[],[f235,f144]) ).
fof(f7867,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,x1)
| ~ equidistant(X0,w,X1,w1)
| ~ between(X0,w,v)
| ~ between(X1,w1,v1)
| w = X0 )
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f7857,f25]) ).
fof(f7874,plain,
( ! [X0] :
( ~ equidistant(X0,w,extension(u1,w1,w,X0),w1)
| ~ between(X0,w,v)
| ~ between(extension(u1,w1,w,X0),w1,v1)
| w = X0
| ~ between(u,w,X0) )
| spl0_9
| ~ spl0_16 ),
inference(resolution,[],[f7867,f1071]) ).
fof(f7895,plain,
( ! [X0] :
( ~ between(X0,w,v)
| ~ between(extension(u1,w1,w,X0),w1,v1)
| w = X0
| ~ between(u,w,X0) )
| spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f7874,f510]) ).
fof(f7899,plain,
( ! [X0] :
( ~ between(u,w,X0)
| w = X0
| ~ between(X0,w,v) )
| spl0_9
| ~ spl0_16
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f7895,f5564]) ).
fof(f7912,plain,
( ! [X0,X1] :
( w = extension(v,w,X0,X1)
| ~ between(extension(v,w,X0,X1),w,v) )
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(resolution,[],[f7899,f4155]) ).
fof(f7917,plain,
( ! [X0,X1] : w = extension(v,w,X0,X1)
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f7912,f1788]) ).
fof(f7953,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(w,w,X2,X3)
| equidistant(X2,X3,X1,X0) )
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(superposition,[],[f492,f7917]) ).
fof(f7954,plain,
( ! [X0,X1] : equidistant(w,w,X1,X0)
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(superposition,[],[f504,f7917]) ).
fof(f7974,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X1,X0)
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f7953,f7954]) ).
fof(f8011,plain,
( $false
| spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(resolution,[],[f7974,f25]) ).
fof(f8018,plain,
( spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f8011]) ).
cnf(s7,plain,
( spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f239]) ).
cnf(s24,plain,
( spl0_9
| spl0_50 ),
inference(sat_conversion,[],[f616]) ).
cnf(s27,plain,
( ~ spl0_9
| spl0_28 ),
inference(sat_conversion,[],[f847]) ).
cnf(s46,plain,
~ spl0_28,
inference(sat_conversion,[],[f1345]) ).
cnf(s61,plain,
( spl0_83
| spl0_89 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s63,plain,
( spl0_83
| spl0_91 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s66,plain,
( spl0_81
| spl0_94 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s81,plain,
( ~ spl0_50
| ~ spl0_81
| ~ spl0_89 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s125,plain,
( spl0_28
| ~ spl0_50
| ~ spl0_83 ),
inference(sat_conversion,[],[f4700]) ).
cnf(s142,plain,
( spl0_79
| spl0_125 ),
inference(sat_conversion,[],[f5107]) ).
cnf(s149,plain,
( spl0_28
| ~ spl0_50
| ~ spl0_79 ),
inference(sat_conversion,[],[f5537]) ).
cnf(s166,plain,
( ~ spl0_17
| spl0_28
| ~ spl0_91 ),
inference(sat_conversion,[],[f7848]) ).
cnf(s170,plain,
( spl0_9
| ~ spl0_16
| ~ spl0_94
| ~ spl0_125 ),
inference(sat_conversion,[],[f8018]) ).
cnf(s173,plain,
~ spl0_9,
inference(rat,[],[s27,s46]) ).
cnf(s176,plain,
spl0_50,
inference(rat,[],[s24,s173]) ).
cnf(s177,plain,
~ spl0_79,
inference(rat,[],[s149,s46,s176]) ).
cnf(s178,plain,
~ spl0_83,
inference(rat,[],[s125,s46,s176]) ).
cnf(s181,plain,
spl0_125,
inference(rat,[],[s142,s177]) ).
cnf(s183,plain,
spl0_91,
inference(rat,[],[s63,s178]) ).
cnf(s185,plain,
spl0_89,
inference(rat,[],[s61,s178]) ).
cnf(s189,plain,
~ spl0_17,
inference(rat,[],[s166,s46,s183]) ).
cnf(s190,plain,
~ spl0_81,
inference(rat,[],[s81,s176,s185]) ).
cnf(s192,plain,
spl0_94,
inference(rat,[],[s66,s190]) ).
cnf(s196,plain,
~ spl0_16,
inference(rat,[],[s170,s181,s173,s192]) ).
cnf(s201,plain,
$false,
inference(rat,[],[s7,s189,s196]) ).
fof(f8023,plain,
$false,
inference(avatar_sat_refutation,[],[s201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO031-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.10/0.44 % Computer : n016.cluster.edu
% 0.10/0.44 % Model : x86_64 x86_64
% 0.10/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.44 % Memory : 8046.5625MB
% 0.10/0.44 % OS : Linux 6.8.0-71-generic
% 0.10/0.45 % CPULimit : 300
% 0.10/0.45 % WCLimit : 300
% 0.10/0.45 % DateTime : Sun Sep 27 06:43:32 UTC 2026
% 0.10/0.45 % CPUTime :
% 0.10/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.47 Running first-order theorem proving
% 0.15/0.47 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.34/2.28 % (2272925)Input is clausal, will run a generic CNF schedule.
% 9.34/2.28 % (2272934)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3499445703:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.34/2.28 % (2272934)Instruction limit reached!
% 9.34/2.28 % (2272934)------------------------------
% 9.34/2.28 % (2272934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.28 % (2272934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.28 % (2272934)CaDiCaL version: 2.1.3
% 9.34/2.28 % (2272934)Termination reason: Instruction limit
% 9.34/2.28 % (2272934)Termination phase: Saturation
% 9.34/2.28 % (2272934)Time elapsed: 0.025 s
% 9.34/2.28 % (2272934)Peak memory usage: 87 MB
% 9.34/2.28 % (2272934)Instructions burned: 117 (million)
% 9.34/2.28 % (2272931)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3472677393:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.34/2.28 % (2272932)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3233445443:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.34/2.28 % (2272930)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=3187366584:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.34/2.28 % (2272933)lrs+10_1_sil=8000:sp=occurrence:random_seed=1499336201:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.34/2.28 % (2272933)Refutation not found, incomplete strategy
% 9.34/2.28 % (2272933)------------------------------
% 9.34/2.28 % (2272933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.28 % (2272933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.28 % (2272933)CaDiCaL version: 2.1.3
% 9.34/2.28 % (2272933)Termination reason: Refutation not found, incomplete strategy
% 9.34/2.28 % (2272933)Time elapsed: 0.004 s
% 9.34/2.28 % (2272933)Peak memory usage: 87 MB
% 9.34/2.28 % (2272933)Instructions burned: 5 (million)
% 9.34/2.28 % (2272936)dis-21_1_sil=8000:lcm=predicate:random_seed=2380032998: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.34/2.28 % (2272935)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1324774127:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.34/2.28 % (2272936)Instruction limit reached!
% 9.34/2.28 % (2272936)------------------------------
% 9.34/2.28 % (2272936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.28 % (2272936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.28 % (2272936)CaDiCaL version: 2.1.3
% 9.34/2.28 % (2272936)Termination reason: Instruction limit
% 9.34/2.28 % (2272936)Termination phase: Saturation
% 9.34/2.28 % (2272936)Time elapsed: 0.067 s
% 9.34/2.28 % (2272936)Peak memory usage: 88 MB
% 9.34/2.28 % (2272936)Instructions burned: 119 (million)
% 9.34/2.28 % (2272938)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=3471474853:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.34/2.28 % (2272935)Instruction limit reached!
% 9.34/2.28 % (2272935)------------------------------
% 9.34/2.28 % (2272935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.28 % (2272935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.28 % (2272935)CaDiCaL version: 2.1.3
% 9.34/2.28 % (2272935)Termination reason: Instruction limit
% 9.34/2.28 % (2272935)Termination phase: Saturation
% 9.34/2.28 % (2272935)Time elapsed: 0.119 s
% 9.34/2.28 % (2272935)Peak memory usage: 89 MB
% 9.34/2.28 % (2272935)Instructions burned: 180 (million)
% 9.34/2.28 % (2272938)Instruction limit reached!
% 9.34/2.28 % (2272938)------------------------------
% 9.34/2.28 % (2272938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.34/2.28 % (2272938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.34/2.28 % (2272938)CaDiCaL version: 2.1.3
% 9.34/2.28 % (2272938)Termination reason: Instruction limit
% 9.34/2.28 % (2272938)Termination phase: Saturation
% 9.34/2.28 % (2272938)Time elapsed: 0.056 s
% 9.34/2.28 % (2272938)Peak memory usage: 89 MB
% 9.34/2.28 % (2272938)Instructions burned: 143 (million)
% 9.34/2.28 % (2272933)------------------------------
% 12.48/2.79 % (2272933)------------------------------
% 12.48/2.79 % (2272945)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1123614419: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)
% 12.48/2.79 % (2272947)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3219455116:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.48/2.79 % (2272948)lrs+10_64_to=lpo:sil=8000:random_seed=1708482613:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 12.48/2.79 % (2272948)Instruction limit reached!
% 12.48/2.79 % (2272948)------------------------------
% 12.48/2.79 % (2272948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272948)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272948)Termination reason: Instruction limit
% 12.48/2.79 % (2272948)Termination phase: Saturation
% 12.48/2.79 % (2272948)Time elapsed: 0.044 s
% 12.48/2.79 % (2272948)Peak memory usage: 89 MB
% 12.48/2.79 % (2272948)Instructions burned: 129 (million)
% 12.48/2.79 % (2272945)Instruction limit reached!
% 12.48/2.79 % (2272945)------------------------------
% 12.48/2.79 % (2272945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272945)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272945)Termination reason: Instruction limit
% 12.48/2.79 % (2272945)Termination phase: Saturation
% 12.48/2.79 % (2272945)Time elapsed: 0.104 s
% 12.48/2.79 % (2272945)Peak memory usage: 89 MB
% 12.48/2.79 % (2272945)Instructions burned: 191 (million)
% 12.48/2.79 % (2272947)Instruction limit reached!
% 12.48/2.79 % (2272947)------------------------------
% 12.48/2.79 % (2272947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272947)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272947)Termination reason: Instruction limit
% 12.48/2.79 % (2272947)Termination phase: Saturation
% 12.48/2.79 % (2272947)Time elapsed: 0.117 s
% 12.48/2.79 % (2272947)Peak memory usage: 89 MB
% 12.48/2.79 % (2272947)Instructions burned: 219 (million)
% 12.48/2.79 % (2272950)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3909602081:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 12.48/2.79 % (2272953)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2118744684:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.48/2.79 % (2272953)Instruction limit reached!
% 12.48/2.79 % (2272953)------------------------------
% 12.48/2.79 % (2272953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272953)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272953)Termination reason: Instruction limit
% 12.48/2.79 % (2272953)Termination phase: Saturation
% 12.48/2.79 % (2272953)Time elapsed: 0.058 s
% 12.48/2.79 % (2272953)Peak memory usage: 90 MB
% 12.48/2.79 % (2272953)Instructions burned: 158 (million)
% 12.48/2.79 % (2272954)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=253657335:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 12.48/2.79 % (2272950)Instruction limit reached!
% 12.48/2.79 % (2272950)------------------------------
% 12.48/2.79 % (2272950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272950)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272950)Termination reason: Instruction limit
% 12.48/2.79 % (2272950)Termination phase: Saturation
% 12.48/2.79 % (2272950)Time elapsed: 0.116 s
% 12.48/2.79 % (2272950)Peak memory usage: 89 MB
% 12.48/2.79 % (2272950)Instructions burned: 195 (million)
% 12.48/2.79 % (2272956)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=1070171974:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 12.48/2.79 % (2272958)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1594445008:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 12.48/2.79 % (2272956)Instruction limit reached!
% 12.48/2.79 % (2272956)------------------------------
% 12.48/2.79 % (2272956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272956)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272956)Termination reason: Instruction limit
% 12.48/2.79 % (2272956)Termination phase: Saturation
% 12.48/2.79 % (2272956)Time elapsed: 0.060 s
% 12.48/2.79 % (2272956)Peak memory usage: 88 MB
% 12.48/2.79 % (2272956)Instructions burned: 106 (million)
% 12.48/2.79 % (2272958)Instruction limit reached!
% 12.48/2.79 % (2272958)------------------------------
% 12.48/2.79 % (2272958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272958)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272958)Termination reason: Instruction limit
% 12.48/2.79 % (2272958)Termination phase: Saturation
% 12.48/2.79 % (2272958)Time elapsed: 0.041 s
% 12.48/2.79 % (2272958)Peak memory usage: 89 MB
% 12.48/2.79 % (2272958)Instructions burned: 109 (million)
% 12.48/2.79 % (2272960)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3982234405:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 12.48/2.79 % (2272960)Instruction limit reached!
% 12.48/2.79 % (2272960)------------------------------
% 12.48/2.79 % (2272960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272960)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272960)Termination reason: Instruction limit
% 12.48/2.79 % (2272960)Termination phase: Saturation
% 12.48/2.79 % (2272960)Time elapsed: 0.089 s
% 12.48/2.79 % (2272960)Peak memory usage: 88 MB
% 12.48/2.79 % (2272960)Instructions burned: 244 (million)
% 12.48/2.79 % (2272963)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=387909950:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 12.48/2.79 % (2272964)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4272431038:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 12.48/2.79 % (2272964)Instruction limit reached!
% 12.48/2.79 % (2272964)------------------------------
% 12.48/2.79 % (2272964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272964)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272964)Termination reason: Instruction limit
% 12.48/2.79 % (2272964)Termination phase: Saturation
% 12.48/2.79 % (2272964)Time elapsed: 0.048 s
% 12.48/2.79 % (2272964)Peak memory usage: 89 MB
% 12.48/2.79 % (2272964)Instructions burned: 135 (million)
% 12.48/2.79 % (2272967)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4066031504:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 12.48/2.79 % (2272969)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1867342728:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 12.48/2.79 % (2272969)Instruction limit reached!
% 12.48/2.79 % (2272969)------------------------------
% 12.48/2.79 % (2272969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272969)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272969)Termination reason: Instruction limit
% 12.48/2.79 % (2272969)Termination phase: Saturation
% 12.48/2.79 % (2272969)Time elapsed: 0.071 s
% 12.48/2.79 % (2272969)Peak memory usage: 92 MB
% 12.48/2.79 % (2272969)Instructions burned: 192 (million)
% 12.48/2.79 % (2272972)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4004626980:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 12.48/2.79 % (2272967)Instruction limit reached!
% 12.48/2.79 % (2272967)------------------------------
% 12.48/2.79 % (2272967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272967)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272967)Termination reason: Instruction limit
% 12.48/2.79 % (2272967)Termination phase: Saturation
% 12.48/2.79 % (2272967)Time elapsed: 0.288 s
% 12.48/2.79 % (2272967)Peak memory usage: 91 MB
% 12.48/2.79 % (2272967)Instructions burned: 501 (million)
% 12.48/2.79 % (2272972)Instruction limit reached!
% 12.48/2.79 % (2272972)------------------------------
% 12.48/2.79 % (2272972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272972)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272972)Termination reason: Instruction limit
% 12.48/2.79 % (2272972)Termination phase: Saturation
% 12.48/2.79 % (2272972)Time elapsed: 0.089 s
% 12.48/2.79 % (2272972)Peak memory usage: 91 MB
% 12.48/2.79 % (2272972)Instructions burned: 267 (million)
% 12.48/2.79 % (2272975)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=3595964642:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 12.48/2.79 % (2272974)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3081556972:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 12.48/2.79 % (2272930)First to succeed.
% 12.48/2.79 % (2272930)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2272925"
% 12.48/2.79 % (2272974)Instruction limit reached!
% 12.48/2.79 % (2272974)------------------------------
% 12.48/2.79 % (2272974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.48/2.79 % (2272974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.48/2.79 % (2272974)CaDiCaL version: 2.1.3
% 12.48/2.79 % (2272974)Termination reason: Instruction limit
% 12.48/2.79 % (2272974)Termination phase: Saturation
% 12.48/2.79 % (2272974)Time elapsed: 0.106 s
% 12.48/2.79 % (2272974)Peak memory usage: 88 MB
% 12.48/2.79 % (2272974)Instructions burned: 157 (million)
% 12.48/2.79 % (2272978)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1194683413:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 12.48/2.79 % (2272930)Refutation found. Thanks to Tanya!
% 12.48/2.79 % SZS status Unsatisfiable for theBenchmark
% 12.48/2.79 % SZS output start Proof for theBenchmark
% See solution above
% 13.63/2.88 % (2272930)------------------------------
% 13.63/2.88 % (2272930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.88 % (2272930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.88 % (2272930)CaDiCaL version: 2.1.3
% 13.63/2.88 % (2272930)Termination reason: Refutation
% 13.63/2.88 % (2272930)Time elapsed: 1.445 s
% 13.63/2.88 % (2272930)Peak memory usage: 137 MB
% 13.63/2.88 % (2272930)Instructions burned: 2118 (million)
% 13.63/2.88 % (2272930)------------------------------
% 13.63/2.88 % (2272930)------------------------------
% 13.63/2.88 % (2272925)Success in time 1.869 s
% 13.63/2.88 % Vampire exiting
%------------------------------------------------------------------------------