%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO032-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 : 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:16 AM UTC 2026
% Result : Unsatisfiable 8.13s 2.08s
% Output : Refutation 8.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 19
% Syntax : Number of formulae : 114 ( 34 unt; 5 def)
% Number of atoms : 287 ( 41 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 318 ( 145 ~; 168 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-5 aty)
% Number of variables : 217 ( 0 sgn 217 !; 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,
between(u,v,w),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_between_u_and_w) ).
fof(f20,axiom,
between(u1,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1_between_u1_and_w1) ).
fof(f21,axiom,
equidistant(u,v,u1,v1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_u1_to_v1) ).
fof(f22,axiom,
equidistant(u,w,u1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_w_equals_u1_to_w1) ).
fof(f23,negated_conjecture,
~ equidistant(v,w,v1,w1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v_to_w_equals_v1_to_w1) ).
fof(f26,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f1,f2]) ).
fof(f28,plain,
equidistant(u1,v1,v,u),
inference(resolution,[],[f26,f21]) ).
fof(f29,plain,
! [X0,X1] : equidistant(X0,X1,X0,X1),
inference(resolution,[],[f26,f1]) ).
fof(f31,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X0,X1) ),
inference(resolution,[],[f29,f2]) ).
fof(f36,plain,
equidistant(v,u,v1,u1),
inference(resolution,[],[f28,f26]) ).
fof(f38,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X0,X1),X3),
inference(resolution,[],[f5,f26]) ).
fof(f39,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(f40,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f5,f3]) ).
fof(f41,plain,
! [X2,X0] : equidistant(X0,X0,X2,X2),
inference(superposition,[],[f5,f40]) ).
fof(f42,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f4,f40]) ).
fof(f44,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X0,X1,X2)
| equidistant(X1,X2,X3,X3) ),
inference(resolution,[],[f41,f2]) ).
fof(f49,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(f50,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(f66,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,extension(X2,X0,X3,X4))
| inner_pasch(X0,X1,extension(X2,X0,X3,X4),X0,X2) = X0 ),
inference(resolution,[],[f49,f4]) ).
fof(f75,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,f21]) ).
fof(f77,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,f29]) ).
fof(f83,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,[],[f75,f22]) ).
fof(f97,definition,
( spl0_3
<=> equidistant(w,v,w1,v1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f99,plain,
( equidistant(w,v,w1,v1)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f101,definition,
( spl0_4
<=> ! [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_4])],[avatar_definition]) ).
fof(f102,plain,
( ! [X0,X1] :
( ~ equidistant(X0,v,X1,v1)
| u = X0
| ~ between(X1,u1,w1)
| ~ between(X0,u,w)
| ~ equidistant(X0,u,X1,u1) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f101]) ).
fof(f103,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f83,f101,f97]) ).
fof(f105,plain,
( equidistant(w1,v1,v,w)
| ~ spl0_3 ),
inference(resolution,[],[f99,f26]) ).
fof(f108,plain,
( equidistant(v,w,v1,w1)
| ~ spl0_3 ),
inference(resolution,[],[f105,f26]) ).
fof(f110,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f108,f23]) ).
fof(f111,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f110]) ).
fof(f142,definition,
( spl0_11
<=> u = v ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f143,plain,
( u != v
| spl0_11 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f144,plain,
( u = v
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f218,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X3,X2),
inference(resolution,[],[f38,f26]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4,X5] : equidistant(extension(X0,X1,X2,extension(X3,X2,X4,X5)),X1,X4,X5),
inference(resolution,[],[f38,f39]) ).
fof(f249,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,[],[f77,f29]) ).
fof(f256,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,[],[f249,f29]) ).
fof(f260,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,[],[f256,f5]) ).
fof(f268,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,X2,extension(X3,X2,X0,X1)),
inference(resolution,[],[f31,f5]) ).
fof(f270,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X1,X0),X3),
inference(resolution,[],[f31,f218]) ).
fof(f287,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,[],[f268,f75]) ).
fof(f310,plain,
( equidistant(u,u,u1,v1)
| ~ spl0_11 ),
inference(superposition,[],[f21,f144]) ).
fof(f325,plain,
( ! [X0] : equidistant(u1,v1,X0,X0)
| ~ spl0_11 ),
inference(resolution,[],[f310,f44]) ).
fof(f339,plain,
( u1 = v1
| ~ spl0_11 ),
inference(resolution,[],[f325,f3]) ).
fof(f353,plain,
( ~ equidistant(v,w,u1,w1)
| ~ spl0_11 ),
inference(superposition,[],[f23,f339]) ).
fof(f373,plain,
( ~ equidistant(u,w,u1,w1)
| ~ spl0_11 ),
inference(forward_demodulation,[],[f353,f144]) ).
fof(f379,plain,
( $false
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f373,f22]) ).
fof(f380,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f379]) ).
fof(f541,definition,
( spl0_31
<=> u1 = v1 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f543,plain,
( u1 = v1
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f630,plain,
! [X2,X3,X0,X1] : inner_pasch(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3),X0,X1) = X0,
inference(resolution,[],[f66,f42]) ).
fof(f658,plain,
! [X2,X3,X0,X1] :
( between(extension(X1,X0,X2,X3),X0,X1)
| ~ between(X1,X0,extension(X1,X0,X2,X3))
| ~ between(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3)) ),
inference(superposition,[],[f8,f630]) ).
fof(f660,plain,
! [X2,X3,X0,X1] :
( between(extension(X1,X0,X2,X3),X0,X1)
| ~ between(X0,extension(X1,X0,X2,X3),extension(X1,X0,X2,X3)) ),
inference(forward_subsumption_resolution,[],[f658,f4]) ).
fof(f661,plain,
! [X2,X3,X0,X1] : between(extension(X1,X0,X2,X3),X0,X1),
inference(forward_subsumption_resolution,[],[f660,f42]) ).
fof(f663,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| inner_pasch(extension(X2,X0,X3,X4),X0,X2,X1,X0) = X0 ),
inference(resolution,[],[f661,f50]) ).
fof(f721,plain,
! [X0,X1] : u = inner_pasch(extension(w,u,X0,X1),u,w,v,u),
inference(resolution,[],[f663,f19]) ).
fof(f723,plain,
! [X0,X1] : u1 = inner_pasch(extension(w1,u1,X0,X1),u1,w1,v1,u1),
inference(resolution,[],[f663,f20]) ).
fof(f728,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,f721]) ).
fof(f729,plain,
! [X0,X1] :
( between(v,u,extension(w,u,X0,X1))
| ~ between(extension(w,u,X0,X1),u,w) ),
inference(forward_subsumption_resolution,[],[f728,f19]) ).
fof(f730,plain,
! [X0,X1] : between(v,u,extension(w,u,X0,X1)),
inference(forward_subsumption_resolution,[],[f729,f661]) ).
fof(f734,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,f723]) ).
fof(f735,plain,
! [X0,X1] :
( between(v1,u1,extension(w1,u1,X0,X1))
| ~ between(extension(w1,u1,X0,X1),u1,w1) ),
inference(forward_subsumption_resolution,[],[f734,f20]) ).
fof(f736,plain,
! [X0,X1] : between(v1,u1,extension(w1,u1,X0,X1)),
inference(forward_subsumption_resolution,[],[f735,f661]) ).
fof(f739,plain,
! [X0,X1] :
( ~ between(v,u,X0)
| u = v
| equidistant(extension(w,u,u,X0),X1,X0,X1) ),
inference(resolution,[],[f730,f260]) ).
fof(f747,plain,
( ! [X0,X1] :
( equidistant(extension(w,u,u,X0),X1,X0,X1)
| ~ between(v,u,X0) )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f739,f143]) ).
fof(f750,plain,
! [X0,X1] :
( ~ between(v1,u1,X0)
| u1 = v1
| equidistant(extension(w1,u1,u1,X0),X1,X0,X1) ),
inference(resolution,[],[f736,f260]) ).
fof(f762,definition,
( spl0_35
<=> ! [X0,X1] :
( ~ between(v1,u1,X0)
| equidistant(extension(w1,u1,u1,X0),X1,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f763,plain,
( ! [X0,X1] :
( equidistant(extension(w1,u1,u1,X0),X1,X0,X1)
| ~ between(v1,u1,X0) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f764,plain,
( spl0_31
| spl0_35 ),
inference(avatar_split_clause,[],[f750,f762,f541]) ).
fof(f766,plain,
( equidistant(u,v,u1,u1)
| ~ spl0_31 ),
inference(superposition,[],[f21,f543]) ).
fof(f791,plain,
( u = v
| ~ spl0_31 ),
inference(resolution,[],[f766,f3]) ).
fof(f792,plain,
( $false
| spl0_11
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f791,f143]) ).
fof(f793,plain,
( spl0_11
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f805,plain,
( ! [X0] :
( ~ between(v1,u1,X0)
| extension(w1,u1,u1,X0) = X0 )
| ~ spl0_35 ),
inference(resolution,[],[f763,f3]) ).
fof(f812,plain,
( ! [X0,X1] : extension(v1,u1,X0,X1) = extension(w1,u1,u1,extension(v1,u1,X0,X1))
| ~ spl0_35 ),
inference(resolution,[],[f805,f4]) ).
fof(f819,plain,
( ! [X0] :
( ~ between(v,u,X0)
| extension(w,u,u,X0) = X0 )
| spl0_11 ),
inference(resolution,[],[f747,f3]) ).
fof(f856,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,[],[f287,f4]) ).
fof(f863,plain,
! [X0] :
( ~ between(v,u,X0)
| ~ equidistant(v,u,v1,u1)
| u = v
| equidistant(X0,v,extension(v1,u1,u,X0),v1) ),
inference(resolution,[],[f856,f41]) ).
fof(f871,plain,
! [X0] :
( ~ between(v,u,X0)
| u = v
| equidistant(X0,v,extension(v1,u1,u,X0),v1) ),
inference(forward_subsumption_resolution,[],[f863,f36]) ).
fof(f872,plain,
( ! [X0] :
( equidistant(X0,v,extension(v1,u1,u,X0),v1)
| ~ between(v,u,X0) )
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f871,f143]) ).
fof(f875,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_4
| spl0_11 ),
inference(resolution,[],[f872,f102]) ).
fof(f892,plain,
( ! [X0] :
( ~ between(extension(v1,u1,u,X0),u1,w1)
| u = X0
| ~ between(v,u,X0)
| ~ between(X0,u,w) )
| ~ spl0_4
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f875,f270]) ).
fof(f950,plain,
( ! [X0,X1] : between(extension(v1,u1,X0,X1),u1,w1)
| ~ spl0_35 ),
inference(superposition,[],[f661,f812]) ).
fof(f954,plain,
( ! [X0] :
( ~ between(v,u,X0)
| u = X0
| ~ between(X0,u,w) )
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(resolution,[],[f950,f892]) ).
fof(f1144,plain,
( ! [X0,X1] : extension(v,u,X0,X1) = extension(w,u,u,extension(v,u,X0,X1))
| spl0_11 ),
inference(resolution,[],[f819,f4]) ).
fof(f1167,plain,
( ! [X0,X1] : between(extension(v,u,X0,X1),u,w)
| spl0_11 ),
inference(superposition,[],[f661,f1144]) ).
fof(f1226,plain,
( ! [X0,X1] :
( u = extension(v,u,X0,X1)
| ~ between(extension(v,u,X0,X1),u,w) )
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(resolution,[],[f954,f4]) ).
fof(f1228,plain,
( ! [X0,X1] : u = extension(v,u,X0,X1)
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1226,f1167]) ).
fof(f1240,plain,
( ! [X2,X3,X0,X1] :
( ~ equidistant(u,u,X2,X3)
| equidistant(X2,X3,X0,X1) )
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(superposition,[],[f39,f1228]) ).
fof(f1255,plain,
( ! [X2,X3] : equidistant(u,u,X2,X3)
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(superposition,[],[f220,f1228]) ).
fof(f1264,plain,
( ! [X2,X3,X0,X1] : equidistant(X2,X3,X0,X1)
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1240,f1255]) ).
fof(f1287,plain,
( $false
| ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(resolution,[],[f1264,f23]) ).
fof(f1292,plain,
( ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1287]) ).
cnf(s2,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f103]) ).
cnf(s3,plain,
~ spl0_3,
inference(sat_conversion,[],[f111]) ).
cnf(s11,plain,
~ spl0_11,
inference(sat_conversion,[],[f380]) ).
cnf(s22,plain,
( spl0_31
| spl0_35 ),
inference(sat_conversion,[],[f764]) ).
cnf(s23,plain,
( spl0_11
| ~ spl0_31 ),
inference(sat_conversion,[],[f793]) ).
cnf(s27,plain,
( ~ spl0_4
| spl0_11
| ~ spl0_35 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s29,plain,
~ spl0_31,
inference(rat,[],[s23,s11]) ).
cnf(s30,plain,
spl0_35,
inference(rat,[],[s22,s29]) ).
cnf(s33,plain,
~ spl0_4,
inference(rat,[],[s27,s11,s30]) ).
cnf(s36,plain,
$false,
inference(rat,[],[s2,s33,s3]) ).
fof(f1295,plain,
$false,
inference(avatar_sat_refutation,[],[s36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO032-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 06:40:52 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 8.13/2.08 % (3182624)Input is clausal, will run a generic CNF schedule.
% 8.13/2.08 % (3182645)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=2566672974:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.13/2.08 % (3182648)lrs+10_1_sil=8000:sp=occurrence:random_seed=2616117257:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.13/2.08 % (3182646)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2530456002:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.13/2.08 % (3182651)dis-21_1_sil=8000:lcm=predicate:random_seed=74081918: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)
% 8.13/2.08 % (3182647)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2146026237:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.13/2.08 % (3182649)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1385594924:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.13/2.08 % (3182648)Refutation not found, incomplete strategy
% 8.13/2.08 % (3182648)------------------------------
% 8.13/2.08 % (3182648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182648)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182648)Termination reason: Refutation not found, incomplete strategy
% 8.13/2.08 % (3182648)Time elapsed: 0.002 s
% 8.13/2.08 % (3182648)Peak memory usage: 87 MB
% 8.13/2.08 % (3182648)Instructions burned: 2 (million)
% 8.13/2.08 % (3182650)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2319539185:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.13/2.08 % (3182649)Instruction limit reached!
% 8.13/2.08 % (3182649)------------------------------
% 8.13/2.08 % (3182649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182649)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182649)Termination reason: Instruction limit
% 8.13/2.08 % (3182649)Termination phase: Saturation
% 8.13/2.08 % (3182649)Time elapsed: 0.024 s
% 8.13/2.08 % (3182649)Peak memory usage: 87 MB
% 8.13/2.08 % (3182649)Instructions burned: 118 (million)
% 8.13/2.08 % (3182651)Instruction limit reached!
% 8.13/2.08 % (3182651)------------------------------
% 8.13/2.08 % (3182651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182651)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182651)Termination reason: Instruction limit
% 8.13/2.08 % (3182651)Termination phase: Saturation
% 8.13/2.08 % (3182651)Time elapsed: 0.065 s
% 8.13/2.08 % (3182651)Peak memory usage: 88 MB
% 8.13/2.08 % (3182651)Instructions burned: 118 (million)
% 8.13/2.08 % (3182660)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=23052653:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.13/2.08 % (3182650)Instruction limit reached!
% 8.13/2.08 % (3182650)------------------------------
% 8.13/2.08 % (3182650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182650)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182650)Termination reason: Instruction limit
% 8.13/2.08 % (3182650)Termination phase: Saturation
% 8.13/2.08 % (3182650)Time elapsed: 0.116 s
% 8.13/2.08 % (3182650)Peak memory usage: 89 MB
% 8.13/2.08 % (3182650)Instructions burned: 180 (million)
% 8.13/2.08 % (3182660)Instruction limit reached!
% 8.13/2.08 % (3182660)------------------------------
% 8.13/2.08 % (3182660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182660)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182660)Termination reason: Instruction limit
% 8.13/2.08 % (3182660)Termination phase: Saturation
% 8.13/2.08 % (3182660)Time elapsed: 0.055 s
% 8.13/2.08 % (3182660)Peak memory usage: 89 MB
% 8.13/2.08 % (3182660)Instructions burned: 143 (million)
% 8.13/2.08 % (3182661)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3369306672:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 8.13/2.08 % (3182648)------------------------------
% 8.13/2.08 % (3182648)------------------------------
% 8.13/2.08 % (3182688)lrs+10_64_to=lpo:sil=8000:random_seed=178360259:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 8.13/2.08 % (3182671)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=525156973:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.13/2.08 % (3182661)Instruction limit reached!
% 8.13/2.08 % (3182661)------------------------------
% 8.13/2.08 % (3182661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182661)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182661)Termination reason: Instruction limit
% 8.13/2.08 % (3182661)Termination phase: Saturation
% 8.13/2.08 % (3182661)Time elapsed: 0.107 s
% 8.13/2.08 % (3182661)Peak memory usage: 89 MB
% 8.13/2.08 % (3182661)Instructions burned: 189 (million)
% 8.13/2.08 % (3182688)Instruction limit reached!
% 8.13/2.08 % (3182688)------------------------------
% 8.13/2.08 % (3182688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182688)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182688)Termination reason: Instruction limit
% 8.13/2.08 % (3182688)Termination phase: Saturation
% 8.13/2.08 % (3182688)Time elapsed: 0.044 s
% 8.13/2.08 % (3182688)Peak memory usage: 89 MB
% 8.13/2.08 % (3182688)Instructions burned: 129 (million)
% 8.13/2.08 % (3182721)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1845855207:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 8.13/2.08 % (3182743)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3846153725:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 8.13/2.08 % (3182671)Instruction limit reached!
% 8.13/2.08 % (3182671)------------------------------
% 8.13/2.08 % (3182671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182671)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182671)Termination reason: Instruction limit
% 8.13/2.08 % (3182671)Termination phase: Saturation
% 8.13/2.08 % (3182671)Time elapsed: 0.126 s
% 8.13/2.08 % (3182671)Peak memory usage: 89 MB
% 8.13/2.08 % (3182671)Instructions burned: 220 (million)
% 8.13/2.08 % (3182742)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2972649438:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.13/2.08 % (3182721)Instruction limit reached!
% 8.13/2.08 % (3182721)------------------------------
% 8.13/2.08 % (3182721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182721)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182721)Termination reason: Instruction limit
% 8.13/2.08 % (3182721)Termination phase: Saturation
% 8.13/2.08 % (3182721)Time elapsed: 0.120 s
% 8.13/2.08 % (3182721)Peak memory usage: 88 MB
% 8.13/2.08 % (3182721)Instructions burned: 194 (million)
% 8.13/2.08 % (3182742)Instruction limit reached!
% 8.13/2.08 % (3182742)------------------------------
% 8.13/2.08 % (3182742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182742)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182742)Termination reason: Instruction limit
% 8.13/2.08 % (3182742)Termination phase: Saturation
% 8.13/2.08 % (3182742)Time elapsed: 0.109 s
% 8.13/2.08 % (3182742)Peak memory usage: 90 MB
% 8.13/2.08 % (3182742)Instructions burned: 157 (million)
% 8.13/2.08 % (3182768)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=3318028124:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 8.13/2.08 % (3182768)Instruction limit reached!
% 8.13/2.08 % (3182768)------------------------------
% 8.13/2.08 % (3182768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182768)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182768)Termination reason: Instruction limit
% 8.13/2.08 % (3182768)Termination phase: Saturation
% 8.13/2.08 % (3182768)Time elapsed: 0.060 s
% 8.13/2.08 % (3182768)Peak memory usage: 88 MB
% 8.13/2.08 % (3182768)Instructions burned: 106 (million)
% 8.13/2.08 % (3182780)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=812103333:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 8.13/2.08 % (3182786)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1271169917:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 8.13/2.08 % (3182780)Instruction limit reached!
% 8.13/2.08 % (3182780)------------------------------
% 8.13/2.08 % (3182780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182780)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182780)Termination reason: Instruction limit
% 8.13/2.08 % (3182780)Termination phase: Saturation
% 8.13/2.08 % (3182780)Time elapsed: 0.074 s
% 8.13/2.08 % (3182780)Peak memory usage: 89 MB
% 8.13/2.08 % (3182780)Instructions burned: 108 (million)
% 8.13/2.08 % (3182807)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3689690308:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 8.13/2.08 % (3182786)Instruction limit reached!
% 8.13/2.08 % (3182786)------------------------------
% 8.13/2.08 % (3182786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182786)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182786)Termination reason: Instruction limit
% 8.13/2.08 % (3182786)Termination phase: Saturation
% 8.13/2.08 % (3182786)Time elapsed: 0.163 s
% 8.13/2.08 % (3182786)Peak memory usage: 89 MB
% 8.13/2.08 % (3182786)Instructions burned: 244 (million)
% 8.13/2.08 % (3182833)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3047862065:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 8.13/2.08 % (3182743)First to succeed.
% 8.13/2.08 % (3182743)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3182624"
% 8.13/2.08 % (3182833)Instruction limit reached!
% 8.13/2.08 % (3182833)------------------------------
% 8.13/2.08 % (3182833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.13/2.08 % (3182833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/2.08 % (3182833)CaDiCaL version: 2.1.3
% 8.13/2.08 % (3182833)Termination reason: Instruction limit
% 8.13/2.08 % (3182833)Termination phase: Saturation
% 8.13/2.08 % (3182833)Time elapsed: 0.089 s
% 8.13/2.08 % (3182833)Peak memory usage: 89 MB
% 8.13/2.08 % (3182833)Instructions burned: 135 (million)
% 8.13/2.08 % (3182645)Also succeeded, but the first one will report.
% 8.13/2.08 % (3182835)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=145685191:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 8.13/2.08 % (3182743)Refutation found. Thanks to Tanya!
% 8.13/2.08 % SZS status Unsatisfiable for theBenchmark
% 8.13/2.08 % SZS output start Proof for theBenchmark
% See solution above
% 8.65/2.27 % (3182743)------------------------------
% 8.65/2.27 % (3182743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.65/2.27 % (3182743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.65/2.27 % (3182743)CaDiCaL version: 2.1.3
% 8.65/2.27 % (3182743)Termination reason: Refutation
% 8.65/2.27 % (3182743)Time elapsed: 0.449 s
% 8.65/2.27 % (3182743)Peak memory usage: 131 MB
% 8.65/2.27 % (3182743)Instructions burned: 1199 (million)
% 8.65/2.27 % (3182743)------------------------------
% 8.65/2.27 % (3182743)------------------------------
% 8.65/2.27 % (3182624)Success in time 1.128 s
% 8.65/2.27 % Vampire exiting
%------------------------------------------------------------------------------