%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO587+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:54:48 AM UTC 2026
% Result : Theorem 1.93s 0.89s
% Output : Refutation 1.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 17
% Syntax : Number of formulae : 100 ( 10 unt; 2 def)
% Number of atoms : 272 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 294 ( 122 ~; 117 |; 37 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 3 prp; 0-8 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-4 aty)
% Number of variables : 432 ( 0 sgn 411 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [X0,X1,X2,X3] :
( perp(X0,X1,X2,X3)
=> perp(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD8) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X0,X1,X2,X3)
& perp(X2,X3,X4,X5) )
=> para(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD9) ).
fof(f17,axiom,
! [X0,X1,X2,X3,X4] :
( ( cyclic(X0,X1,X2,X3)
& cyclic(X0,X1,X2,X4) )
=> cyclic(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD17) ).
fof(f18,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD18) ).
fof(f19,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD19) ).
fof(f21,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD21) ).
fof(f39,axiom,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD39) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
=> eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD40) ).
fof(f42,axiom,
! [X0,X1,X2,X3] :
( ( eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
& ~ coll(X2,X3,X0) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD42a) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
& coll(X2,X3,X1) )
=> cyclic(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f44,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( cyclic(X0,X1,X2,X3)
& cyclic(X0,X1,X2,X4)
& cyclic(X0,X1,X2,X5)
& eqangle(X2,X0,X2,X1,X5,X3,X5,X4) )
=> cong(X0,X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD43) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( circle(X3,X0,X1,X2)
& perp(X3,X0,X0,X4) )
=> eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD48) ).
fof(f58,axiom,
! [X0,X1,X2,X3] :
( ( cong(X0,X2,X1,X2)
& cong(X0,X3,X1,X3)
& cyclic(X0,X1,X2,X3) )
=> perp(X2,X0,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD57) ).
fof(f90,axiom,
! [X0,X1,X2,X3] :
? [X4] :
( ( perp(X0,X2,X2,X1)
& cyclic(X0,X1,X2,X3) )
=> circle(X4,X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX14) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( perp(X0,X1,X2,X3)
& midp(X4,X2,X0)
& midp(X5,X1,X2)
& midp(X6,X3,X1)
& midp(X7,X0,X3)
& coll(X8,X4,X6)
& coll(X8,X5,X7) )
=> cong(X8,X7,X8,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL416049) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( perp(X0,X1,X2,X3)
& midp(X4,X2,X0)
& midp(X5,X1,X2)
& midp(X6,X3,X1)
& midp(X7,X0,X3)
& coll(X8,X4,X6)
& coll(X8,X5,X7) )
=> cong(X8,X7,X8,X6) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X4,X5)
| ~ perp(X0,X1,X2,X3)
| ~ perp(X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f9]) ).
fof(f109,plain,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X4,X5)
| ~ perp(X0,X1,X2,X3)
| ~ perp(X2,X3,X4,X5) ),
inference(flattening,[],[f108]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4] :
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X3)
| ~ cyclic(X0,X1,X2,X4) ),
inference(ennf_transformation,[],[f17]) ).
fof(f121,plain,
! [X0,X1,X2,X3,X4] :
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X3)
| ~ cyclic(X0,X1,X2,X4) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X1,X0,X2,X3,X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f18]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X2,X3,X0,X1,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f19]) ).
fof(f125,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f21]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X2,X3)
| ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(ennf_transformation,[],[f39]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f40]) ).
fof(f151,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| coll(X2,X3,X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| coll(X2,X3,X0) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ coll(X2,X3,X1) ),
inference(ennf_transformation,[],[f43]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ coll(X2,X3,X1) ),
inference(flattening,[],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3,X4,X5] :
( cong(X0,X1,X3,X4)
| ~ cyclic(X0,X1,X2,X3)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4) ),
inference(ennf_transformation,[],[f44]) ).
fof(f156,plain,
! [X0,X1,X2,X3,X4,X5] :
( cong(X0,X1,X3,X4)
| ~ cyclic(X0,X1,X2,X3)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4) ),
inference(flattening,[],[f155]) ).
fof(f164,plain,
! [X0,X1,X2,X3,X4] :
( eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| ~ perp(X3,X0,X0,X4) ),
inference(ennf_transformation,[],[f49]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4] :
( eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ circle(X3,X0,X1,X2)
| ~ perp(X3,X0,X0,X4) ),
inference(flattening,[],[f164]) ).
fof(f182,plain,
! [X0,X1,X2,X3] :
( perp(X2,X0,X0,X3)
| ~ cong(X0,X2,X1,X2)
| ~ cong(X0,X3,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f58]) ).
fof(f183,plain,
! [X0,X1,X2,X3] :
( perp(X2,X0,X0,X3)
| ~ cong(X0,X2,X1,X2)
| ~ cong(X0,X3,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f182]) ).
fof(f239,plain,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X4,X0,X1,X2)
| ~ perp(X0,X2,X2,X1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f90]) ).
fof(f240,plain,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X4,X0,X1,X2)
| ~ perp(X0,X2,X2,X1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(flattening,[],[f239]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ cong(X8,X7,X8,X6)
& perp(X0,X1,X2,X3)
& midp(X4,X2,X0)
& midp(X5,X1,X2)
& midp(X6,X3,X1)
& midp(X7,X0,X3)
& coll(X8,X4,X6)
& coll(X8,X5,X7) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ cong(X8,X7,X8,X6)
& perp(X0,X1,X2,X3)
& midp(X4,X2,X0)
& midp(X5,X1,X2)
& midp(X6,X3,X1)
& midp(X7,X0,X3)
& coll(X8,X4,X6)
& coll(X8,X5,X7) ),
inference(flattening,[],[f249]) ).
fof(f258,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f259,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3)
| para(X0,X1,X4,X5) ),
inference(cnf_transformation,[],[f109]) ).
fof(f267,plain,
! [X2,X3,X0,X1,X4] :
( ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f121]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X1,X0,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f122]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X2,X3,X0,X1,X6,X7,X4,X5) ),
inference(cnf_transformation,[],[f123]) ).
fof(f271,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X0,X1,X4,X5,X2,X3,X6,X7) ),
inference(cnf_transformation,[],[f125]) ).
fof(f289,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f148]) ).
fof(f290,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| coll(X2,X3,X0)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f152]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ coll(X2,X3,X1)
| cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f294,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3)
| cong(X0,X1,X3,X4) ),
inference(cnf_transformation,[],[f156]) ).
fof(f299,plain,
! [X2,X3,X0,X1,X4] :
( ~ circle(X3,X0,X1,X2)
| ~ perp(X3,X0,X0,X4)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) ),
inference(cnf_transformation,[],[f165]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2)
| perp(X2,X0,X0,X3) ),
inference(cnf_transformation,[],[f183]) ).
fof(f356,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| ~ perp(X0,X2,X2,X1)
| circle(sK15(X0,X1,X2,X3),X0,X1,X2) ),
inference(cnf_transformation,[],[f240]) ).
fof(f370,plain,
perp(sK20,sK21,sK22,sK23),
inference(cnf_transformation,[],[f250]) ).
fof(f371,plain,
~ cong(sK28,sK27,sK28,sK26),
inference(cnf_transformation,[],[f250]) ).
fof(f465,plain,
perp(sK22,sK23,sK20,sK21),
inference(resolution,[],[f258,f370]) ).
fof(f476,plain,
! [X0,X1] :
( ~ perp(X0,X1,sK20,sK21)
| para(X0,X1,sK22,sK23) ),
inference(resolution,[],[f259,f370]) ).
fof(f501,plain,
para(sK22,sK23,sK22,sK23),
inference(resolution,[],[f476,f465]) ).
fof(f517,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X0,X1,X2,X3,X4,X5,X2,X3)
| ~ para(X1,X0,X4,X5) ),
inference(resolution,[],[f268,f290]) ).
fof(f523,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X2,X3)
| para(X1,X0,X2,X3) ),
inference(resolution,[],[f517,f289]) ).
fof(f543,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ para(X3,X2,X4,X5)
| eqangle(X0,X1,X2,X3,X0,X1,X4,X5) ),
inference(resolution,[],[f269,f517]) ).
fof(f544,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X0,X1,X2,X3,X0,X1,X4,X5)
| ~ para(X2,X3,X4,X5) ),
inference(resolution,[],[f269,f290]) ).
fof(f549,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X0,X1)
| para(X2,X3,X2,X3) ),
inference(resolution,[],[f544,f289]) ).
fof(f553,definition,
( spl29_1
<=> ! [X2,X3] : para(X2,X3,X2,X3) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f554,plain,
( ! [X2,X3] : para(X2,X3,X2,X3)
| ~ spl29_1 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f556,definition,
( spl29_2
<=> ! [X0,X1] : ~ para(X0,X1,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f557,plain,
( ! [X0,X1] : ~ para(X0,X1,X0,X1)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( spl29_1
| spl29_2 ),
inference(avatar_split_clause,[],[f549,f556,f553]) ).
fof(f563,plain,
( ! [X0,X1] : para(X0,X1,X1,X0)
| ~ spl29_1 ),
inference(resolution,[],[f554,f523]) ).
fof(f619,plain,
( ! [X2,X3,X0,X1] : eqangle(X0,X1,X2,X3,X0,X1,X3,X2)
| ~ spl29_1 ),
inference(resolution,[],[f543,f554]) ).
fof(f620,plain,
( ! [X2,X3,X0,X1] : eqangle(X0,X1,X2,X3,X0,X1,X2,X3)
| ~ spl29_1 ),
inference(resolution,[],[f543,f563]) ).
fof(f765,plain,
( ! [X2,X3,X0,X1] : eqangle(X0,X1,X0,X1,X2,X3,X2,X3)
| ~ spl29_1 ),
inference(resolution,[],[f271,f620]) ).
fof(f1416,plain,
( ! [X2,X0,X1] :
( cyclic(X2,X2,X0,X1)
| coll(X0,X1,X2) )
| ~ spl29_1 ),
inference(resolution,[],[f292,f765]) ).
fof(f1534,plain,
( ! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| cyclic(X2,X2,X0,X1) )
| ~ spl29_1 ),
inference(resolution,[],[f293,f765]) ).
fof(f1542,plain,
( ! [X2,X0,X1] : cyclic(X2,X2,X0,X1)
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f1534,f1416]) ).
fof(f1664,plain,
( ! [X2,X3,X0,X1] :
( ~ cyclic(X0,X0,X1,X2)
| cyclic(X0,X1,X2,X3) )
| ~ spl29_1 ),
inference(resolution,[],[f1542,f267]) ).
fof(f1671,plain,
( ! [X2,X3,X0,X1] : cyclic(X0,X1,X2,X3)
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f1664,f1542]) ).
fof(f4570,plain,
( ! [X2,X3,X0,X1] :
( ~ perp(X0,X2,X2,X1)
| circle(sK15(X0,X1,X2,X3),X0,X1,X2) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f356,f1671]) ).
fof(f4668,plain,
( ! [X2,X3,X0,X1] :
( ~ cong(X0,X2,X1,X2)
| ~ cong(X0,X3,X1,X3)
| perp(X2,X0,X0,X3) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f308,f1671]) ).
fof(f12269,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| cong(X0,X1,X3,X4) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f294,f1671]) ).
fof(f12270,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| cong(X0,X1,X3,X4) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f12269,f1671]) ).
fof(f12271,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| cong(X0,X1,X3,X4) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f12270,f1671]) ).
fof(f12367,plain,
( ! [X0,X1] : cong(X0,X1,X0,X1)
| ~ spl29_1 ),
inference(resolution,[],[f12271,f619]) ).
fof(f12442,plain,
( ! [X2,X0,X1] :
( ~ cong(X0,X1,X0,X1)
| perp(X2,X0,X0,X1) )
| ~ spl29_1 ),
inference(resolution,[],[f12367,f4668]) ).
fof(f12445,plain,
( ! [X2,X0,X1] : perp(X2,X0,X0,X1)
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f12442,f12367]) ).
fof(f12800,plain,
( ! [X2,X3,X0,X1] : circle(sK15(X0,X1,X2,X3),X0,X1,X2)
| ~ spl29_1 ),
inference(resolution,[],[f12445,f4570]) ).
fof(f12961,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ perp(sK15(X0,X1,X2,X3),X0,X0,X4)
| eqangle(X0,X4,X0,X1,X2,X0,X2,X1) )
| ~ spl29_1 ),
inference(resolution,[],[f12800,f299]) ).
fof(f12970,plain,
( ! [X2,X0,X1,X4] : eqangle(X0,X4,X0,X1,X2,X0,X2,X1)
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f12961,f12445]) ).
fof(f12973,plain,
( ! [X2,X3,X0,X1] : eqangle(X0,X1,X0,X2,X3,X1,X3,X0)
| ~ spl29_1 ),
inference(resolution,[],[f12970,f269]) ).
fof(f15175,plain,
( ! [X2,X0,X1] : cong(X0,X1,X0,X2)
| ~ spl29_1 ),
inference(resolution,[],[f12973,f12271]) ).
fof(f15180,plain,
( $false
| ~ spl29_1 ),
inference(resolution,[],[f15175,f371]) ).
fof(f15189,plain,
~ spl29_1,
inference(avatar_contradiction_clause,[],[f15180]) ).
fof(f16849,plain,
( $false
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f501,f557]) ).
fof(f16850,plain,
~ spl29_2,
inference(avatar_contradiction_clause,[],[f16849]) ).
cnf(s1,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f558]) ).
cnf(s69,plain,
~ spl29_1,
inference(sat_conversion,[],[f15189]) ).
cnf(s203,plain,
~ spl29_2,
inference(sat_conversion,[],[f16850]) ).
cnf(s204,plain,
$false,
inference(rat,[],[s1,s203,s69]) ).
fof(f16851,plain,
$false,
inference(avatar_sat_refutation,[],[s204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO587+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 % Computer : n011.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 08:34:30 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.42 Running first-order model finding
% 0.09/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.93/0.89 % (2096209)Will run a generic schedule for satisfiability detection.
% 1.93/0.89 % (2096217)dis+10_1_sil=32000:sp=arity:random_seed=1326394579:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.93/0.89 % (2096215)% WARNING: option uhcvi not known.
% 1.93/0.89 % (2096214)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3236719458_2999 on theBenchmark for (2999ds/0Mi)
% 1.93/0.89 % (2096215)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1070422654:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.93/0.89 % (2096216)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2088420921:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.93/0.89 % (2096218)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3510271225:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.93/0.89 % (2096219)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4281003483:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.93/0.89 % (2096220)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4243648998:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.93/0.89 % TRYING [1]
% 1.93/0.89 % TRYING [2]
% 1.93/0.89 % (2096217)Instruction limit reached!
% 1.93/0.89 % (2096217)------------------------------
% 1.93/0.89 % (2096217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096217)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096217)Termination reason: Instruction limit
% 1.93/0.89 % (2096217)Termination phase: Saturation
% 1.93/0.89 % (2096217)Time elapsed: 0.038 s
% 1.93/0.89 % (2096217)Peak memory usage: 13 MB
% 1.93/0.89 % (2096217)Instructions burned: 103 (million)
% 1.93/0.89 % TRYING [3]
% 1.93/0.89 % (2096228)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2160264884:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.93/0.89 % TRYING [1]
% 1.93/0.89 % TRYING [2]
% 1.93/0.89 % TRYING [3]
% 1.93/0.89 % (2096218)Instruction limit reached!
% 1.93/0.89 % (2096218)------------------------------
% 1.93/0.89 % (2096218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096218)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096218)Termination reason: Instruction limit
% 1.93/0.89 % (2096218)Termination phase: Saturation
% 1.93/0.89 % (2096218)Time elapsed: 0.071 s
% 1.93/0.89 % (2096218)Peak memory usage: 13 MB
% 1.93/0.89 % (2096218)Instructions burned: 119 (million)
% 1.93/0.89 % (2096219)Instruction limit reached!
% 1.93/0.89 % (2096219)------------------------------
% 1.93/0.89 % (2096219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096219)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096219)Termination reason: Instruction limit
% 1.93/0.89 % (2096219)Termination phase: Saturation
% 1.93/0.89 % (2096219)Time elapsed: 0.080 s
% 1.93/0.89 % (2096219)Peak memory usage: 14 MB
% 1.93/0.89 % (2096219)Instructions burned: 132 (million)
% 1.93/0.89 % (2096230)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=201944556:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.93/0.89 % (2096220)Instruction limit reached!
% 1.93/0.89 % (2096220)------------------------------
% 1.93/0.89 % (2096220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096220)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096220)Termination reason: Instruction limit
% 1.93/0.89 % (2096220)Termination phase: Saturation
% 1.93/0.89 % (2096220)Time elapsed: 0.094 s
% 1.93/0.89 % (2096220)Peak memory usage: 14 MB
% 1.93/0.89 % (2096220)Instructions burned: 159 (million)
% 1.93/0.89 % (2096231)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=853420638:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.93/0.89 % (2096233)ott-21_1_sil=16000:fs=off:random_seed=3579720734:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.93/0.89 % (2096230)Instruction limit reached!
% 1.93/0.89 % (2096230)------------------------------
% 1.93/0.89 % (2096230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096230)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096230)Termination reason: Instruction limit
% 1.93/0.89 % (2096230)Termination phase: Saturation
% 1.93/0.89 % (2096230)Time elapsed: 0.082 s
% 1.93/0.89 % (2096230)Peak memory usage: 14 MB
% 1.93/0.89 % (2096230)Instructions burned: 132 (million)
% 1.93/0.89 % (2096228)Instruction limit reached!
% 1.93/0.89 % (2096228)------------------------------
% 1.93/0.89 % (2096228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096228)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096228)Termination reason: Instruction limit
% 1.93/0.89 % (2096228)Termination phase: Finite model building constraint generation
% 1.93/0.89 % (2096228)Time elapsed: 0.133 s
% 1.93/0.89 % (2096228)Peak memory usage: 25 MB
% 1.93/0.89 % (2096228)Instructions burned: 719 (million)
% 1.93/0.89 % (2096237)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1486259003:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.93/0.89 % TRYING [1]
% 1.93/0.89 % TRYING [2]
% 1.93/0.89 % (2096236)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2905585247:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.93/0.89 % (2096233)Instruction limit reached!
% 1.93/0.89 % (2096233)------------------------------
% 1.93/0.89 % (2096233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096233)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096233)Termination reason: Instruction limit
% 1.93/0.89 % (2096233)Termination phase: Saturation
% 1.93/0.89 % (2096233)Time elapsed: 0.097 s
% 1.93/0.89 % (2096233)Peak memory usage: 13 MB
% 1.93/0.89 % (2096233)Instructions burned: 180 (million)
% 1.93/0.89 % TRYING [3]
% 1.93/0.89 % (2096240)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3758027000:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.93/0.89 % (2096237)Instruction limit reached!
% 1.93/0.89 % (2096237)------------------------------
% 1.93/0.89 % (2096237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096237)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096237)Termination reason: Instruction limit
% 1.93/0.89 % (2096237)Termination phase: Finite model building constraint generation
% 1.93/0.89 % (2096237)Time elapsed: 0.164 s
% 1.93/0.89 % (2096237)Peak memory usage: 51 MB
% 1.93/0.89 % (2096237)Instructions burned: 870 (million)
% 1.93/0.89 % (2096242)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2814299466:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 1.93/0.89 % (2096242)Cannot represent all propositional literals internally
% 1.93/0.89 % (2096242)Refutation not found, incomplete strategy
% 1.93/0.89 % (2096242)------------------------------
% 1.93/0.89 % (2096242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096242)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096242)Termination reason: Refutation not found, incomplete strategy
% 1.93/0.89 % (2096242)Time elapsed: 0.003 s
% 1.93/0.89 % (2096242)Peak memory usage: 10 MB
% 1.93/0.89 % (2096242)Instructions burned: 12 (million)
% 1.93/0.89 % (2096242)------------------------------
% 1.93/0.89 % (2096242)------------------------------
% 1.93/0.89 % (2096244)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=639573227:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 1.93/0.89 % (2096231) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2096209-2096231"...
% 1.93/0.89 % (2096231)...printing done.
% 1.93/0.89 % (2096231)Refutation found. Thanks to Tanya!
% 1.93/0.89 % SZS status Theorem for theBenchmark
% 1.93/0.89 % SZS output start Proof for theBenchmark
% See solution above
% 1.93/0.89 % (2096231)------------------------------
% 1.93/0.89 % (2096231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.89 % (2096231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.89 % (2096231)CaDiCaL version: 2.1.3
% 1.93/0.89 % (2096231)Termination reason: Refutation
% 1.93/0.89 % (2096231)Time elapsed: 0.311 s
% 1.93/0.89 % (2096231)Peak memory usage: 18 MB
% 1.93/0.89 % (2096231)Instructions burned: 540 (million)
% 1.93/0.89 % (2096209)Success in time 0.462 s
% 1.93/0.89 % Vampire exiting
%------------------------------------------------------------------------------