%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO070-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:51:26 AM UTC 2026
% Result : Unsatisfiable 22.38s 4.30s
% Output : Refutation 23.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 56
% Syntax : Number of formulae : 339 ( 57 unt; 32 def)
% Number of atoms : 815 ( 36 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 881 ( 405 ~; 444 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 33 prp; 0-4 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 83 ( 0 sgn 83 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : equidistant(X0,X1,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| between(X0,X1,X2)
| between(X1,X2,X0)
| between(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',colinearity4) ).
fof(f26,axiom,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2) ).
fof(f27,axiom,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X1,X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3) ).
fof(f28,axiom,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_1) ).
fof(f29,axiom,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X1,X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_2) ).
fof(f56,axiom,
! [X0,X1] : between(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3) ).
fof(f58,axiom,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| between(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1) ).
fof(f59,axiom,
! [X0,X1] : between(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2) ).
fof(f60,axiom,
! [X2,X0,X1] :
( ~ between(X1,X0,X2)
| ~ between(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b2) ).
fof(f61,axiom,
! [X2,X0,X1] :
( ~ between(X0,X2,X1)
| ~ between(X0,X1,X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b3) ).
fof(f62,axiom,
! [X2,X0,X1] :
( ~ between(X1,X0,X2)
| ~ between(X0,X1,X2)
| X0 = X1
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_1) ).
fof(f67,axiom,
! [X2,X3,X0,X1] :
( ~ between(X1,X2,X3)
| ~ between(X0,X1,X2)
| between(X0,X1,X3)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b7) ).
fof(f89,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X1,X2,X3)
| ~ equidistant(X0,X4,X2,X5)
| ~ between(X0,X1,X4)
| between(X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b11) ).
fof(f100,axiom,
! [X2,X0,X1] :
( ~ colinear(X0,X1,X2)
| colinear(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_1) ).
fof(f110,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X1,X2,X3)
| ~ equidistant(X0,X4,X2,X5)
| ~ colinear(X0,X1,X4)
| colinear(X2,X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c4) ).
fof(f118,axiom,
equidistant(u,v,w,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_w_to_x) ).
fof(f119,axiom,
equidistant(v,w,x,u),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_to_w_equals_x_to_u) ).
fof(f120,axiom,
equidistant(u,w,v,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_w_equals_v_to_x) ).
fof(f121,axiom,
between(u,y,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',y_between_u_and_w) ).
fof(f122,axiom,
between(v,y,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',y_between_v_and_x) ).
fof(f123,axiom,
u != v,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_not_v) ).
fof(f124,axiom,
x != u,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_not_u) ).
fof(f125,plain,
u != x,
inference(reorient_equations,[],[f124]) ).
fof(f126,negated_conjecture,
colinear(u,v,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_uvw_not_colinear) ).
fof(f144,plain,
between(w,y,u),
inference(resolution,[],[f58,f121]) ).
fof(f145,plain,
between(x,y,v),
inference(resolution,[],[f58,f122]) ).
fof(f150,definition,
( spl0_1
<=> between(w,u,v) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f151,plain,
( ~ between(w,u,v)
| spl0_1 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f152,plain,
( between(w,u,v)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f154,definition,
( spl0_2
<=> between(v,w,u) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f155,plain,
( ~ between(v,w,u)
| spl0_2 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f156,plain,
( between(v,w,u)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f162,plain,
! [X0,X1] :
( ~ equidistant(X0,w,X1,u)
| ~ equidistant(X0,v,X1,x)
| ~ colinear(X0,v,w)
| colinear(X1,x,u) ),
inference(resolution,[],[f110,f119]) ).
fof(f173,plain,
colinear(w,v,u),
inference(resolution,[],[f100,f126]) ).
fof(f178,plain,
( between(w,v,u)
| between(v,u,w)
| between(u,w,v) ),
inference(resolution,[],[f173,f22]) ).
fof(f180,definition,
( spl0_4
<=> between(u,w,v) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f182,plain,
( between(u,w,v)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_5
<=> between(v,u,w) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f185,plain,
( ~ between(v,u,w)
| spl0_5 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( between(v,u,w)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_6
<=> between(w,v,u) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f190,plain,
( between(w,v,u)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f178,f188,f184,f180]) ).
fof(f206,plain,
! [X0,X1] :
( ~ equidistant(X0,w,X1,u)
| ~ equidistant(X0,v,X1,x)
| ~ between(X0,v,w)
| between(X1,x,u) ),
inference(resolution,[],[f89,f119]) ).
fof(f208,plain,
! [X0,X1] :
( ~ equidistant(X0,v,X1,x)
| ~ equidistant(X0,u,X1,w)
| ~ between(X0,u,v)
| between(X1,w,x) ),
inference(resolution,[],[f89,f118]) ).
fof(f213,plain,
( between(v,w,u)
| ~ spl0_4 ),
inference(resolution,[],[f182,f58]) ).
fof(f214,plain,
( between(u,w,v)
| ~ spl0_2 ),
inference(resolution,[],[f156,f58]) ).
fof(f216,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X3,X2,X1)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X0,X1,X3)
| between(X2,X3,X1) ),
inference(resolution,[],[f1,f89]) ).
fof(f219,plain,
( ~ equidistant(u,v,w,x)
| ~ colinear(u,v,w)
| colinear(w,x,u) ),
inference(resolution,[],[f1,f162]) ).
fof(f233,definition,
( spl0_9
<=> equidistant(x,u,v,w) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f234,plain,
( equidistant(x,u,v,w)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( ~ equidistant(x,u,v,w)
| spl0_9 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f238,definition,
( spl0_10
<=> between(v,w,x) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f239,plain,
( ~ between(v,w,x)
| spl0_10 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( between(v,w,x)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f255,definition,
( spl0_14
<=> equidistant(x,u,w,v) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f256,plain,
( equidistant(x,u,w,v)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f257,plain,
( ~ equidistant(x,u,w,v)
| spl0_14 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f264,definition,
( spl0_16
<=> between(x,u,w) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f265,plain,
( between(x,u,w)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f268,plain,
( ~ colinear(u,v,w)
| colinear(w,x,u) ),
inference(forward_subsumption_resolution,[],[f219,f118]) ).
fof(f270,plain,
colinear(w,x,u),
inference(forward_subsumption_resolution,[],[f268,f126]) ).
fof(f272,definition,
( spl0_17
<=> between(w,x,u) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f274,plain,
( between(w,x,u)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f281,plain,
( between(w,x,u)
| between(x,u,w)
| between(u,w,x) ),
inference(resolution,[],[f270,f22]) ).
fof(f283,definition,
( spl0_18
<=> between(u,w,x) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f285,plain,
( between(u,w,x)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( spl0_18
| spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f281,f272,f264,f283]) ).
fof(f295,definition,
( spl0_19
<=> between(u,x,w) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f297,plain,
( between(u,x,w)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl0_20
<=> between(w,u,x) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f300,plain,
( ~ between(w,u,x)
| spl0_20 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( between(w,u,x)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f313,plain,
( between(w,x,u)
| ~ spl0_19 ),
inference(resolution,[],[f297,f58]) ).
fof(f314,plain,
( spl0_17
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f313,f295,f272]) ).
fof(f315,plain,
( between(u,x,w)
| ~ spl0_17 ),
inference(resolution,[],[f274,f58]) ).
fof(f364,definition,
( spl0_27
<=> equidistant(w,u,x,v) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f365,plain,
( equidistant(w,u,x,v)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( ~ equidistant(w,u,x,v)
| spl0_27 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f377,definition,
( spl0_30
<=> equidistant(w,v,u,x) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f378,plain,
( equidistant(w,v,u,x)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f385,plain,
( between(w,u,x)
| ~ spl0_16 ),
inference(resolution,[],[f265,f58]) ).
fof(f386,plain,
( spl0_20
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f385,f264,f299]) ).
fof(f557,definition,
( spl0_32
<=> equidistant(u,x,w,v) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f558,plain,
( equidistant(u,x,w,v)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f559,plain,
( ~ equidistant(u,x,w,v)
| spl0_32 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f563,definition,
( spl0_33
<=> equidistant(u,x,v,w) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f564,plain,
( equidistant(u,x,v,w)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f565,plain,
( ~ equidistant(u,x,v,w)
| spl0_33 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f588,plain,
( ~ between(w,u,v)
| u = w
| ~ spl0_4 ),
inference(resolution,[],[f60,f182]) ).
fof(f615,definition,
( spl0_38
<=> v = y ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f617,plain,
( v = y
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f624,definition,
( spl0_40
<=> u = y ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f626,plain,
( u = y
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f638,definition,
( spl0_43
<=> v = w ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f640,plain,
( v = w
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f643,definition,
( spl0_44
<=> u = w ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f644,plain,
( u != w
| spl0_44 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( u = w
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( spl0_44
| ~ spl0_1
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f588,f180,f150,f643]) ).
fof(f657,plain,
( ~ between(w,u,y)
| u = y ),
inference(resolution,[],[f61,f144]) ).
fof(f658,plain,
( ~ between(x,v,y)
| v = y ),
inference(resolution,[],[f61,f145]) ).
fof(f660,definition,
( spl0_45
<=> between(x,v,y) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f662,plain,
( ~ between(x,v,y)
| spl0_45 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( spl0_38
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f658,f660,f615]) ).
fof(f665,definition,
( spl0_46
<=> between(w,u,y) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f667,plain,
( ~ between(w,u,y)
| spl0_46 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f668,plain,
( spl0_40
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f657,f665,f624]) ).
fof(f721,definition,
( spl0_49
<=> equidistant(x,w,v,u) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f722,plain,
( ~ equidistant(x,w,v,u)
| spl0_49 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f723,plain,
( equidistant(x,w,v,u)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f725,definition,
( spl0_50
<=> between(v,x,w) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f726,plain,
( between(v,x,w)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f729,definition,
( spl0_51
<=> between(x,v,u) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f730,plain,
( between(x,v,u)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f731,plain,
( ~ between(x,v,u)
| spl0_51 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f745,plain,
equidistant(w,x,u,v),
inference(resolution,[],[f26,f118]) ).
fof(f746,plain,
equidistant(x,u,v,w),
inference(resolution,[],[f26,f119]) ).
fof(f747,plain,
equidistant(v,x,u,w),
inference(resolution,[],[f26,f120]) ).
fof(f748,plain,
( $false
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f746,f235]) ).
fof(f749,plain,
spl0_9,
inference(avatar_contradiction_clause,[],[f748]) ).
fof(f752,plain,
( ~ equidistant(v,w,u,x)
| ~ between(v,w,x)
| between(u,x,w) ),
inference(resolution,[],[f747,f216]) ).
fof(f758,plain,
! [X0,X1] :
( ~ equidistant(X0,x,X1,v)
| ~ equidistant(X0,w,X1,u)
| ~ between(X0,w,x)
| between(X1,u,v) ),
inference(resolution,[],[f745,f89]) ).
fof(f765,definition,
( spl0_52
<=> equidistant(x,v,w,u) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f766,plain,
( equidistant(x,v,w,u)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f791,plain,
( equidistant(u,x,v,w)
| ~ spl0_9 ),
inference(resolution,[],[f27,f234]) ).
fof(f792,plain,
equidistant(v,u,w,x),
inference(resolution,[],[f27,f118]) ).
fof(f794,plain,
equidistant(w,u,v,x),
inference(resolution,[],[f27,f120]) ).
fof(f798,plain,
( $false
| ~ spl0_9
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f791,f565]) ).
fof(f799,plain,
( ~ spl0_9
| spl0_33 ),
inference(avatar_contradiction_clause,[],[f798]) ).
fof(f801,plain,
equidistant(w,x,v,u),
inference(resolution,[],[f792,f26]) ).
fof(f803,plain,
( ~ equidistant(v,x,w,u)
| ~ between(v,x,u)
| between(w,u,x) ),
inference(resolution,[],[f792,f216]) ).
fof(f804,plain,
! [X0,X1] :
( ~ equidistant(X0,v,X1,w)
| ~ equidistant(X0,u,X1,x)
| ~ between(X0,v,u)
| between(X1,w,x) ),
inference(resolution,[],[f792,f89]) ).
fof(f806,plain,
( ~ equidistant(v,x,w,u)
| ~ between(v,x,u)
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f803,f300]) ).
fof(f808,definition,
( spl0_54
<=> between(v,x,u) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f809,plain,
( between(v,x,u)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f810,plain,
( ~ between(v,x,u)
| spl0_54 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f812,definition,
( spl0_55
<=> equidistant(v,x,w,u) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f813,plain,
( equidistant(v,x,w,u)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f815,plain,
( ~ spl0_54
| ~ spl0_55
| spl0_20 ),
inference(avatar_split_clause,[],[f806,f299,f812,f808]) ).
fof(f817,plain,
equidistant(v,x,w,u),
inference(resolution,[],[f794,f26]) ).
fof(f819,plain,
( ~ equidistant(w,x,v,u)
| ~ between(w,x,u)
| between(v,u,x) ),
inference(resolution,[],[f794,f216]) ).
fof(f822,plain,
( ~ between(w,x,u)
| between(v,u,x) ),
inference(forward_subsumption_resolution,[],[f819,f801]) ).
fof(f823,plain,
spl0_55,
inference(avatar_split_clause,[],[f817,f812]) ).
fof(f824,plain,
( between(v,u,x)
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f822,f274]) ).
fof(f863,definition,
( spl0_56
<=> between(x,v,w) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f864,plain,
( between(x,v,w)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f865,plain,
( ~ between(x,v,w)
| spl0_56 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f875,plain,
( equidistant(v,w,u,x)
| ~ spl0_33 ),
inference(resolution,[],[f564,f26]) ).
fof(f878,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,w)
| ~ equidistant(X0,u,X1,v)
| ~ between(X0,u,x)
| between(X1,v,w) )
| ~ spl0_33 ),
inference(resolution,[],[f564,f89]) ).
fof(f883,plain,
( ~ equidistant(w,u,v,x)
| ~ between(w,v,u)
| between(v,w,x) ),
inference(resolution,[],[f804,f1]) ).
fof(f891,plain,
( ~ between(v,w,x)
| between(u,x,w)
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f752,f875]) ).
fof(f894,plain,
( between(u,x,w)
| ~ spl0_10
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f891,f240]) ).
fof(f992,plain,
( $false
| spl0_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f213,f155]) ).
fof(f993,plain,
( spl0_2
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f1060,plain,
( equidistant(x,v,w,u)
| ~ spl0_55 ),
inference(resolution,[],[f813,f27]) ).
fof(f1066,plain,
( spl0_52
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1060,f812,f765]) ).
fof(f1071,plain,
( equidistant(x,u,w,v)
| ~ spl0_9 ),
inference(resolution,[],[f28,f234]) ).
fof(f1073,plain,
equidistant(w,u,x,v),
inference(resolution,[],[f28,f794]) ).
fof(f1074,plain,
equidistant(u,v,x,w),
inference(resolution,[],[f28,f118]) ).
fof(f1079,plain,
( equidistant(u,x,w,v)
| ~ spl0_33 ),
inference(resolution,[],[f28,f564]) ).
fof(f1081,plain,
( $false
| spl0_32
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1079,f559]) ).
fof(f1082,plain,
( spl0_32
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1081]) ).
fof(f1083,plain,
( $false
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f1073,f366]) ).
fof(f1084,plain,
spl0_27,
inference(avatar_contradiction_clause,[],[f1083]) ).
fof(f1086,plain,
( $false
| ~ spl0_9
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1071,f257]) ).
fof(f1087,plain,
( ~ spl0_9
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f1086]) ).
fof(f1103,plain,
! [X0,X1] :
( ~ equidistant(X0,v,X1,w)
| ~ equidistant(X0,u,X1,x)
| ~ between(X0,u,v)
| between(X1,x,w) ),
inference(resolution,[],[f1074,f89]) ).
fof(f1113,plain,
( ~ equidistant(u,w,w,u)
| ~ between(u,w,x)
| between(w,u,v)
| ~ spl0_32 ),
inference(resolution,[],[f558,f758]) ).
fof(f1123,plain,
( ~ equidistant(w,u,v,x)
| ~ between(w,u,v)
| between(v,x,w) ),
inference(resolution,[],[f1103,f1]) ).
fof(f1133,plain,
( ~ equidistant(x,v,w,u)
| ~ between(x,v,u)
| between(w,u,v)
| ~ spl0_14 ),
inference(resolution,[],[f256,f216]) ).
fof(f1144,plain,
equidistant(w,v,u,x),
inference(resolution,[],[f29,f119]) ).
fof(f1148,plain,
equidistant(x,w,v,u),
inference(resolution,[],[f29,f745]) ).
fof(f1152,plain,
( $false
| spl0_49 ),
inference(forward_subsumption_resolution,[],[f1148,f722]) ).
fof(f1153,plain,
spl0_49,
inference(avatar_contradiction_clause,[],[f1152]) ).
fof(f1154,plain,
( ~ equidistant(x,v,v,x)
| ~ between(x,v,w)
| between(v,x,u)
| ~ spl0_49 ),
inference(resolution,[],[f723,f206]) ).
fof(f1161,plain,
( ! [X0,X1] :
( ~ equidistant(X0,x,X1,v)
| ~ equidistant(X0,w,X1,u)
| ~ between(X0,x,w)
| between(X1,v,u) )
| ~ spl0_49 ),
inference(resolution,[],[f723,f89]) ).
fof(f1163,plain,
( ~ equidistant(x,u,v,w)
| ~ between(x,u,w)
| between(v,w,u)
| ~ spl0_49 ),
inference(resolution,[],[f723,f216]) ).
fof(f1735,plain,
( ~ equidistant(w,u,u,w)
| ~ between(w,u,v)
| between(u,w,x)
| ~ spl0_30 ),
inference(resolution,[],[f378,f208]) ).
fof(f1837,plain,
( ~ equidistant(v,w,x,u)
| ~ between(v,x,w)
| between(x,v,u)
| ~ spl0_49 ),
inference(resolution,[],[f1161,f1]) ).
fof(f2082,plain,
( ~ equidistant(w,u,x,v)
| ~ between(w,u,x)
| between(x,v,w)
| ~ spl0_33 ),
inference(resolution,[],[f878,f1]) ).
fof(f2334,plain,
( ! [X0] :
( ~ between(X0,v,w)
| between(X0,v,u)
| v = w )
| ~ spl0_2 ),
inference(resolution,[],[f67,f156]) ).
fof(f2368,definition,
( spl0_70
<=> v = x ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f2369,plain,
( v != x
| spl0_70 ),
inference(avatar_component_clause,[],[f2368]) ).
fof(f2370,plain,
( v = x
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f2368]) ).
fof(f2377,definition,
( spl0_72
<=> ! [X0] :
( ~ between(X0,v,w)
| between(X0,v,u) ) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f2378,plain,
( ! [X0] :
( ~ between(X0,v,w)
| between(X0,v,u) )
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f2377]) ).
fof(f2379,plain,
( spl0_43
| spl0_72
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f2334,f154,f2377,f638]) ).
fof(f2397,plain,
( ~ between(x,v,w)
| between(v,x,u)
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1154,f1]) ).
fof(f2466,plain,
( spl0_19
| ~ spl0_10
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f894,f563,f238,f295]) ).
fof(f2539,plain,
( ~ between(w,u,v)
| ~ spl0_38
| spl0_46 ),
inference(superposition,[],[f667,f617]) ).
fof(f2584,plain,
( u = v
| ~ spl0_38
| ~ spl0_40 ),
inference(superposition,[],[f626,f617]) ).
fof(f2624,plain,
( $false
| ~ spl0_38
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2584,f123]) ).
fof(f2625,plain,
( ~ spl0_38
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f2624]) ).
fof(f2664,plain,
( ~ between(w,u,v)
| u = v
| ~ spl0_6 ),
inference(resolution,[],[f190,f61]) ).
fof(f2684,plain,
( ! [X0] :
( ~ between(X0,u,x)
| between(X0,u,w)
| u = x )
| ~ spl0_19 ),
inference(resolution,[],[f297,f67]) ).
fof(f2691,plain,
( ! [X0] :
( ~ between(X0,u,x)
| between(X0,u,w) )
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2684,f125]) ).
fof(f2791,plain,
( between(v,u,w)
| ~ spl0_17
| ~ spl0_19 ),
inference(resolution,[],[f824,f2691]) ).
fof(f2809,plain,
( $false
| spl0_5
| ~ spl0_17
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2791,f185]) ).
fof(f2810,plain,
( spl0_5
| ~ spl0_17
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2809]) ).
fof(f2827,plain,
( ~ between(w,u,x)
| between(x,v,w)
| ~ spl0_27
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2082,f365]) ).
fof(f2828,plain,
( ~ between(x,u,w)
| between(v,w,u)
| ~ spl0_9
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1163,f234]) ).
fof(f2831,plain,
( ~ between(w,v,u)
| between(v,w,x) ),
inference(forward_subsumption_resolution,[],[f883,f794]) ).
fof(f2836,plain,
( ~ between(w,u,v)
| between(v,x,w) ),
inference(forward_subsumption_resolution,[],[f1123,f794]) ).
fof(f2837,plain,
( ~ between(w,u,v)
| between(u,w,x)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1735,f1]) ).
fof(f2839,plain,
( u = v
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2664,f152]) ).
fof(f2843,plain,
( between(x,v,w)
| ~ spl0_20
| ~ spl0_27
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2827,f301]) ).
fof(f2844,plain,
( between(v,w,u)
| ~ spl0_9
| ~ spl0_16
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f2828,f265]) ).
fof(f2848,plain,
( between(v,x,w)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2836,f152]) ).
fof(f2849,plain,
( between(u,w,x)
| ~ spl0_1
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f2837,f152]) ).
fof(f2851,plain,
( $false
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2839,f123]) ).
fof(f2852,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[],[f2851]) ).
fof(f2855,plain,
( $false
| spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f2844,f155]) ).
fof(f2856,plain,
( spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f2855]) ).
fof(f2879,plain,
( ~ between(w,v,u)
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f2831,f239]) ).
fof(f2893,plain,
( ~ between(v,v,u)
| spl0_10
| ~ spl0_43 ),
inference(forward_demodulation,[],[f2879,f640]) ).
fof(f2901,plain,
( $false
| spl0_10
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f2893,f59]) ).
fof(f2902,plain,
( spl0_10
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f2901]) ).
fof(f2911,plain,
( spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f214,f154,f180]) ).
fof(f3014,plain,
( ~ between(u,w,x)
| u = w
| ~ spl0_20 ),
inference(resolution,[],[f301,f60]) ).
fof(f3119,plain,
( ~ between(x,v,u)
| v = x
| u = v
| ~ spl0_54 ),
inference(resolution,[],[f809,f62]) ).
fof(f3254,plain,
( between(x,v,u)
| ~ spl0_56
| ~ spl0_72 ),
inference(resolution,[],[f2378,f864]) ).
fof(f3258,plain,
( $false
| spl0_51
| ~ spl0_56
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f3254,f731]) ).
fof(f3259,plain,
( spl0_51
| ~ spl0_56
| ~ spl0_72 ),
inference(avatar_contradiction_clause,[],[f3258]) ).
fof(f3260,plain,
( ~ between(x,v,u)
| between(w,u,v)
| ~ spl0_14
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f1133,f766]) ).
fof(f3261,plain,
( v = x
| u = v
| ~ spl0_51
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f3119,f730]) ).
fof(f3263,plain,
( between(w,u,v)
| ~ spl0_14
| ~ spl0_51
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f3260,f730]) ).
fof(f3264,plain,
( u = v
| ~ spl0_51
| ~ spl0_54
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f3261,f2369]) ).
fof(f3267,plain,
( $false
| spl0_1
| ~ spl0_14
| ~ spl0_51
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f3263,f151]) ).
fof(f3268,plain,
( spl0_1
| ~ spl0_14
| ~ spl0_51
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f3267]) ).
fof(f3269,plain,
( $false
| ~ spl0_51
| ~ spl0_54
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f3264,f123]) ).
fof(f3270,plain,
( ~ spl0_51
| ~ spl0_54
| spl0_70 ),
inference(avatar_contradiction_clause,[],[f3269]) ).
fof(f3271,plain,
( spl0_50
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f2848,f150,f725]) ).
fof(f3272,plain,
( spl0_18
| ~ spl0_1
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f2849,f377,f150,f283]) ).
fof(f3286,plain,
( between(v,x,w)
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f2836,f152]) ).
fof(f3291,plain,
( between(v,x,u)
| ~ spl0_1
| ~ spl0_44 ),
inference(forward_demodulation,[],[f3286,f645]) ).
fof(f3337,plain,
( ~ between(v,v,y)
| spl0_45
| ~ spl0_70 ),
inference(superposition,[],[f662,f2370]) ).
fof(f3421,plain,
( $false
| spl0_45
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f3337,f59]) ).
fof(f3422,plain,
( spl0_45
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f3421]) ).
fof(f3476,plain,
( $false
| ~ spl0_1
| ~ spl0_38
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f2539,f152]) ).
fof(f3477,plain,
( ~ spl0_1
| ~ spl0_38
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f3476]) ).
fof(f3486,plain,
( ~ between(v,u,u)
| spl0_2
| ~ spl0_44 ),
inference(forward_demodulation,[],[f155,f645]) ).
fof(f3506,plain,
( between(v,x,u)
| ~ spl0_49
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f2397,f864]) ).
fof(f3512,plain,
( $false
| ~ spl0_1
| ~ spl0_44
| spl0_54 ),
inference(forward_subsumption_resolution,[],[f3291,f810]) ).
fof(f3513,plain,
( ~ spl0_1
| ~ spl0_44
| spl0_54 ),
inference(avatar_contradiction_clause,[],[f3512]) ).
fof(f3561,plain,
( $false
| spl0_2
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f3486,f56]) ).
fof(f3562,plain,
( spl0_2
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f3561]) ).
fof(f3576,plain,
( $false
| ~ spl0_49
| spl0_54
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f3506,f810]) ).
fof(f3577,plain,
( ~ spl0_49
| spl0_54
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f3576]) ).
fof(f3632,plain,
( $false
| ~ spl0_20
| ~ spl0_27
| ~ spl0_33
| spl0_56 ),
inference(forward_subsumption_resolution,[],[f2843,f865]) ).
fof(f3633,plain,
( ~ spl0_20
| ~ spl0_27
| ~ spl0_33
| spl0_56 ),
inference(avatar_contradiction_clause,[],[f3632]) ).
fof(f3638,plain,
( u = w
| ~ spl0_18
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f3014,f285]) ).
fof(f3645,plain,
spl0_30,
inference(avatar_split_clause,[],[f1144,f377]) ).
fof(f3657,plain,
( $false
| ~ spl0_18
| ~ spl0_20
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f3638,f644]) ).
fof(f3658,plain,
( ~ spl0_18
| ~ spl0_20
| spl0_44 ),
inference(avatar_contradiction_clause,[],[f3657]) ).
fof(f3706,plain,
( ~ between(v,x,w)
| between(x,v,u)
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1837,f119]) ).
fof(f3710,plain,
( between(x,v,u)
| ~ spl0_49
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f3706,f726]) ).
fof(f3712,plain,
( $false
| ~ spl0_49
| ~ spl0_50
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f3710,f731]) ).
fof(f3713,plain,
( ~ spl0_49
| ~ spl0_50
| spl0_51 ),
inference(avatar_contradiction_clause,[],[f3712]) ).
fof(f3799,plain,
( between(w,u,v)
| ~ spl0_5 ),
inference(resolution,[],[f186,f58]) ).
fof(f3805,plain,
( ! [X0] :
( ~ between(X0,v,u)
| between(X0,v,w)
| u = v )
| ~ spl0_5 ),
inference(resolution,[],[f186,f67]) ).
fof(f3812,plain,
( ! [X0] :
( ~ between(X0,v,u)
| between(X0,v,w) )
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3805,f123]) ).
fof(f3933,plain,
( between(x,v,w)
| ~ spl0_5
| ~ spl0_51 ),
inference(resolution,[],[f3812,f730]) ).
fof(f3937,plain,
( $false
| ~ spl0_5
| ~ spl0_51
| spl0_56 ),
inference(forward_subsumption_resolution,[],[f3933,f865]) ).
fof(f3938,plain,
( ~ spl0_5
| ~ spl0_51
| spl0_56 ),
inference(avatar_contradiction_clause,[],[f3937]) ).
fof(f3942,plain,
( spl0_19
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f315,f272,f295]) ).
fof(f3954,plain,
( ~ between(u,w,x)
| between(w,u,v)
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1113,f1]) ).
fof(f3956,plain,
( $false
| spl0_1
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f3799,f151]) ).
fof(f3957,plain,
( spl0_1
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[],[f3956]) ).
fof(f3967,plain,
( between(w,u,v)
| ~ spl0_18
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f3954,f285]) ).
fof(f3974,plain,
( $false
| spl0_1
| ~ spl0_18
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f3967,f151]) ).
fof(f3975,plain,
( spl0_1
| ~ spl0_18
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f3974]) ).
cnf(s2,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f191]) ).
cnf(s8,plain,
( spl0_16
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f286]) ).
cnf(s11,plain,
( spl0_17
| ~ spl0_19 ),
inference(sat_conversion,[],[f314]) ).
cnf(s15,plain,
( ~ spl0_16
| spl0_20 ),
inference(sat_conversion,[],[f386]) ).
cnf(s25,plain,
( ~ spl0_1
| ~ spl0_4
| spl0_44 ),
inference(sat_conversion,[],[f646]) ).
cnf(s26,plain,
( spl0_38
| ~ spl0_45 ),
inference(sat_conversion,[],[f663]) ).
cnf(s27,plain,
( spl0_40
| ~ spl0_46 ),
inference(sat_conversion,[],[f668]) ).
cnf(s33,plain,
spl0_9,
inference(sat_conversion,[],[f749]) ).
cnf(s39,plain,
( ~ spl0_9
| spl0_33 ),
inference(sat_conversion,[],[f799]) ).
cnf(s40,plain,
( spl0_20
| ~ spl0_54
| ~ spl0_55 ),
inference(sat_conversion,[],[f815]) ).
cnf(s41,plain,
spl0_55,
inference(sat_conversion,[],[f823]) ).
cnf(s56,plain,
( spl0_2
| ~ spl0_4 ),
inference(sat_conversion,[],[f993]) ).
cnf(s65,plain,
( spl0_52
| ~ spl0_55 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s66,plain,
( spl0_32
| ~ spl0_33 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s67,plain,
spl0_27,
inference(sat_conversion,[],[f1084]) ).
cnf(s69,plain,
( ~ spl0_9
| spl0_14 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s71,plain,
spl0_49,
inference(sat_conversion,[],[f1153]) ).
cnf(s83,plain,
( ~ spl0_2
| spl0_43
| spl0_72 ),
inference(sat_conversion,[],[f2379]) ).
cnf(s94,plain,
( ~ spl0_10
| spl0_19
| ~ spl0_33 ),
inference(sat_conversion,[],[f2466]) ).
cnf(s110,plain,
( ~ spl0_38
| ~ spl0_40 ),
inference(sat_conversion,[],[f2625]) ).
cnf(s111,plain,
( spl0_5
| ~ spl0_17
| ~ spl0_19 ),
inference(sat_conversion,[],[f2810]) ).
cnf(s121,plain,
( ~ spl0_1
| ~ spl0_6 ),
inference(sat_conversion,[],[f2852]) ).
cnf(s123,plain,
( spl0_2
| ~ spl0_9
| ~ spl0_16
| ~ spl0_49 ),
inference(sat_conversion,[],[f2856]) ).
cnf(s132,plain,
( spl0_10
| ~ spl0_43 ),
inference(sat_conversion,[],[f2902]) ).
cnf(s133,plain,
( ~ spl0_2
| spl0_4 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s142,plain,
( spl0_51
| ~ spl0_56
| ~ spl0_72 ),
inference(sat_conversion,[],[f3259]) ).
cnf(s144,plain,
( spl0_1
| ~ spl0_14
| ~ spl0_51
| ~ spl0_52 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s145,plain,
( ~ spl0_51
| ~ spl0_54
| spl0_70 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s146,plain,
( ~ spl0_1
| spl0_50 ),
inference(sat_conversion,[],[f3271]) ).
cnf(s147,plain,
( ~ spl0_1
| spl0_18
| ~ spl0_30 ),
inference(sat_conversion,[],[f3272]) ).
cnf(s149,plain,
( spl0_45
| ~ spl0_70 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s151,plain,
( ~ spl0_1
| ~ spl0_38
| spl0_46 ),
inference(sat_conversion,[],[f3477]) ).
cnf(s156,plain,
( ~ spl0_1
| ~ spl0_44
| spl0_54 ),
inference(sat_conversion,[],[f3513]) ).
cnf(s159,plain,
( spl0_2
| ~ spl0_44 ),
inference(sat_conversion,[],[f3562]) ).
cnf(s165,plain,
( ~ spl0_49
| spl0_54
| ~ spl0_56 ),
inference(sat_conversion,[],[f3577]) ).
cnf(s174,plain,
( ~ spl0_20
| ~ spl0_27
| ~ spl0_33
| spl0_56 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s176,plain,
spl0_30,
inference(sat_conversion,[],[f3645]) ).
cnf(s184,plain,
( ~ spl0_18
| ~ spl0_20
| spl0_44 ),
inference(sat_conversion,[],[f3658]) ).
cnf(s194,plain,
( ~ spl0_49
| ~ spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f3713]) ).
cnf(s196,plain,
( ~ spl0_5
| ~ spl0_51
| spl0_56 ),
inference(sat_conversion,[],[f3938]) ).
cnf(s203,plain,
( ~ spl0_17
| spl0_19 ),
inference(sat_conversion,[],[f3942]) ).
cnf(s205,plain,
( spl0_1
| ~ spl0_5 ),
inference(sat_conversion,[],[f3957]) ).
cnf(s210,plain,
( spl0_1
| ~ spl0_18
| ~ spl0_32 ),
inference(sat_conversion,[],[f3975]) ).
cnf(s212,plain,
( ~ spl0_1
| spl0_18 ),
inference(rat,[],[s147,s176]) ).
cnf(s216,plain,
spl0_52,
inference(rat,[],[s65,s41]) ).
cnf(s217,plain,
( spl0_20
| ~ spl0_54 ),
inference(rat,[],[s40,s41]) ).
cnf(s222,plain,
spl0_14,
inference(rat,[],[s69,s33]) ).
cnf(s223,plain,
spl0_33,
inference(rat,[],[s39,s33]) ).
cnf(s224,plain,
spl0_32,
inference(rat,[],[s66,s223]) ).
cnf(s235,plain,
( ~ spl0_17
| spl0_5 ),
inference(rat,[],[s111,s203]) ).
cnf(s236,plain,
spl0_1,
inference(rat,[],[s142,s83,s174,s132,s15,s123,s94,s8,s11,s235,s144,s205,s210,s67,s223,s33,s71,s222,s216,s224]) ).
cnf(s237,plain,
spl0_18,
inference(rat,[],[s212,s236]) ).
cnf(s238,plain,
spl0_50,
inference(rat,[],[s146,s236]) ).
cnf(s239,plain,
~ spl0_6,
inference(rat,[],[s121,s236]) ).
cnf(s240,plain,
spl0_51,
inference(rat,[],[s194,s71,s238]) ).
cnf(s249,plain,
spl0_2,
inference(rat,[],[s165,s196,s217,s2,s184,s56,s159,s71,s240,s239,s237]) ).
cnf(s250,plain,
spl0_4,
inference(rat,[],[s133,s249]) ).
cnf(s253,plain,
spl0_44,
inference(rat,[],[s25,s236,s250]) ).
cnf(s259,plain,
spl0_54,
inference(rat,[],[s156,s236,s253]) ).
cnf(s263,plain,
spl0_70,
inference(rat,[],[s145,s240,s259]) ).
cnf(s264,plain,
spl0_45,
inference(rat,[],[s149,s263]) ).
cnf(s268,plain,
spl0_38,
inference(rat,[],[s26,s264]) ).
cnf(s271,plain,
spl0_46,
inference(rat,[],[s151,s236,s268]) ).
cnf(s272,plain,
~ spl0_40,
inference(rat,[],[s110,s268]) ).
cnf(s278,plain,
$false,
inference(rat,[],[s27,s271,s272]) ).
fof(f3978,plain,
$false,
inference(avatar_sat_refutation,[],[s278]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO070-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.44 % Computer : n002.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 27 06:53:36 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.50 Running first-order theorem proving
% 0.23/0.50 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
% 18.60/3.76 % (3191100)Input is clausal, will run a generic CNF schedule.
% 18.60/3.76 % (3191114)dis-21_1_sil=8000:lcm=predicate:random_seed=693065824: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)
% 18.60/3.76 % (3191111)lrs+10_1_sil=8000:sp=occurrence:random_seed=1737700163:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.60/3.76 % (3191110)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1332882298:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.60/3.76 % (3191109)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1854758999:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.60/3.76 % (3191112)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1741274069:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.60/3.76 % (3191113)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2030415084:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.60/3.76 % (3191108)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=2957130317:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.60/3.76 % (3191111)Instruction limit reached!
% 18.60/3.76 % (3191111)------------------------------
% 18.60/3.76 % (3191111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.76 % (3191111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.76 % (3191111)CaDiCaL version: 2.1.3
% 18.60/3.76 % (3191111)Termination reason: Instruction limit
% 18.60/3.76 % (3191111)Termination phase: Saturation
% 18.60/3.76 % (3191111)Time elapsed: 0.099 s
% 18.60/3.76 % (3191111)Peak memory usage: 88 MB
% 18.60/3.76 % (3191111)Instructions burned: 108 (million)
% 18.60/3.76 % (3191114)Instruction limit reached!
% 18.60/3.76 % (3191114)------------------------------
% 18.60/3.76 % (3191114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.76 % (3191114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.76 % (3191114)CaDiCaL version: 2.1.3
% 18.60/3.76 % (3191114)Termination reason: Instruction limit
% 18.60/3.76 % (3191114)Termination phase: Saturation
% 18.60/3.76 % (3191114)Time elapsed: 0.112 s
% 18.60/3.76 % (3191114)Peak memory usage: 89 MB
% 18.60/3.76 % (3191114)Instructions burned: 117 (million)
% 18.60/3.76 % (3191112)Instruction limit reached!
% 18.60/3.76 % (3191112)------------------------------
% 18.60/3.76 % (3191112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.76 % (3191112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.76 % (3191112)CaDiCaL version: 2.1.3
% 18.60/3.76 % (3191112)Termination reason: Instruction limit
% 18.60/3.76 % (3191112)Termination phase: Saturation
% 18.60/3.76 % (3191112)Time elapsed: 0.111 s
% 18.60/3.76 % (3191112)Peak memory usage: 88 MB
% 18.60/3.76 % (3191112)Instructions burned: 114 (million)
% 18.60/3.76 % (3191113)Instruction limit reached!
% 18.60/3.76 % (3191113)------------------------------
% 18.60/3.76 % (3191113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/3.76 % (3191113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/3.76 % (3191113)CaDiCaL version: 2.1.3
% 18.60/3.76 % (3191113)Termination reason: Instruction limit
% 18.60/3.76 % (3191113)Termination phase: Saturation
% 18.60/3.76 % (3191113)Time elapsed: 0.185 s
% 18.60/3.76 % (3191113)Peak memory usage: 89 MB
% 18.60/3.76 % (3191113)Instructions burned: 181 (million)
% 18.60/3.76 % (3191123)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=2214304816:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.60/3.76 % (3191124)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1346579576:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 18.60/3.76 % (3191125)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3273621737:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 18.60/3.76 % (3191123)Instruction limit reached!
% 18.60/3.76 % (3191123)------------------------------
% 18.60/3.76 % (3191123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191123)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191123)Termination reason: Instruction limit
% 22.38/4.30 % (3191123)Termination phase: Saturation
% 22.38/4.30 % (3191123)Time elapsed: 0.139 s
% 22.38/4.30 % (3191123)Peak memory usage: 89 MB
% 22.38/4.30 % (3191123)Instructions burned: 143 (million)
% 22.38/4.30 % (3191126)lrs+10_64_to=lpo:sil=8000:random_seed=1408882129:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 22.38/4.30 % (3191124)Instruction limit reached!
% 22.38/4.30 % (3191124)------------------------------
% 22.38/4.30 % (3191124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191124)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191124)Termination reason: Instruction limit
% 22.38/4.30 % (3191124)Termination phase: Saturation
% 22.38/4.30 % (3191124)Time elapsed: 0.155 s
% 22.38/4.30 % (3191124)Peak memory usage: 88 MB
% 22.38/4.30 % (3191124)Instructions burned: 189 (million)
% 22.38/4.30 % (3191126)Instruction limit reached!
% 22.38/4.30 % (3191126)------------------------------
% 22.38/4.30 % (3191126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191126)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191126)Termination reason: Instruction limit
% 22.38/4.30 % (3191126)Termination phase: Saturation
% 22.38/4.30 % (3191126)Time elapsed: 0.127 s
% 22.38/4.30 % (3191126)Peak memory usage: 89 MB
% 22.38/4.30 % (3191126)Instructions burned: 126 (million)
% 22.38/4.30 % (3191125)Instruction limit reached!
% 22.38/4.30 % (3191125)------------------------------
% 22.38/4.30 % (3191125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191125)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191125)Termination reason: Instruction limit
% 22.38/4.30 % (3191125)Termination phase: Saturation
% 22.38/4.30 % (3191125)Time elapsed: 0.212 s
% 22.38/4.30 % (3191125)Peak memory usage: 90 MB
% 22.38/4.30 % (3191125)Instructions burned: 219 (million)
% 22.38/4.30 % (3191130)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1247431976:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 22.38/4.30 % (3191132)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1019858785:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 22.38/4.30 % (3191134)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=3992168563:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 22.38/4.30 % (3191133)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2569434586:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 22.38/4.30 % (3191130)Instruction limit reached!
% 22.38/4.30 % (3191130)------------------------------
% 22.38/4.30 % (3191130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191130)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191130)Termination reason: Instruction limit
% 22.38/4.30 % (3191130)Termination phase: Saturation
% 22.38/4.30 % (3191130)Time elapsed: 0.201 s
% 22.38/4.30 % (3191130)Peak memory usage: 89 MB
% 22.38/4.30 % (3191130)Instructions burned: 194 (million)
% 22.38/4.30 % (3191132)Instruction limit reached!
% 22.38/4.30 % (3191132)------------------------------
% 22.38/4.30 % (3191132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191132)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191132)Termination reason: Instruction limit
% 22.38/4.30 % (3191132)Termination phase: Saturation
% 22.38/4.30 % (3191132)Time elapsed: 0.129 s
% 22.38/4.30 % (3191132)Peak memory usage: 90 MB
% 22.38/4.30 % (3191132)Instructions burned: 158 (million)
% 22.38/4.30 % (3191134)Instruction limit reached!
% 22.38/4.30 % (3191134)------------------------------
% 22.38/4.30 % (3191134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191134)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191134)Termination reason: Instruction limit
% 22.38/4.30 % (3191134)Termination phase: Saturation
% 22.38/4.30 % (3191134)Time elapsed: 0.091 s
% 22.38/4.30 % (3191134)Peak memory usage: 88 MB
% 22.38/4.30 % (3191134)Instructions burned: 107 (million)
% 22.38/4.30 % (3191141)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4219043267:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 22.38/4.30 % (3191140)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3002636752:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 22.38/4.30 % (3191140)Instruction limit reached!
% 22.38/4.30 % (3191140)------------------------------
% 22.38/4.30 % (3191140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191140)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191140)Termination reason: Instruction limit
% 22.38/4.30 % (3191140)Termination phase: Saturation
% 22.38/4.30 % (3191140)Time elapsed: 0.081 s
% 22.38/4.30 % (3191140)Peak memory usage: 89 MB
% 22.38/4.30 % (3191140)Instructions burned: 108 (million)
% 22.38/4.30 % (3191143)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2298336057:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 22.38/4.30 % (3191141)Instruction limit reached!
% 22.38/4.30 % (3191141)------------------------------
% 22.38/4.30 % (3191141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191141)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191141)Termination reason: Instruction limit
% 22.38/4.30 % (3191141)Termination phase: Saturation
% 22.38/4.30 % (3191141)Time elapsed: 0.255 s
% 22.38/4.30 % (3191141)Peak memory usage: 90 MB
% 22.38/4.30 % (3191141)Instructions burned: 243 (million)
% 22.38/4.30 % (3191147)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2731540840:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 22.38/4.30 % (3191150)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2317402821:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 22.38/4.30 % (3191147)Instruction limit reached!
% 22.38/4.30 % (3191147)------------------------------
% 22.38/4.30 % (3191147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191147)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191147)Termination reason: Instruction limit
% 22.38/4.30 % (3191147)Termination phase: Saturation
% 22.38/4.30 % (3191147)Time elapsed: 0.135 s
% 22.38/4.30 % (3191147)Peak memory usage: 89 MB
% 22.38/4.30 % (3191147)Instructions burned: 134 (million)
% 22.38/4.30 % (3191153)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1960434919:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 22.38/4.30 % (3191150)Instruction limit reached!
% 22.38/4.30 % (3191150)------------------------------
% 22.38/4.30 % (3191150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191150)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191150)Termination reason: Instruction limit
% 22.38/4.30 % (3191150)Termination phase: Saturation
% 22.38/4.30 % (3191150)Time elapsed: 0.472 s
% 22.38/4.30 % (3191150)Peak memory usage: 93 MB
% 22.38/4.30 % (3191150)Instructions burned: 499 (million)
% 22.38/4.30 % (3191153)Instruction limit reached!
% 22.38/4.30 % (3191153)------------------------------
% 22.38/4.30 % (3191153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191153)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191153)Termination reason: Instruction limit
% 22.38/4.30 % (3191153)Termination phase: Saturation
% 22.38/4.30 % (3191153)Time elapsed: 0.198 s
% 22.38/4.30 % (3191153)Peak memory usage: 91 MB
% 22.38/4.30 % (3191153)Instructions burned: 191 (million)
% 22.38/4.30 % (3191157)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=821466290:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 22.38/4.30 % (3191158)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4234788251:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 22.38/4.30 % (3191133)First to succeed.
% 22.38/4.30 % (3191133)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3191100"
% 22.38/4.30 % (3191158)Instruction limit reached!
% 22.38/4.30 % (3191158)------------------------------
% 22.38/4.30 % (3191158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191158)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191158)Termination reason: Instruction limit
% 22.38/4.30 % (3191158)Termination phase: Saturation
% 22.38/4.30 % (3191158)Time elapsed: 0.152 s
% 22.38/4.30 % (3191158)Peak memory usage: 89 MB
% 22.38/4.30 % (3191158)Instructions burned: 157 (million)
% 22.38/4.30 % (3191157)Instruction limit reached!
% 22.38/4.30 % (3191157)------------------------------
% 22.38/4.30 % (3191157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.38/4.30 % (3191157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.38/4.30 % (3191157)CaDiCaL version: 2.1.3
% 22.38/4.30 % (3191157)Termination reason: Instruction limit
% 22.38/4.30 % (3191157)Termination phase: Saturation
% 22.38/4.30 % (3191157)Time elapsed: 0.258 s
% 22.38/4.30 % (3191157)Peak memory usage: 91 MB
% 22.38/4.30 % (3191157)Instructions burned: 264 (million)
% 22.38/4.30 % (3191161)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=1777971751:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 22.38/4.30 % (3191133)Refutation found. Thanks to Tanya!
% 22.38/4.30 % SZS status Unsatisfiable for theBenchmark
% 22.38/4.30 % SZS output start Proof for theBenchmark
% See solution above
% 23.45/4.55 % (3191133)------------------------------
% 23.45/4.55 % (3191133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.45/4.55 % (3191133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.45/4.55 % (3191133)CaDiCaL version: 2.1.3
% 23.45/4.55 % (3191133)Termination reason: Refutation
% 23.45/4.55 % (3191133)Time elapsed: 1.604 s
% 23.45/4.55 % (3191133)Peak memory usage: 134 MB
% 23.45/4.55 % (3191133)Instructions burned: 1451 (million)
% 23.45/4.55 % (3191133)------------------------------
% 23.45/4.55 % (3191133)------------------------------
% 23.45/4.55 % (3191100)Success in time 3.2 s
% 23.45/4.55 % Vampire exiting
%------------------------------------------------------------------------------