%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO555+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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:54:43 AM UTC 2026
% Result : Theorem 2.38s 0.93s
% Output : Refutation 2.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 125 ( 21 unt; 6 def)
% Number of atoms : 316 ( 0 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 302 ( 111 ~; 98 |; 72 &)
% ( 6 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 7 prp; 0-8 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 322 ( 0 sgn 302 !; 20 ?)
% 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(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(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(f95,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X1,X0,X2)
& coll(X4,X0,X2)
& perp(X5,X2,X0,X1)
& coll(X5,X0,X1)
& perp(X6,X5,X1,X2)
& coll(X6,X1,X2)
& perp(X7,X5,X0,X2)
& coll(X7,X0,X2)
& perp(X8,X4,X0,X1)
& coll(X8,X0,X1)
& perp(X9,X3,X0,X1)
& coll(X9,X0,X1) )
=> cyclic(X7,X8,X9,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL012015) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X1,X0,X2)
& coll(X4,X0,X2)
& perp(X5,X2,X0,X1)
& coll(X5,X0,X1)
& perp(X6,X5,X1,X2)
& coll(X6,X1,X2)
& perp(X7,X5,X0,X2)
& coll(X7,X0,X2)
& perp(X8,X4,X0,X1)
& coll(X8,X0,X1)
& perp(X9,X3,X0,X1)
& coll(X9,X0,X1) )
=> cyclic(X7,X8,X9,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(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(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(f249,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ cyclic(X7,X8,X9,X6)
& perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X1,X0,X2)
& coll(X4,X0,X2)
& perp(X5,X2,X0,X1)
& coll(X5,X0,X1)
& perp(X6,X5,X1,X2)
& coll(X6,X1,X2)
& perp(X7,X5,X0,X2)
& coll(X7,X0,X2)
& perp(X8,X4,X0,X1)
& coll(X8,X0,X1)
& perp(X9,X3,X0,X1)
& coll(X9,X0,X1) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ cyclic(X7,X8,X9,X6)
& perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X1,X0,X2)
& coll(X4,X0,X2)
& perp(X5,X2,X0,X1)
& coll(X5,X0,X1)
& perp(X6,X5,X1,X2)
& coll(X6,X1,X2)
& perp(X7,X5,X0,X2)
& coll(X7,X0,X2)
& perp(X8,X4,X0,X1)
& coll(X8,X0,X1)
& perp(X9,X3,X0,X1)
& coll(X9,X0,X1) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( ~ cyclic(sK27,sK28,sK29,sK26)
& perp(sK23,sK20,sK21,sK22)
& coll(sK23,sK21,sK22)
& perp(sK24,sK21,sK20,sK22)
& coll(sK24,sK20,sK22)
& perp(sK25,sK22,sK20,sK21)
& coll(sK25,sK20,sK21)
& perp(sK26,sK25,sK21,sK22)
& coll(sK26,sK21,sK22)
& perp(sK27,sK25,sK20,sK22)
& coll(sK27,sK20,sK22)
& perp(sK28,sK24,sK20,sK21)
& coll(sK28,sK20,sK21)
& perp(sK29,sK23,sK20,sK21)
& coll(sK29,sK20,sK21) ),
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(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(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(f389,plain,
perp(sK27,sK25,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f392,plain,
coll(sK25,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f393,plain,
perp(sK25,sK22,sK20,sK21),
inference(cnf_transformation,[],[f270]) ).
fof(f398,plain,
~ cyclic(sK27,sK28,sK29,sK26),
inference(cnf_transformation,[],[f270]) ).
fof(f400,definition,
( spl30_1
<=> ! [X2,X0,X1] : coll(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f401,plain,
( ! [X2,X0,X1] : coll(X0,X2,X1)
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f407,plain,
coll(sK25,sK21,sK20),
inference(resolution,[],[f271,f392]) ).
fof(f697,plain,
perp(sK20,sK21,sK25,sK22),
inference(resolution,[],[f278,f393]) ).
fof(f698,plain,
perp(sK20,sK22,sK27,sK25),
inference(resolution,[],[f278,f389]) ).
fof(f964,plain,
! [X0,X1] :
( ~ perp(X0,X1,sK25,sK22)
| para(X0,X1,sK20,sK21) ),
inference(resolution,[],[f279,f393]) ).
fof(f1011,plain,
! [X0,X1] :
( ~ perp(X0,X1,sK20,sK22)
| para(X0,X1,sK27,sK25) ),
inference(resolution,[],[f279,f698]) ).
fof(f1023,plain,
para(sK20,sK21,sK20,sK21),
inference(resolution,[],[f964,f697]) ).
fof(f1066,definition,
( spl30_30
<=> ! [X2,X0] : ~ para(X0,X2,X0,X2) ),
introduced(definition,[new_symbols(definition,[spl30_30])],[avatar_definition]) ).
fof(f1067,plain,
( ! [X2,X0] : ~ para(X0,X2,X0,X2)
| ~ spl30_30 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1068,plain,
( $false
| ~ spl30_30 ),
inference(forward_subsumption_resolution,[],[f1023,f1067]) ).
fof(f1069,plain,
~ spl30_30,
inference(avatar_contradiction_clause,[],[f1068]) ).
fof(f1448,plain,
! [X0] :
( ~ coll(sK25,sK20,X0)
| coll(X0,sK21,sK25) ),
inference(resolution,[],[f273,f392]) ).
fof(f1467,plain,
! [X0] :
( ~ coll(sK25,sK21,X0)
| coll(X0,sK20,sK25) ),
inference(resolution,[],[f273,f407]) ).
fof(f2823,plain,
para(sK27,sK25,sK27,sK25),
inference(resolution,[],[f1011,f389]) ).
fof(f4580,definition,
( spl30_110
<=> ! [X0,X1] : para(X0,X1,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl30_110])],[avatar_definition]) ).
fof(f4581,plain,
( ! [X0,X1] : para(X0,X1,X0,X1)
| ~ spl30_110 ),
inference(avatar_component_clause,[],[f4580]) ).
fof(f4790,plain,
! [X2,X3,X0,X1,X4,X5] :
( eqangle(X0,X1,X2,X3,X0,X1,X4,X5)
| ~ para(X2,X3,X4,X5) ),
inference(resolution,[],[f289,f310]) ).
fof(f4799,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X0,X1)
| para(X2,X3,X2,X3) ),
inference(resolution,[],[f4790,f309]) ).
fof(f6016,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,f401]) ).
fof(f6071,plain,
( ! [X2,X0,X1] :
( ~ para(X2,X0,X2,X0)
| cyclic(X0,X1,X2,X2) )
| ~ spl30_1 ),
inference(resolution,[],[f6016,f310]) ).
fof(f6295,plain,
( ! [X0] : cyclic(sK25,X0,sK27,sK27)
| ~ spl30_1 ),
inference(resolution,[],[f6071,f2823]) ).
fof(f6335,plain,
( ! [X0] : cyclic(sK25,sK27,X0,sK27)
| ~ spl30_1 ),
inference(resolution,[],[f6295,f285]) ).
fof(f6449,plain,
( ! [X0] : cyclic(sK25,sK27,sK27,X0)
| ~ spl30_1 ),
inference(resolution,[],[f6335,f284]) ).
fof(f6803,plain,
( ! [X0,X1] :
( ~ cyclic(sK25,sK27,sK27,X0)
| cyclic(sK27,sK27,X0,X1) )
| ~ spl30_1 ),
inference(resolution,[],[f6449,f287]) ).
fof(f6808,plain,
( ! [X0,X1] : cyclic(sK27,sK27,X0,X1)
| ~ spl30_1 ),
inference(forward_subsumption_resolution,[],[f6803,f6449]) ).
fof(f7624,plain,
( ! [X2,X0,X1] :
( ~ cyclic(sK27,sK27,X0,X1)
| cyclic(sK27,X0,X1,X2) )
| ~ spl30_1 ),
inference(resolution,[],[f6808,f287]) ).
fof(f7629,plain,
( ! [X2,X0,X1] : cyclic(sK27,X0,X1,X2)
| ~ spl30_1 ),
inference(forward_subsumption_resolution,[],[f7624,f6808]) ).
fof(f8195,plain,
( $false
| ~ spl30_1 ),
inference(resolution,[],[f7629,f398]) ).
fof(f8201,plain,
~ spl30_1,
inference(avatar_contradiction_clause,[],[f8195]) ).
fof(f8235,definition,
( spl30_135
<=> ! [X0] : coll(X0,sK21,sK25) ),
introduced(definition,[new_symbols(definition,[spl30_135])],[avatar_definition]) ).
fof(f8236,plain,
( ! [X0] : coll(X0,sK21,sK25)
| ~ spl30_135 ),
inference(avatar_component_clause,[],[f8235]) ).
fof(f8241,plain,
( ! [X0] : coll(sK21,X0,sK25)
| ~ spl30_135 ),
inference(resolution,[],[f8236,f272]) ).
fof(f8245,plain,
( ! [X0] : coll(sK21,sK25,X0)
| ~ spl30_135 ),
inference(resolution,[],[f8241,f271]) ).
fof(f8250,plain,
( ! [X0,X1] :
( ~ coll(sK21,sK25,X0)
| coll(X0,X1,sK21) )
| ~ spl30_135 ),
inference(resolution,[],[f8245,f273]) ).
fof(f8253,plain,
( ! [X0,X1] : coll(X0,X1,sK21)
| ~ spl30_135 ),
inference(forward_subsumption_resolution,[],[f8250,f8245]) ).
fof(f8264,plain,
( ! [X0,X1] : coll(X0,sK21,X1)
| ~ spl30_135 ),
inference(resolution,[],[f8253,f271]) ).
fof(f8316,plain,
( ! [X2,X0,X1] :
( ~ coll(X0,sK21,X1)
| coll(X1,X2,X0) )
| ~ spl30_135 ),
inference(resolution,[],[f8264,f273]) ).
fof(f8319,plain,
( ! [X2,X0,X1] : coll(X1,X2,X0)
| ~ spl30_135 ),
inference(forward_subsumption_resolution,[],[f8316,f8264]) ).
fof(f8360,plain,
( spl30_1
| ~ spl30_135 ),
inference(avatar_split_clause,[],[f8319,f8235,f400]) ).
fof(f9187,definition,
( spl30_150
<=> ! [X0] : coll(X0,sK20,sK25) ),
introduced(definition,[new_symbols(definition,[spl30_150])],[avatar_definition]) ).
fof(f9188,plain,
( ! [X0] : coll(X0,sK20,sK25)
| ~ spl30_150 ),
inference(avatar_component_clause,[],[f9187]) ).
fof(f9189,plain,
coll(sK20,sK20,sK25),
inference(resolution,[],[f1467,f407]) ).
fof(f9197,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl30_150 ),
inference(resolution,[],[f9188,f271]) ).
fof(f9208,plain,
( ! [X0] : coll(sK25,X0,sK20)
| ~ spl30_150 ),
inference(resolution,[],[f9197,f272]) ).
fof(f9236,plain,
( ! [X0] : coll(sK25,sK20,X0)
| ~ spl30_150 ),
inference(resolution,[],[f9208,f271]) ).
fof(f9249,plain,
( ! [X0] : coll(X0,sK21,sK25)
| ~ spl30_150 ),
inference(global_subsumption,[],[f9236,f1448]) ).
fof(f9381,plain,
( spl30_135
| ~ spl30_150 ),
inference(avatar_split_clause,[],[f9249,f9187,f8235]) ).
fof(f9382,plain,
! [X0] :
( ~ coll(sK20,sK20,X0)
| coll(X0,sK25,sK20) ),
inference(resolution,[],[f9189,f273]) ).
fof(f10668,definition,
( spl30_174
<=> ! [X0] : coll(X0,sK25,sK20) ),
introduced(definition,[new_symbols(definition,[spl30_174])],[avatar_definition]) ).
fof(f10669,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl30_174 ),
inference(avatar_component_clause,[],[f10668]) ).
fof(f10687,plain,
( ! [X0] : coll(X0,sK20,sK25)
| ~ spl30_174 ),
inference(resolution,[],[f10669,f271]) ).
fof(f10695,plain,
( spl30_150
| ~ spl30_174 ),
inference(avatar_split_clause,[],[f10687,f10668,f9187]) ).
fof(f38142,plain,
( ! [X0,X1] : coll(X0,X1,X1)
| ~ spl30_110 ),
inference(resolution,[],[f4581,f337]) ).
fof(f38248,plain,
( ! [X0,X1] : coll(X0,X1,X0)
| ~ spl30_110 ),
inference(resolution,[],[f38142,f272]) ).
fof(f39252,plain,
( ! [X0,X1] : coll(X0,X0,X1)
| ~ spl30_110 ),
inference(resolution,[],[f38248,f271]) ).
fof(f40259,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl30_110 ),
inference(resolution,[],[f39252,f9382]) ).
fof(f40357,plain,
( spl30_174
| ~ spl30_110 ),
inference(avatar_split_clause,[],[f40259,f4580,f10668]) ).
fof(f42488,plain,
( spl30_110
| spl30_30 ),
inference(avatar_split_clause,[],[f4799,f1066,f4580]) ).
cnf(s754,plain,
~ spl30_30,
inference(sat_conversion,[],[f1069]) ).
cnf(s5046,plain,
~ spl30_1,
inference(sat_conversion,[],[f8201]) ).
cnf(s5245,plain,
( spl30_1
| ~ spl30_135 ),
inference(sat_conversion,[],[f8360]) ).
cnf(s6103,plain,
( spl30_135
| ~ spl30_150 ),
inference(sat_conversion,[],[f9381]) ).
cnf(s7081,plain,
( spl30_150
| ~ spl30_174 ),
inference(sat_conversion,[],[f10695]) ).
cnf(s16862,plain,
( ~ spl30_110
| spl30_174 ),
inference(sat_conversion,[],[f40357]) ).
cnf(s16991,plain,
( spl30_30
| spl30_110 ),
inference(sat_conversion,[],[f42488]) ).
cnf(s16999,plain,
~ spl30_135,
inference(rat,[],[s5245,s5046]) ).
cnf(s17016,plain,
~ spl30_150,
inference(rat,[],[s6103,s16999]) ).
cnf(s17054,plain,
~ spl30_174,
inference(rat,[],[s7081,s17016]) ).
cnf(s17083,plain,
~ spl30_110,
inference(rat,[],[s16862,s17054]) ).
cnf(s17094,plain,
spl30_30,
inference(rat,[],[s16991,s17083]) ).
cnf(s17108,plain,
$false,
inference(rat,[],[s754,s17094]) ).
fof(f42489,plain,
$false,
inference(avatar_sat_refutation,[],[s17108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO555+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.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 08:35:25 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 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
% 2.38/0.93 % (2322072)Will run a generic schedule for satisfiability detection.
% 2.38/0.93 % (2322079)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=224238389:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.38/0.93 % (2322078)% WARNING: option uhcvi not known.
% 2.38/0.93 % (2322078)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1938557347:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.38/0.93 % (2322077)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2516596210_2999 on theBenchmark for (2999ds/0Mi)
% 2.38/0.93 % (2322080)dis+10_1_sil=32000:sp=arity:random_seed=677899973:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.38/0.93 % (2322081)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=834031167:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.38/0.93 % (2322083)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3015181529:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.38/0.93 % (2322082)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1105609391:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.38/0.93 % TRYING [1]
% 2.38/0.93 % TRYING [2]
% 2.38/0.93 % TRYING [3]
% 2.38/0.93 % (2322080)Instruction limit reached!
% 2.38/0.93 % (2322080)------------------------------
% 2.38/0.93 % (2322080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322080)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322080)Termination reason: Instruction limit
% 2.38/0.93 % (2322080)Termination phase: Saturation
% 2.38/0.93 % (2322080)Time elapsed: 0.067 s
% 2.38/0.93 % (2322080)Peak memory usage: 12 MB
% 2.38/0.93 % (2322080)Instructions burned: 103 (million)
% 2.38/0.93 % (2322081)Instruction limit reached!
% 2.38/0.93 % (2322081)------------------------------
% 2.38/0.93 % (2322081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322081)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322081)Termination reason: Instruction limit
% 2.38/0.93 % (2322081)Termination phase: Saturation
% 2.38/0.93 % (2322081)Time elapsed: 0.068 s
% 2.38/0.93 % (2322081)Peak memory usage: 13 MB
% 2.38/0.93 % (2322081)Instructions burned: 117 (million)
% 2.38/0.93 % (2322082)Instruction limit reached!
% 2.38/0.93 % (2322082)------------------------------
% 2.38/0.93 % (2322082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322082)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322082)Termination reason: Instruction limit
% 2.38/0.93 % (2322082)Termination phase: Saturation
% 2.38/0.93 % (2322082)Time elapsed: 0.079 s
% 2.38/0.93 % (2322082)Peak memory usage: 14 MB
% 2.38/0.93 % (2322082)Instructions burned: 131 (million)
% 2.38/0.93 % (2322091)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4025847392:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 2.38/0.93 % (2322092)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1731007063:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.38/0.93 % (2322083)Instruction limit reached!
% 2.38/0.93 % (2322083)------------------------------
% 2.38/0.93 % (2322083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322083)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322083)Termination reason: Instruction limit
% 2.38/0.93 % (2322083)Termination phase: Saturation
% 2.38/0.93 % (2322083)Time elapsed: 0.092 s
% 2.38/0.93 % (2322083)Peak memory usage: 14 MB
% 2.38/0.93 % (2322083)Instructions burned: 160 (million)
% 2.38/0.93 % TRYING [1]
% 2.38/0.93 % TRYING [2]
% 2.38/0.93 % (2322093)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=417563041:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.38/0.93 % (2322096)ott-21_1_sil=16000:fs=off:random_seed=160304711:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.38/0.93 % TRYING [3]
% 2.38/0.93 % (2322092)Instruction limit reached!
% 2.38/0.93 % (2322092)------------------------------
% 2.38/0.93 % (2322092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322092)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322092)Termination reason: Instruction limit
% 2.38/0.93 % (2322092)Termination phase: Saturation
% 2.38/0.93 % (2322092)Time elapsed: 0.081 s
% 2.38/0.93 % (2322092)Peak memory usage: 14 MB
% 2.38/0.93 % (2322092)Instructions burned: 132 (million)
% 2.38/0.93 % (2322099)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3878418807:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 2.38/0.93 % (2322096)Instruction limit reached!
% 2.38/0.93 % (2322096)------------------------------
% 2.38/0.93 % (2322096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322096)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322096)Termination reason: Instruction limit
% 2.38/0.93 % (2322096)Termination phase: Saturation
% 2.38/0.93 % (2322096)Time elapsed: 0.093 s
% 2.38/0.93 % (2322096)Peak memory usage: 13 MB
% 2.38/0.93 % (2322096)Instructions burned: 183 (million)
% 2.38/0.93 % (2322101)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=210614780:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.38/0.93 % TRYING [1]
% 2.38/0.93 % TRYING [2]
% 2.38/0.93 % TRYING [3]
% 2.38/0.93 % (2322091)Instruction limit reached!
% 2.38/0.93 % (2322091)------------------------------
% 2.38/0.93 % (2322091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322091)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322091)Termination reason: Instruction limit
% 2.38/0.93 % (2322091)Termination phase: Finite model building constraint generation
% 2.38/0.93 % (2322091)Time elapsed: 0.250 s
% 2.38/0.93 % (2322091)Peak memory usage: 24 MB
% 2.38/0.93 % (2322091)Instructions burned: 714 (million)
% 2.38/0.93 % (2322103)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3730682498:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 2.38/0.93 % (2322079) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2322072-2322079"...
% 2.38/0.93 % (2322079)...printing done.
% 2.38/0.93 % (2322079)Refutation found. Thanks to Tanya!
% 2.38/0.93 % SZS status Theorem for theBenchmark
% 2.38/0.93 % SZS output start Proof for theBenchmark
% See solution above
% 2.38/0.93 % (2322079)------------------------------
% 2.38/0.93 % (2322079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.93 % (2322079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.93 % (2322079)CaDiCaL version: 2.1.3
% 2.38/0.93 % (2322079)Termination reason: Refutation
% 2.38/0.93 % (2322079)Time elapsed: 0.475 s
% 2.38/0.93 % (2322079)Peak memory usage: 31 MB
% 2.38/0.93 % (2322079)Instructions burned: 1625 (million)
% 2.38/0.93 % (2322072)Success in time 0.518 s
% 2.38/0.93 % Vampire exiting
%------------------------------------------------------------------------------