%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO643+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 : n014.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:56 AM UTC 2026
% Result : Theorem 13.21s 2.35s
% Output : Refutation 13.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 29
% Syntax : Number of formulae : 188 ( 22 unt; 10 def)
% Number of atoms : 431 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 433 ( 190 ~; 170 |; 43 &)
% ( 10 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 16 usr; 11 prp; 0-8 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-4 aty)
% Number of variables : 539 ( 0 sgn 517 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD2) ).
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( coll(X0,X1,X2)
& coll(X0,X1,X3) )
=> coll(X2,X3,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD3) ).
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(f14,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD14) ).
fof(f15,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X0,X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD15) ).
fof(f16,axiom,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X2,X3)
=> cyclic(X1,X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD16) ).
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(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(f20,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
=> eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD20) ).
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(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(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD66) ).
fof(f74,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
& para(X4,X5,X6,X7) )
=> para(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleD73) ).
fof(f87,axiom,
! [X0,X1,X2,X3] :
? [X4] :
( circle(X3,X0,X1,X2)
=> perp(X4,X0,X0,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax',ruleX11) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( coll(X2,X0,X1)
& coll(X4,X0,X3)
& coll(X5,X1,X4)
& coll(X5,X2,X3)
& circle(X6,X3,X4,X5)
& circle(X7,X0,X2,X3)
& circle(X8,X1,X2,X5)
& circle(X9,X1,X0,X4) )
=> cyclic(X8,X9,X7,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL81109109F) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( coll(X2,X0,X1)
& coll(X4,X0,X3)
& coll(X5,X1,X4)
& coll(X5,X2,X3)
& circle(X6,X3,X4,X5)
& circle(X7,X0,X2,X3)
& circle(X8,X1,X2,X5)
& circle(X9,X1,X0,X4) )
=> cyclic(X8,X9,X7,X6) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f98,plain,
! [X0,X1,X2] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f99,plain,
! [X0,X1,X2] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X2)
| ~ coll(X0,X1,X3) ),
inference(ennf_transformation,[],[f3]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X2)
| ~ coll(X0,X1,X3) ),
inference(flattening,[],[f100]) ).
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(f117,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X1,X3,X2)
| ~ cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( cyclic(X0,X2,X1,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f15]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( cyclic(X1,X0,X2,X3)
| ~ cyclic(X0,X1,X2,X3) ),
inference(ennf_transformation,[],[f16]) ).
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(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(f124,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X4,X5,X6,X7,X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f20]) ).
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(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(f197,plain,
! [X0,X1,X2] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(ennf_transformation,[],[f67]) ).
fof(f208,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( para(X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ para(X4,X5,X6,X7) ),
inference(ennf_transformation,[],[f74]) ).
fof(f209,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( para(X0,X1,X2,X3)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ para(X4,X5,X6,X7) ),
inference(flattening,[],[f208]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
? [X4] :
( perp(X4,X0,X0,X3)
| ~ circle(X3,X0,X1,X2) ),
inference(ennf_transformation,[],[f87]) ).
fof(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ cyclic(X8,X9,X7,X6)
& coll(X2,X0,X1)
& coll(X4,X0,X3)
& coll(X5,X1,X4)
& coll(X5,X2,X3)
& circle(X6,X3,X4,X5)
& circle(X7,X0,X2,X3)
& circle(X8,X1,X2,X5)
& circle(X9,X1,X0,X4) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ cyclic(X8,X9,X7,X6)
& coll(X2,X0,X1)
& coll(X4,X0,X3)
& coll(X5,X1,X4)
& coll(X5,X2,X3)
& circle(X6,X3,X4,X5)
& circle(X7,X0,X2,X3)
& circle(X8,X1,X2,X5)
& circle(X9,X1,X0,X4) ),
inference(flattening,[],[f249]) ).
fof(f262,plain,
! [X0,X1,X2,X3] :
( perp(sK11(X0,X1,X2,X3),X0,X0,X3)
| ~ circle(X3,X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X4,sK11(X0,X1,X2,X3))],[f234]) ).
fof(f270,plain,
( ~ cyclic(sK28,sK29,sK27,sK26)
& coll(sK22,sK20,sK21)
& coll(sK24,sK20,sK23)
& coll(sK25,sK21,sK24)
& coll(sK25,sK22,sK23)
& circle(sK26,sK23,sK24,sK25)
& circle(sK27,sK20,sK22,sK23)
& circle(sK28,sK21,sK22,sK25)
& circle(sK29,sK21,sK20,sK24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25),skolemize(X6,sK26),skolemize(X7,sK27),skolemize(X8,sK28),skolemize(X9,sK29)],[f250]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X0,X2,X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ coll(X0,X1,X2)
| coll(X1,X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2)
| coll(X2,X3,X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ perp(X0,X1,X2,X3)
| perp(X2,X3,X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f279,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(f284,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X1,X3,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f285,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X0,X2,X1,X3) ),
inference(cnf_transformation,[],[f118]) ).
fof(f286,plain,
! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X2,X3)
| cyclic(X1,X0,X2,X3) ),
inference(cnf_transformation,[],[f119]) ).
fof(f287,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(f289,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(f290,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| eqangle(X4,X5,X6,X7,X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f124]) ).
fof(f291,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(f309,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(f310,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(f313,plain,
! [X2,X3,X0,X1] :
( ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3)
| ~ coll(X2,X3,X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ para(X0,X1,X0,X2)
| coll(X0,X1,X2) ),
inference(cnf_transformation,[],[f197]) ).
fof(f344,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7)
| para(X0,X1,X2,X3)
| ~ para(X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f209]) ).
fof(f370,plain,
! [X2,X3,X0,X1] :
( perp(sK11(X0,X1,X2,X3),X0,X0,X3)
| ~ circle(X3,X0,X1,X2) ),
inference(cnf_transformation,[],[f262]) ).
fof(f384,plain,
circle(sK29,sK21,sK20,sK24),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
coll(sK24,sK20,sK23),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
~ cyclic(sK28,sK29,sK27,sK26),
inference(cnf_transformation,[],[f270]) ).
fof(f394,definition,
( spl30_1
<=> ! [X2,X0,X1] : coll(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f395,plain,
( ! [X2,X0,X1] : coll(X0,X2,X1)
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f401,plain,
coll(sK24,sK23,sK20),
inference(resolution,[],[f271,f390]) ).
fof(f430,definition,
( spl30_6
<=> ! [X2,X0,X1,X3] : ~ para(X0,X1,X2,X3) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
fof(f431,plain,
( ! [X2,X3,X0,X1] : ~ para(X0,X1,X2,X3)
| ~ spl30_6 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f443,definition,
( spl30_9
<=> ! [X2,X0,X1,X3] : cyclic(X0,X1,X3,X2) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
fof(f444,plain,
( ! [X2,X3,X0,X1] : cyclic(X0,X1,X3,X2)
| ~ spl30_9 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f469,plain,
coll(sK20,sK24,sK23),
inference(resolution,[],[f272,f390]) ).
fof(f547,plain,
! [X0] :
( ~ coll(sK20,sK24,X0)
| coll(X0,sK23,sK20) ),
inference(resolution,[],[f273,f469]) ).
fof(f560,plain,
! [X0] :
( ~ coll(sK24,sK20,X0)
| coll(X0,sK23,sK24) ),
inference(resolution,[],[f273,f390]) ).
fof(f562,plain,
! [X0] :
( ~ coll(sK24,sK23,X0)
| coll(X0,sK20,sK24) ),
inference(resolution,[],[f273,f401]) ).
fof(f637,definition,
( spl30_21
<=> ! [X0] : coll(X0,sK23,sK24) ),
introduced(definition,[new_symbols(definition,[spl30_21])],[avatar_definition]) ).
fof(f638,plain,
( ! [X0] : coll(X0,sK23,sK24)
| ~ spl30_21 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
coll(sK23,sK23,sK24),
inference(resolution,[],[f560,f390]) ).
fof(f649,plain,
( ! [X0] : coll(sK23,X0,sK24)
| ~ spl30_21 ),
inference(resolution,[],[f638,f272]) ).
fof(f650,plain,
( ! [X0] : coll(X0,sK24,sK23)
| ~ spl30_21 ),
inference(resolution,[],[f638,f271]) ).
fof(f653,plain,
( ! [X0] : coll(sK23,sK24,X0)
| ~ spl30_21 ),
inference(resolution,[],[f649,f271]) ).
fof(f655,plain,
( ! [X0,X1] :
( ~ coll(X0,sK24,X1)
| coll(X1,sK23,X0) )
| ~ spl30_21 ),
inference(resolution,[],[f650,f273]) ).
fof(f658,plain,
( ! [X0,X1] :
( ~ coll(sK23,sK24,X0)
| coll(X0,X1,sK23) )
| ~ spl30_21 ),
inference(resolution,[],[f653,f273]) ).
fof(f661,plain,
( ! [X0,X1] : coll(X0,X1,sK23)
| ~ spl30_21 ),
inference(forward_subsumption_resolution,[],[f658,f653]) ).
fof(f672,plain,
( ! [X0,X1] : coll(X0,sK23,X1)
| ~ spl30_21 ),
inference(resolution,[],[f661,f271]) ).
fof(f872,plain,
coll(sK23,sK24,sK23),
inference(resolution,[],[f639,f271]) ).
fof(f876,plain,
! [X0] :
( ~ coll(sK23,sK24,X0)
| coll(X0,sK23,sK23) ),
inference(resolution,[],[f872,f273]) ).
fof(f1171,definition,
( spl30_32
<=> ! [X0] : coll(X0,sK23,sK20) ),
introduced(definition,[new_symbols(definition,[spl30_32])],[avatar_definition]) ).
fof(f1172,plain,
( ! [X0] : coll(X0,sK23,sK20)
| ~ spl30_32 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1177,plain,
( ! [X0] : coll(sK23,X0,sK20)
| ~ spl30_32 ),
inference(resolution,[],[f1172,f272]) ).
fof(f1181,plain,
( ! [X0] : coll(sK23,sK20,X0)
| ~ spl30_32 ),
inference(resolution,[],[f1177,f271]) ).
fof(f1188,plain,
( ! [X0,X1] :
( ~ coll(sK23,sK20,X0)
| coll(X0,X1,sK23) )
| ~ spl30_32 ),
inference(resolution,[],[f1181,f273]) ).
fof(f1191,plain,
( ! [X0,X1] : coll(X0,X1,sK23)
| ~ spl30_32 ),
inference(forward_subsumption_resolution,[],[f1188,f1181]) ).
fof(f1206,plain,
( ! [X0,X1] : coll(X0,sK23,X1)
| ~ spl30_32 ),
inference(resolution,[],[f1191,f271]) ).
fof(f1554,definition,
( spl30_40
<=> ! [X0] : coll(X0,sK20,sK24) ),
introduced(definition,[new_symbols(definition,[spl30_40])],[avatar_definition]) ).
fof(f1555,plain,
( ! [X0] : coll(X0,sK20,sK24)
| ~ spl30_40 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1556,plain,
coll(sK20,sK20,sK24),
inference(resolution,[],[f562,f401]) ).
fof(f1563,plain,
( ! [X0] : coll(sK20,X0,sK24)
| ~ spl30_40 ),
inference(resolution,[],[f1555,f272]) ).
fof(f1571,plain,
( ! [X0] : coll(sK20,sK24,X0)
| ~ spl30_40 ),
inference(resolution,[],[f1563,f271]) ).
fof(f1587,plain,
( ! [X0] : coll(X0,sK23,sK20)
| ~ spl30_40 ),
inference(resolution,[],[f1571,f547]) ).
fof(f1618,plain,
( spl30_32
| ~ spl30_40 ),
inference(avatar_split_clause,[],[f1587,f1554,f1171]) ).
fof(f1619,plain,
! [X0] :
( ~ coll(sK20,sK20,X0)
| coll(X0,sK24,sK20) ),
inference(resolution,[],[f1556,f273]) ).
fof(f1889,definition,
( spl30_48
<=> ! [X0] : coll(X0,sK24,sK20) ),
introduced(definition,[new_symbols(definition,[spl30_48])],[avatar_definition]) ).
fof(f1890,plain,
( ! [X0] : coll(X0,sK24,sK20)
| ~ spl30_48 ),
inference(avatar_component_clause,[],[f1889]) ).
fof(f1902,plain,
( ! [X0] : coll(X0,sK20,sK24)
| ~ spl30_48 ),
inference(resolution,[],[f1890,f271]) ).
fof(f1911,plain,
( spl30_40
| ~ spl30_48 ),
inference(avatar_split_clause,[],[f1902,f1889,f1554]) ).
fof(f2432,plain,
! [X2,X3,X0,X1] :
( perp(X1,X0,sK11(X1,X2,X3,X0),X1)
| ~ circle(X0,X1,X2,X3) ),
inference(resolution,[],[f370,f278]) ).
fof(f2697,plain,
( ! [X0,X1] :
( ~ coll(X0,sK23,X1)
| coll(X1,sK20,X0) )
| ~ spl30_32 ),
inference(resolution,[],[f1172,f273]) ).
fof(f2706,plain,
( ! [X0,X1] : coll(X1,sK20,X0)
| ~ spl30_32 ),
inference(global_subsumption,[],[f2697,f1206]) ).
fof(f2745,plain,
( ! [X0] : coll(X0,sK23,sK24)
| ~ spl30_32 ),
inference(resolution,[],[f2706,f560]) ).
fof(f2835,plain,
( spl30_21
| ~ spl30_32 ),
inference(avatar_split_clause,[],[f2745,f1171,f637]) ).
fof(f2836,plain,
( ! [X0,X1] :
( ~ coll(X0,sK23,X1)
| coll(X1,sK24,X0) )
| ~ spl30_21 ),
inference(resolution,[],[f638,f273]) ).
fof(f2845,plain,
( ! [X0,X1] : coll(X1,sK24,X0)
| ~ spl30_21 ),
inference(global_subsumption,[],[f2836,f672]) ).
fof(f2987,plain,
( ! [X0,X1] : coll(X1,sK23,X0)
| ~ spl30_21 ),
inference(global_subsumption,[],[f2845,f655]) ).
fof(f3786,plain,
( $false
| ~ spl30_9 ),
inference(resolution,[],[f444,f392]) ).
fof(f3790,plain,
~ spl30_9,
inference(avatar_contradiction_clause,[],[f3786]) ).
fof(f3907,definition,
( spl30_81
<=> ! [X2,X0] : para(X2,X0,X2,X0) ),
introduced(definition,[new_symbols(definition,[spl30_81])],[avatar_definition]) ).
fof(f3908,plain,
( ! [X2,X0] : para(X2,X0,X2,X0)
| ~ spl30_81 ),
inference(avatar_component_clause,[],[f3907]) ).
fof(f3916,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X0,X1,X2,X3,X4,X5,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(resolution,[],[f310,f291]) ).
fof(f3918,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X4,X5,X0,X1,X4,X5,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(resolution,[],[f310,f289]) ).
fof(f3944,definition,
( spl30_83
<=> ! [X0] : coll(X0,sK23,sK23) ),
introduced(definition,[new_symbols(definition,[spl30_83])],[avatar_definition]) ).
fof(f3945,plain,
( ! [X0] : coll(X0,sK23,sK23)
| ~ spl30_83 ),
inference(avatar_component_clause,[],[f3944]) ).
fof(f3953,plain,
( ! [X0] : coll(sK23,X0,sK23)
| ~ spl30_83 ),
inference(resolution,[],[f3945,f272]) ).
fof(f3970,plain,
( ! [X0] : coll(sK23,sK23,X0)
| ~ spl30_83 ),
inference(resolution,[],[f3953,f271]) ).
fof(f3973,plain,
( ! [X0,X1] :
( ~ coll(sK23,sK23,X0)
| coll(X0,X1,sK23) )
| ~ spl30_83 ),
inference(resolution,[],[f3970,f273]) ).
fof(f3976,plain,
( ! [X0,X1] : coll(X0,X1,sK23)
| ~ spl30_83 ),
inference(forward_subsumption_resolution,[],[f3973,f3970]) ).
fof(f4370,plain,
( ! [X0,X1] : coll(X0,sK23,X1)
| ~ spl30_83 ),
inference(resolution,[],[f3976,f271]) ).
fof(f4402,plain,
( ! [X2,X0,X1] :
( ~ coll(X0,sK23,X1)
| coll(X1,X2,X0) )
| ~ spl30_83 ),
inference(resolution,[],[f4370,f273]) ).
fof(f4411,plain,
( ! [X2,X0,X1] : coll(X1,X2,X0)
| ~ spl30_83 ),
inference(forward_subsumption_resolution,[],[f4402,f4370]) ).
fof(f4422,plain,
( spl30_1
| ~ spl30_83 ),
inference(avatar_split_clause,[],[f4411,f3944,f394]) ).
fof(f5896,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X4,X5,X4,X5,X0,X1,X2,X3)
| ~ para(X0,X1,X2,X3) ),
inference(resolution,[],[f3916,f290]) ).
fof(f6091,plain,
( ! [X0,X1] :
( ~ coll(X0,sK23,X1)
| coll(X1,sK24,X0) )
| ~ spl30_21 ),
inference(resolution,[],[f638,f273]) ).
fof(f6108,plain,
( ! [X0,X1] : coll(X1,sK24,X0)
| ~ spl30_21 ),
inference(global_subsumption,[],[f6091,f2987]) ).
fof(f6232,plain,
( ! [X0] : coll(X0,sK23,sK23)
| ~ spl30_21 ),
inference(resolution,[],[f6108,f876]) ).
fof(f6953,plain,
( spl30_83
| ~ spl30_21 ),
inference(avatar_split_clause,[],[f6232,f637,f3944]) ).
fof(f7183,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X0,X1)
| para(X2,X3,X2,X3) ),
inference(resolution,[],[f3918,f309]) ).
fof(f14820,plain,
( ! [X0,X1] : coll(X0,X1,X1)
| ~ spl30_81 ),
inference(resolution,[],[f3908,f337]) ).
fof(f14822,plain,
( ! [X0,X1] : coll(X0,X1,X0)
| ~ spl30_81 ),
inference(resolution,[],[f14820,f272]) ).
fof(f15042,plain,
( ! [X0,X1] : coll(X0,X0,X1)
| ~ spl30_81 ),
inference(resolution,[],[f14822,f271]) ).
fof(f15266,plain,
( ! [X0] : coll(X0,sK24,sK20)
| ~ spl30_81 ),
inference(resolution,[],[f15042,f1619]) ).
fof(f15299,plain,
( spl30_48
| ~ spl30_81 ),
inference(avatar_split_clause,[],[f15266,f3907,f1889]) ).
fof(f21417,definition,
( spl30_116
<=> ! [X0,X1] : ~ para(X0,X1,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl30_116])],[avatar_definition]) ).
fof(f21418,plain,
( ! [X0,X1] : ~ para(X0,X1,X0,X1)
| ~ spl30_116 ),
inference(avatar_component_clause,[],[f21417]) ).
fof(f21419,plain,
( spl30_81
| spl30_116 ),
inference(avatar_split_clause,[],[f7183,f21417,f3907]) ).
fof(f21555,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ circle(X0,X1,X2,X3)
| ~ perp(X4,X5,X1,X0)
| para(X4,X5,sK11(X1,X2,X3,X0),X1) ),
inference(resolution,[],[f2432,f279]) ).
fof(f21558,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ circle(X0,X1,X2,X3)
| ~ perp(X4,X5,X1,X0) )
| ~ spl30_6 ),
inference(forward_subsumption_resolution,[],[f21555,f431]) ).
fof(f21559,plain,
( ! [X0,X1] : ~ perp(X0,X1,sK21,sK29)
| ~ spl30_6 ),
inference(resolution,[],[f21558,f384]) ).
fof(f21563,plain,
( ! [X0,X1] : ~ circle(sK29,sK21,X0,X1)
| ~ spl30_6 ),
inference(resolution,[],[f21559,f370]) ).
fof(f21567,plain,
( $false
| ~ spl30_6 ),
inference(resolution,[],[f21563,f384]) ).
fof(f21568,plain,
~ spl30_6,
inference(avatar_contradiction_clause,[],[f21567]) ).
fof(f22746,plain,
( ! [X2,X3,X0,X1] :
( ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) )
| ~ spl30_1 ),
inference(forward_subsumption_resolution,[],[f313,f395]) ).
fof(f27598,plain,
( ! [X2,X0,X1] :
( cyclic(X0,X1,X2,X2)
| ~ para(X2,X0,X2,X0) )
| ~ spl30_1 ),
inference(resolution,[],[f22746,f310]) ).
fof(f37540,plain,
( ! [X2,X0,X1] : cyclic(X0,X1,X2,X2)
| ~ spl30_1
| ~ spl30_81 ),
inference(forward_subsumption_resolution,[],[f27598,f3908]) ).
fof(f37543,plain,
( ! [X2,X0,X1] : cyclic(X0,X1,X2,X1)
| ~ spl30_1
| ~ spl30_81 ),
inference(resolution,[],[f37540,f285]) ).
fof(f37550,plain,
( ! [X2,X0,X1] : cyclic(X0,X1,X2,X0)
| ~ spl30_1
| ~ spl30_81 ),
inference(resolution,[],[f37543,f286]) ).
fof(f37560,plain,
( ! [X2,X0,X1] : cyclic(X0,X1,X0,X2)
| ~ spl30_1
| ~ spl30_81 ),
inference(resolution,[],[f37550,f284]) ).
fof(f37574,plain,
( ! [X2,X3,X0,X1] :
( ~ cyclic(X0,X1,X0,X2)
| cyclic(X1,X0,X2,X3) )
| ~ spl30_1
| ~ spl30_81 ),
inference(resolution,[],[f37560,f287]) ).
fof(f37582,plain,
( ! [X2,X3,X0,X1] : cyclic(X1,X0,X2,X3)
| ~ spl30_1
| ~ spl30_81 ),
inference(forward_subsumption_resolution,[],[f37574,f37560]) ).
fof(f37592,plain,
( spl30_9
| ~ spl30_1
| ~ spl30_81 ),
inference(avatar_split_clause,[],[f37582,f3907,f394,f443]) ).
fof(f63503,plain,
! [X2,X3,X0,X1,X4,X5] :
( para(X0,X1,X0,X1)
| ~ para(X2,X3,X4,X5)
| ~ para(X2,X3,X4,X5) ),
inference(resolution,[],[f344,f5896]) ).
fof(f64039,plain,
! [X2,X3,X0,X1,X4,X5] :
( para(X0,X1,X0,X1)
| ~ para(X2,X3,X4,X5) ),
inference(duplicate_literal_removal,[],[f63503]) ).
fof(f64087,plain,
( ! [X2,X3,X4,X5] : ~ para(X2,X3,X4,X5)
| ~ spl30_116 ),
inference(forward_subsumption_resolution,[],[f64039,f21418]) ).
fof(f64244,plain,
( spl30_6
| ~ spl30_116 ),
inference(avatar_split_clause,[],[f64087,f21417,f430]) ).
cnf(s1175,plain,
( spl30_32
| ~ spl30_40 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s1422,plain,
( spl30_40
| ~ spl30_48 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s2120,plain,
( spl30_21
| ~ spl30_32 ),
inference(sat_conversion,[],[f2835]) ).
cnf(s2799,plain,
~ spl30_9,
inference(sat_conversion,[],[f3790]) ).
cnf(s3216,plain,
( spl30_1
| ~ spl30_83 ),
inference(sat_conversion,[],[f4422]) ).
cnf(s4422,plain,
( ~ spl30_21
| spl30_83 ),
inference(sat_conversion,[],[f6953]) ).
cnf(s6185,plain,
( spl30_48
| ~ spl30_81 ),
inference(sat_conversion,[],[f15299]) ).
cnf(s6735,plain,
( spl30_81
| spl30_116 ),
inference(sat_conversion,[],[f21419]) ).
cnf(s6893,plain,
~ spl30_6,
inference(sat_conversion,[],[f21568]) ).
cnf(s16705,plain,
( ~ spl30_1
| spl30_9
| ~ spl30_81 ),
inference(sat_conversion,[],[f37592]) ).
cnf(s38041,plain,
( spl30_6
| ~ spl30_116 ),
inference(sat_conversion,[],[f64244]) ).
cnf(s38043,plain,
~ spl30_116,
inference(rat,[],[s38041,s6893]) ).
cnf(s38044,plain,
spl30_81,
inference(rat,[],[s6735,s38043]) ).
cnf(s38048,plain,
spl30_48,
inference(rat,[],[s6185,s38044]) ).
cnf(s38053,plain,
~ spl30_1,
inference(rat,[],[s16705,s38044,s2799]) ).
cnf(s38055,plain,
~ spl30_83,
inference(rat,[],[s3216,s38053]) ).
cnf(s38057,plain,
~ spl30_21,
inference(rat,[],[s4422,s38055]) ).
cnf(s38061,plain,
~ spl30_32,
inference(rat,[],[s2120,s38057]) ).
cnf(s38078,plain,
spl30_40,
inference(rat,[],[s1422,s38048]) ).
cnf(s38085,plain,
$false,
inference(rat,[],[s1175,s38078,s38061]) ).
fof(f64245,plain,
$false,
inference(avatar_sat_refutation,[],[s38085]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO643+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 08:42:31 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 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
% 6.86/1.45 % (508410)Will run a generic schedule for satisfiability detection.
% 6.86/1.45 % (508418)dis+10_1_sil=32000:sp=arity:random_seed=693133326:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.86/1.45 % (508416)% WARNING: option uhcvi not known.
% 6.86/1.45 % (508415)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3110103975_2999 on theBenchmark for (2999ds/0Mi)
% 6.86/1.45 % (508417)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3924943860:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.86/1.45 % (508419)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1623867492:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.86/1.45 % (508420)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3361993148:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.86/1.45 % (508421)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1881028083:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.86/1.45 % (508416)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1108819478:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.86/1.45 % TRYING [1]
% 6.86/1.45 % TRYING [2]
% 6.86/1.45 % (508418)Instruction limit reached!
% 6.86/1.45 % (508418)------------------------------
% 6.86/1.45 % (508418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.86/1.45 % (508418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.86/1.45 % (508418)CaDiCaL version: 2.1.3
% 6.86/1.45 % (508418)Termination reason: Instruction limit
% 6.86/1.45 % (508418)Termination phase: Saturation
% 6.86/1.45 % (508418)Time elapsed: 0.037 s
% 6.86/1.45 % (508418)Peak memory usage: 13 MB
% 6.86/1.45 % (508418)Instructions burned: 103 (million)
% 6.86/1.45 % (508429)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1557648809:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.86/1.45 % TRYING [1]
% 6.86/1.45 % TRYING [2]
% 6.86/1.45 % TRYING [3]
% 6.86/1.45 % (508419)Instruction limit reached!
% 6.86/1.45 % (508419)------------------------------
% 6.86/1.45 % (508419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.86/1.45 % (508419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.86/1.45 % (508419)CaDiCaL version: 2.1.3
% 6.86/1.45 % (508419)Termination reason: Instruction limit
% 6.86/1.45 % (508419)Termination phase: Saturation
% 6.86/1.45 % (508419)Time elapsed: 0.070 s
% 6.86/1.45 % (508419)Peak memory usage: 13 MB
% 6.86/1.45 % (508419)Instructions burned: 116 (million)
% 6.86/1.45 % TRYING [3]
% 6.86/1.45 % (508420)Instruction limit reached!
% 6.86/1.45 % (508420)------------------------------
% 6.86/1.45 % (508420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.86/1.45 % (508420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.86/1.45 % (508420)CaDiCaL version: 2.1.3
% 6.86/1.45 % (508420)Termination reason: Instruction limit
% 6.86/1.45 % (508420)Termination phase: Saturation
% 6.86/1.45 % (508420)Time elapsed: 0.083 s
% 6.86/1.45 % (508420)Peak memory usage: 14 MB
% 6.86/1.45 % (508420)Instructions burned: 132 (million)
% 6.86/1.45 % (508421)Instruction limit reached!
% 6.86/1.45 % (508421)------------------------------
% 6.86/1.45 % (508421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.86/1.45 % (508421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.86/1.45 % (508421)CaDiCaL version: 2.1.3
% 6.86/1.45 % (508421)Termination reason: Instruction limit
% 6.86/1.45 % (508421)Termination phase: Saturation
% 6.86/1.45 % (508421)Time elapsed: 0.090 s
% 6.86/1.45 % (508421)Peak memory usage: 14 MB
% 6.86/1.45 % (508421)Instructions burned: 160 (million)
% 6.86/1.45 % (508431)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=181203486:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.86/1.45 % (508432)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=860203994:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.86/1.45 % (508434)ott-21_1_sil=16000:fs=off:random_seed=1314033136:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.86/1.45 % (508431)Instruction limit reached!
% 6.86/1.45 % (508431)------------------------------
% 6.86/1.45 % (508431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.86/1.45 % (508431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508431)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508431)Termination reason: Instruction limit
% 13.21/2.35 % (508431)Termination phase: Saturation
% 13.21/2.35 % (508431)Time elapsed: 0.084 s
% 13.21/2.35 % (508431)Peak memory usage: 14 MB
% 13.21/2.35 % (508431)Instructions burned: 133 (million)
% 13.21/2.35 % (508429)Instruction limit reached!
% 13.21/2.35 % (508429)------------------------------
% 13.21/2.35 % (508429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508429)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508429)Termination reason: Instruction limit
% 13.21/2.35 % (508429)Termination phase: Finite model building constraint generation
% 13.21/2.35 % (508429)Time elapsed: 0.136 s
% 13.21/2.35 % (508429)Peak memory usage: 24 MB
% 13.21/2.35 % (508429)Instructions burned: 720 (million)
% 13.21/2.35 % (508438)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1130784230:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 13.21/2.35 % TRYING [1]
% 13.21/2.35 % TRYING [2]
% 13.21/2.35 % (508437)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2588370570:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.21/2.35 % (508434)Instruction limit reached!
% 13.21/2.35 % (508434)------------------------------
% 13.21/2.35 % (508434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508434)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508434)Termination reason: Instruction limit
% 13.21/2.35 % (508434)Termination phase: Saturation
% 13.21/2.35 % (508434)Time elapsed: 0.092 s
% 13.21/2.35 % (508434)Peak memory usage: 13 MB
% 13.21/2.35 % (508434)Instructions burned: 181 (million)
% 13.21/2.35 % (508441)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=662525301:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 13.21/2.35 % TRYING [3]
% 13.21/2.35 % (508438)Instruction limit reached!
% 13.21/2.35 % (508438)------------------------------
% 13.21/2.35 % (508438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508438)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508438)Termination reason: Instruction limit
% 13.21/2.35 % (508438)Termination phase: Finite model building constraint generation
% 13.21/2.35 % (508438)Time elapsed: 0.165 s
% 13.21/2.35 % (508438)Peak memory usage: 51 MB
% 13.21/2.35 % (508438)Instructions burned: 874 (million)
% 13.21/2.35 % (508443)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3438752869:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 13.21/2.35 % (508443)Cannot represent all propositional literals internally
% 13.21/2.35 % (508443)Refutation not found, incomplete strategy
% 13.21/2.35 % (508443)------------------------------
% 13.21/2.35 % (508443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508443)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508443)Termination reason: Refutation not found, incomplete strategy
% 13.21/2.35 % (508443)Time elapsed: 0.003 s
% 13.21/2.35 % (508443)Peak memory usage: 10 MB
% 13.21/2.35 % (508443)Instructions burned: 13 (million)
% 13.21/2.35 % (508443)------------------------------
% 13.21/2.35 % (508443)------------------------------
% 13.21/2.35 % (508445)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=1058226516: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)
% 13.21/2.35 % (508437)Instruction limit reached!
% 13.21/2.35 % (508437)------------------------------
% 13.21/2.35 % (508437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508437)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508437)Termination reason: Instruction limit
% 13.21/2.35 % (508437)Termination phase: Saturation
% 13.21/2.35 % (508437)Time elapsed: 0.284 s
% 13.21/2.35 % (508437)Peak memory usage: 15 MB
% 13.21/2.35 % (508437)Instructions burned: 478 (million)
% 13.21/2.35 % (508447)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2774090850:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 13.21/2.35 % (508432)Instruction limit reached!
% 13.21/2.35 % (508432)------------------------------
% 13.21/2.35 % (508432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508432)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508432)Termination reason: Instruction limit
% 13.21/2.35 % (508432)Termination phase: Saturation
% 13.21/2.35 % (508432)Time elapsed: 0.413 s
% 13.21/2.35 % (508432)Peak memory usage: 19 MB
% 13.21/2.35 % (508432)Instructions burned: 685 (million)
% 13.21/2.35 % (508449)fmb+10_1_sil=64000:random_seed=3861610875:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 13.21/2.35 % TRYING [1]
% 13.21/2.35 % TRYING [2]
% 13.21/2.35 % (508445)Instruction limit reached!
% 13.21/2.35 % (508445)------------------------------
% 13.21/2.35 % (508445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508445)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508445)Termination reason: Instruction limit
% 13.21/2.35 % (508445)Termination phase: Saturation
% 13.21/2.35 % (508445)Time elapsed: 0.221 s
% 13.21/2.35 % (508445)Peak memory usage: 21 MB
% 13.21/2.35 % (508445)Instructions burned: 693 (million)
% 13.21/2.35 % (508451)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4054814247:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 13.21/2.35 % (508451)Cannot represent all propositional literals internally
% 13.21/2.35 % (508451)Refutation not found, incomplete strategy
% 13.21/2.35 % (508451)------------------------------
% 13.21/2.35 % (508451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508451)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508451)Termination reason: Refutation not found, incomplete strategy
% 13.21/2.35 % (508451)Time elapsed: 0.003 s
% 13.21/2.35 % (508451)Peak memory usage: 10 MB
% 13.21/2.35 % (508451)Instructions burned: 13 (million)
% 13.21/2.35 % (508451)------------------------------
% 13.21/2.35 % (508451)------------------------------
% 13.21/2.35 % (508453)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=376782720:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 13.21/2.35 % TRYING [3]
% 13.21/2.35 % TRYING [8]
% 13.21/2.35 % (508453)Instruction limit reached!
% 13.21/2.35 % (508453)------------------------------
% 13.21/2.35 % (508453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508453)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508453)Termination reason: Instruction limit
% 13.21/2.35 % (508453)Termination phase: Finite model building constraint generation
% 13.21/2.35 % (508453)Time elapsed: 0.152 s
% 13.21/2.35 % (508453)Peak memory usage: 45 MB
% 13.21/2.35 % (508453)Instructions burned: 921 (million)
% 13.21/2.35 % (508455)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=810508857:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 13.21/2.35 % (508441)Instruction limit reached!
% 13.21/2.35 % (508441)------------------------------
% 13.21/2.35 % (508441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508441)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508441)Termination reason: Instruction limit
% 13.21/2.35 % (508441)Termination phase: Saturation
% 13.21/2.35 % (508441)Time elapsed: 0.726 s
% 13.21/2.35 % (508441)Peak memory usage: 25 MB
% 13.21/2.35 % (508441)Instructions burned: 1179 (million)
% 13.21/2.35 % (508457)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3418160885:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi)
% 13.21/2.35 % (508447)Instruction limit reached!
% 13.21/2.35 % (508447)------------------------------
% 13.21/2.35 % (508447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508447)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508447)Termination reason: Instruction limit
% 13.21/2.35 % (508447)Termination phase: Saturation
% 13.21/2.35 % (508447)Time elapsed: 0.473 s
% 13.21/2.35 % (508447)Peak memory usage: 18 MB
% 13.21/2.35 % (508447)Instructions burned: 880 (million)
% 13.21/2.35 % (508459)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=415992821:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 13.21/2.35 % (508459)Cannot represent all propositional literals internally
% 13.21/2.35 % (508459)Refutation not found, incomplete strategy
% 13.21/2.35 % (508459)------------------------------
% 13.21/2.35 % (508459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508459)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508459)Termination reason: Refutation not found, incomplete strategy
% 13.21/2.35 % (508459)Time elapsed: 0.008 s
% 13.21/2.35 % (508459)Peak memory usage: 11 MB
% 13.21/2.35 % (508459)Instructions burned: 16 (million)
% 13.21/2.35 % (508459)------------------------------
% 13.21/2.35 % (508459)------------------------------
% 13.21/2.35 % (508461)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=107493000:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 13.21/2.35 % (508461)Cannot represent all propositional literals internally
% 13.21/2.35 % (508461)Refutation not found, incomplete strategy
% 13.21/2.35 % (508461)------------------------------
% 13.21/2.35 % (508461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508461)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508461)Termination reason: Refutation not found, incomplete strategy
% 13.21/2.35 % (508461)Time elapsed: 0.082 s
% 13.21/2.35 % (508461)Peak memory usage: 12 MB
% 13.21/2.35 % (508461)Instructions burned: 166 (million)
% 13.21/2.35 % (508461)------------------------------
% 13.21/2.35 % (508461)------------------------------
% 13.21/2.35 % (508463)ott-2_1_sil=16000:newcnf=on:random_seed=916315366:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 13.21/2.35 % (508463)Instruction limit reached!
% 13.21/2.35 % (508463)------------------------------
% 13.21/2.35 % (508463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.35 % (508463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.35 % (508463)CaDiCaL version: 2.1.3
% 13.21/2.35 % (508463)Termination reason: Instruction limit
% 13.21/2.35 % (508463)Termination phase: Saturation
% 13.21/2.35 % (508463)Time elapsed: 0.539 s
% 13.21/2.35 % (508463)Peak memory usage: 17 MB
% 13.21/2.35 % (508463)Instructions burned: 869 (million)
% 13.21/2.35 % (508465)ott+10_1_sil=32000:tgt=ground:random_seed=1494916195:i=5114:av=off_2982 on theBenchmark for (2982ds/5114Mi)
% 13.21/2.35 % (508417) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-508410-508417"...
% 13.21/2.35 % (508417)...printing done.
% 13.21/2.35 % (508417)Refutation found. Thanks to Tanya!
% 13.21/2.35 % SZS status Theorem for theBenchmark
% 13.21/2.35 % SZS output start Proof for theBenchmark
% See solution above
% 13.21/2.36 % (508417)------------------------------
% 13.21/2.36 % (508417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.21/2.36 % (508417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.36 % (508417)CaDiCaL version: 2.1.3
% 13.21/2.36 % (508417)Termination reason: Refutation
% 13.21/2.36 % (508417)Time elapsed: 1.870 s
% 13.21/2.36 % (508417)Peak memory usage: 32 MB
% 13.21/2.36 % (508417)Instructions burned: 4270 (million)
% 13.21/2.36 % (508410)Success in time 1.948 s
% 13.21/2.36 % Vampire exiting
%------------------------------------------------------------------------------