%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO567+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:45 AM UTC 2026
% Result : Theorem 1.95s 0.84s
% Output : Refutation 1.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 20
% Syntax : Number of formulae : 121 ( 18 unt; 6 def)
% Number of atoms : 271 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 260 ( 110 ~; 97 |; 32 &)
% ( 6 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 7 prp; 0-8 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 304 ( 0 sgn 292 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD1) ).
fof(f2,axiom,
! [X0,X1,X2] :
( coll(X0,X1,X2)
=> coll(X1,X0,X2) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD42b) ).
fof(f67,axiom,
! [X0,X1,X2] :
( para(X0,X1,X0,X2)
=> coll(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax',ruleD66) ).
fof(f95,conjecture,
! [X0,X1,X2,X3,X4,X5] :
( ( perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X3,X0,X1)
& coll(X4,X0,X1)
& perp(X5,X3,X0,X2)
& coll(X5,X0,X2) )
=> cyclic(X1,X4,X5,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL214029) ).
fof(f96,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5] :
( ( perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X3,X0,X1)
& coll(X4,X0,X1)
& perp(X5,X3,X0,X2)
& coll(X5,X0,X2) )
=> cyclic(X1,X4,X5,X2) ),
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] :
( ~ cyclic(X1,X4,X5,X2)
& perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X3,X0,X1)
& coll(X4,X0,X1)
& perp(X5,X3,X0,X2)
& coll(X5,X0,X2) ),
inference(ennf_transformation,[],[f96]) ).
fof(f250,plain,
? [X0,X1,X2,X3,X4,X5] :
( ~ cyclic(X1,X4,X5,X2)
& perp(X3,X0,X1,X2)
& coll(X3,X1,X2)
& perp(X4,X3,X0,X1)
& coll(X4,X0,X1)
& perp(X5,X3,X0,X2)
& coll(X5,X0,X2) ),
inference(flattening,[],[f249]) ).
fof(f270,plain,
( ~ cyclic(sK21,sK24,sK25,sK22)
& perp(sK23,sK20,sK21,sK22)
& coll(sK23,sK21,sK22)
& perp(sK24,sK23,sK20,sK21)
& coll(sK24,sK20,sK21)
& perp(sK25,sK23,sK20,sK22)
& coll(sK25,sK20,sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23,sK24,sK25]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22),skolemize(X3,sK23),skolemize(X4,sK24),skolemize(X5,sK25)],[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] :
( cyclic(X0,X1,X2,X3)
| ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ 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(f384,plain,
coll(sK25,sK20,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f389,plain,
perp(sK23,sK20,sK21,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f390,plain,
~ cyclic(sK21,sK24,sK25,sK22),
inference(cnf_transformation,[],[f270]) ).
fof(f392,definition,
( spl26_1
<=> ! [X2,X0,X1] : coll(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
fof(f393,plain,
( ! [X2,X0,X1] : coll(X0,X2,X1)
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f397,plain,
coll(sK25,sK22,sK20),
inference(resolution,[],[f271,f384]) ).
fof(f619,plain,
perp(sK21,sK22,sK23,sK20),
inference(resolution,[],[f278,f389]) ).
fof(f793,plain,
! [X0,X1] :
( ~ perp(X0,X1,sK23,sK20)
| para(X0,X1,sK21,sK22) ),
inference(resolution,[],[f279,f389]) ).
fof(f828,plain,
para(sK21,sK22,sK21,sK22),
inference(resolution,[],[f793,f619]) ).
fof(f880,definition,
( spl26_30
<=> ! [X2,X0] : ~ para(X0,X2,X0,X2) ),
introduced(definition,[new_symbols(definition,[spl26_30])],[avatar_definition]) ).
fof(f881,plain,
( ! [X2,X0] : ~ para(X0,X2,X0,X2)
| ~ spl26_30 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f894,plain,
( $false
| ~ spl26_30 ),
inference(forward_subsumption_resolution,[],[f828,f881]) ).
fof(f895,plain,
~ spl26_30,
inference(avatar_contradiction_clause,[],[f894]) ).
fof(f997,plain,
! [X0] :
( ~ coll(sK25,sK20,X0)
| coll(X0,sK22,sK25) ),
inference(resolution,[],[f273,f384]) ).
fof(f1015,plain,
! [X0] :
( ~ coll(sK25,sK22,X0)
| coll(X0,sK20,sK25) ),
inference(resolution,[],[f273,f397]) ).
fof(f1087,definition,
( spl26_35
<=> ! [X0] : coll(X0,sK22,sK25) ),
introduced(definition,[new_symbols(definition,[spl26_35])],[avatar_definition]) ).
fof(f1088,plain,
( ! [X0] : coll(X0,sK22,sK25)
| ~ spl26_35 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1099,plain,
( ! [X0] : coll(sK22,X0,sK25)
| ~ spl26_35 ),
inference(resolution,[],[f1088,f272]) ).
fof(f1103,plain,
( ! [X0] : coll(sK22,sK25,X0)
| ~ spl26_35 ),
inference(resolution,[],[f1099,f271]) ).
fof(f1108,plain,
( ! [X0,X1] :
( ~ coll(sK22,sK25,X0)
| coll(X0,X1,sK22) )
| ~ spl26_35 ),
inference(resolution,[],[f1103,f273]) ).
fof(f1111,plain,
( ! [X0,X1] : coll(X0,X1,sK22)
| ~ spl26_35 ),
inference(forward_subsumption_resolution,[],[f1108,f1103]) ).
fof(f1122,plain,
( ! [X0,X1] : coll(X0,sK22,X1)
| ~ spl26_35 ),
inference(resolution,[],[f1111,f271]) ).
fof(f1132,plain,
( ! [X2,X0,X1] :
( ~ coll(X0,sK22,X1)
| coll(X1,X2,X0) )
| ~ spl26_35 ),
inference(resolution,[],[f1122,f273]) ).
fof(f1135,plain,
( ! [X2,X0,X1] : coll(X1,X2,X0)
| ~ spl26_35 ),
inference(forward_subsumption_resolution,[],[f1132,f1122]) ).
fof(f1143,plain,
( spl26_1
| ~ spl26_35 ),
inference(avatar_split_clause,[],[f1135,f1087,f392]) ).
fof(f7632,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(f11401,definition,
( spl26_97
<=> ! [X0,X1] : para(X0,X1,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl26_97])],[avatar_definition]) ).
fof(f11402,plain,
( ! [X0,X1] : para(X0,X1,X0,X1)
| ~ spl26_97 ),
inference(avatar_component_clause,[],[f11401]) ).
fof(f11474,plain,
! [X2,X3,X0,X1] :
( ~ para(X0,X1,X0,X1)
| para(X2,X3,X2,X3) ),
inference(resolution,[],[f7632,f309]) ).
fof(f12743,plain,
( ! [X2,X3,X0,X1] :
( ~ eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| cyclic(X0,X1,X2,X3) )
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f313,f393]) ).
fof(f12824,plain,
( ! [X2,X0,X1] :
( ~ para(X2,X0,X2,X0)
| cyclic(X0,X1,X2,X2) )
| ~ spl26_1 ),
inference(resolution,[],[f12743,f310]) ).
fof(f13139,plain,
( ! [X0] : cyclic(sK22,X0,sK21,sK21)
| ~ spl26_1 ),
inference(resolution,[],[f12824,f828]) ).
fof(f13159,plain,
( ! [X0] : cyclic(sK22,sK21,X0,sK21)
| ~ spl26_1 ),
inference(resolution,[],[f13139,f285]) ).
fof(f13208,plain,
( ! [X0] : cyclic(sK22,sK21,sK21,X0)
| ~ spl26_1 ),
inference(resolution,[],[f13159,f284]) ).
fof(f13330,plain,
( ! [X0,X1] :
( ~ cyclic(sK22,sK21,sK21,X0)
| cyclic(sK21,sK21,X0,X1) )
| ~ spl26_1 ),
inference(resolution,[],[f13208,f287]) ).
fof(f13335,plain,
( ! [X0,X1] : cyclic(sK21,sK21,X0,X1)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f13330,f13208]) ).
fof(f13622,plain,
( ! [X2,X0,X1] :
( ~ cyclic(sK21,sK21,X0,X1)
| cyclic(sK21,X0,X1,X2) )
| ~ spl26_1 ),
inference(resolution,[],[f13335,f287]) ).
fof(f13627,plain,
( ! [X2,X0,X1] : cyclic(sK21,X0,X1,X2)
| ~ spl26_1 ),
inference(forward_subsumption_resolution,[],[f13622,f13335]) ).
fof(f13987,plain,
( $false
| ~ spl26_1 ),
inference(resolution,[],[f13627,f390]) ).
fof(f13993,plain,
~ spl26_1,
inference(avatar_contradiction_clause,[],[f13987]) ).
fof(f14335,definition,
( spl26_128
<=> ! [X0] : coll(X0,sK20,sK25) ),
introduced(definition,[new_symbols(definition,[spl26_128])],[avatar_definition]) ).
fof(f14336,plain,
( ! [X0] : coll(X0,sK20,sK25)
| ~ spl26_128 ),
inference(avatar_component_clause,[],[f14335]) ).
fof(f14337,plain,
coll(sK20,sK20,sK25),
inference(resolution,[],[f1015,f397]) ).
fof(f14345,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl26_128 ),
inference(resolution,[],[f14336,f271]) ).
fof(f14353,plain,
( ! [X0] : coll(sK25,X0,sK20)
| ~ spl26_128 ),
inference(resolution,[],[f14345,f272]) ).
fof(f14370,plain,
( ! [X0] : coll(sK25,sK20,X0)
| ~ spl26_128 ),
inference(resolution,[],[f14353,f271]) ).
fof(f14383,plain,
( ! [X0] : coll(X0,sK22,sK25)
| ~ spl26_128 ),
inference(global_subsumption,[],[f14370,f997]) ).
fof(f14405,plain,
( spl26_35
| ~ spl26_128 ),
inference(avatar_split_clause,[],[f14383,f14335,f1087]) ).
fof(f14406,plain,
! [X0] :
( ~ coll(sK20,sK20,X0)
| coll(X0,sK25,sK20) ),
inference(resolution,[],[f14337,f273]) ).
fof(f14796,definition,
( spl26_138
<=> ! [X0] : coll(X0,sK25,sK20) ),
introduced(definition,[new_symbols(definition,[spl26_138])],[avatar_definition]) ).
fof(f14797,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl26_138 ),
inference(avatar_component_clause,[],[f14796]) ).
fof(f14809,plain,
( ! [X0] : coll(X0,sK20,sK25)
| ~ spl26_138 ),
inference(resolution,[],[f14797,f271]) ).
fof(f14817,plain,
( spl26_128
| ~ spl26_138 ),
inference(avatar_split_clause,[],[f14809,f14796,f14335]) ).
fof(f18275,plain,
( ! [X0,X1] : coll(X0,X1,X1)
| ~ spl26_97 ),
inference(resolution,[],[f11402,f337]) ).
fof(f18309,plain,
( ! [X0,X1] : coll(X0,X1,X0)
| ~ spl26_97 ),
inference(resolution,[],[f18275,f272]) ).
fof(f18529,plain,
( ! [X0,X1] : coll(X0,X0,X1)
| ~ spl26_97 ),
inference(resolution,[],[f18309,f271]) ).
fof(f18753,plain,
( ! [X0] : coll(X0,sK25,sK20)
| ~ spl26_97 ),
inference(resolution,[],[f18529,f14406]) ).
fof(f18786,plain,
( spl26_138
| ~ spl26_97 ),
inference(avatar_split_clause,[],[f18753,f11401,f14796]) ).
fof(f18863,plain,
( spl26_97
| spl26_30 ),
inference(avatar_split_clause,[],[f11474,f880,f11401]) ).
cnf(s589,plain,
~ spl26_30,
inference(sat_conversion,[],[f895]) ).
cnf(s788,plain,
( spl26_1
| ~ spl26_35 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s6187,plain,
~ spl26_1,
inference(sat_conversion,[],[f13993]) ).
cnf(s6564,plain,
( spl26_35
| ~ spl26_128 ),
inference(sat_conversion,[],[f14405]) ).
cnf(s6852,plain,
( spl26_128
| ~ spl26_138 ),
inference(sat_conversion,[],[f14817]) ).
cnf(s8253,plain,
( ~ spl26_97
| spl26_138 ),
inference(sat_conversion,[],[f18786]) ).
cnf(s8269,plain,
( spl26_30
| spl26_97 ),
inference(sat_conversion,[],[f18863]) ).
cnf(s8282,plain,
~ spl26_35,
inference(rat,[],[s788,s6187]) ).
cnf(s8284,plain,
~ spl26_128,
inference(rat,[],[s6564,s8282]) ).
cnf(s8288,plain,
~ spl26_138,
inference(rat,[],[s6852,s8284]) ).
cnf(s8292,plain,
~ spl26_97,
inference(rat,[],[s8253,s8288]) ).
cnf(s8297,plain,
spl26_30,
inference(rat,[],[s8269,s8292]) ).
cnf(s8311,plain,
$false,
inference(rat,[],[s589,s8297]) ).
fof(f18864,plain,
$false,
inference(avatar_sat_refutation,[],[s8311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO567+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n004.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 08:32:17 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.95/0.84 % (3199851)Will run a generic schedule for satisfiability detection.
% 1.95/0.84 % (3199860)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1983349428:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.95/0.84 % (3199857)% WARNING: option uhcvi not known.
% 1.95/0.84 % (3199856)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3059429588_2999 on theBenchmark for (2999ds/0Mi)
% 1.95/0.84 % (3199857)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1006755646:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.95/0.84 % (3199861)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1880280738:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.95/0.84 % (3199858)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3500253349:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.95/0.84 % (3199859)dis+10_1_sil=32000:sp=arity:random_seed=3969258100:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.95/0.84 % (3199862)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3280105661:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.95/0.84 % TRYING [1]
% 1.95/0.84 % TRYING [2]
% 1.95/0.84 % (3199860)Instruction limit reached!
% 1.95/0.84 % (3199860)------------------------------
% 1.95/0.84 % (3199860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199860)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199860)Termination reason: Instruction limit
% 1.95/0.84 % (3199860)Termination phase: Saturation
% 1.95/0.84 % (3199860)Time elapsed: 0.037 s
% 1.95/0.84 % (3199860)Peak memory usage: 13 MB
% 1.95/0.84 % (3199860)Instructions burned: 116 (million)
% 1.95/0.84 % TRYING [3]
% 1.95/0.84 % (3199870)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4131550430:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.95/0.84 % TRYING [1]
% 1.95/0.84 % TRYING [2]
% 1.95/0.84 % (3199859)Instruction limit reached!
% 1.95/0.84 % (3199859)------------------------------
% 1.95/0.84 % (3199859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199859)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199859)Termination reason: Instruction limit
% 1.95/0.84 % (3199859)Termination phase: Saturation
% 1.95/0.84 % (3199859)Time elapsed: 0.066 s
% 1.95/0.84 % (3199859)Peak memory usage: 12 MB
% 1.95/0.84 % (3199859)Instructions burned: 104 (million)
% 1.95/0.84 % (3199861)Instruction limit reached!
% 1.95/0.84 % (3199861)------------------------------
% 1.95/0.84 % (3199861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199861)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199861)Termination reason: Instruction limit
% 1.95/0.84 % (3199861)Termination phase: Saturation
% 1.95/0.84 % (3199861)Time elapsed: 0.082 s
% 1.95/0.84 % (3199861)Peak memory usage: 14 MB
% 1.95/0.84 % (3199861)Instructions burned: 132 (million)
% 1.95/0.84 % (3199872)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1943229962:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.95/0.84 % TRYING [3]
% 1.95/0.84 % (3199862)Instruction limit reached!
% 1.95/0.84 % (3199862)------------------------------
% 1.95/0.84 % (3199862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199862)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199862)Termination reason: Instruction limit
% 1.95/0.84 % (3199862)Termination phase: Saturation
% 1.95/0.84 % (3199862)Time elapsed: 0.091 s
% 1.95/0.84 % (3199862)Peak memory usage: 15 MB
% 1.95/0.84 % (3199862)Instructions burned: 161 (million)
% 1.95/0.84 % (3199873)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=4286704722:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.95/0.84 % (3199875)ott-21_1_sil=16000:fs=off:random_seed=3789334610:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.95/0.84 % (3199872)Instruction limit reached!
% 1.95/0.84 % (3199872)------------------------------
% 1.95/0.84 % (3199872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199872)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199872)Termination reason: Instruction limit
% 1.95/0.84 % (3199872)Termination phase: Saturation
% 1.95/0.84 % (3199872)Time elapsed: 0.084 s
% 1.95/0.84 % (3199872)Peak memory usage: 14 MB
% 1.95/0.84 % (3199872)Instructions burned: 132 (million)
% 1.95/0.84 % (3199878)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3106573357:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.95/0.84 % (3199870)Instruction limit reached!
% 1.95/0.84 % (3199870)------------------------------
% 1.95/0.84 % (3199870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199870)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199870)Termination reason: Instruction limit
% 1.95/0.84 % (3199870)Termination phase: Finite model building constraint generation
% 1.95/0.84 % (3199870)Time elapsed: 0.144 s
% 1.95/0.84 % (3199870)Peak memory usage: 24 MB
% 1.95/0.84 % (3199870)Instructions burned: 716 (million)
% 1.95/0.84 % (3199875)Instruction limit reached!
% 1.95/0.84 % (3199875)------------------------------
% 1.95/0.84 % (3199875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199875)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199875)Termination reason: Instruction limit
% 1.95/0.84 % (3199875)Termination phase: Saturation
% 1.95/0.84 % (3199875)Time elapsed: 0.091 s
% 1.95/0.84 % (3199875)Peak memory usage: 13 MB
% 1.95/0.84 % (3199875)Instructions burned: 181 (million)
% 1.95/0.84 % (3199880)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=889324060:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.95/0.84 % TRYING [1]
% 1.95/0.84 % TRYING [2]
% 1.95/0.84 % (3199881)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=539297056:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.95/0.84 % TRYING [3]
% 1.95/0.84 % (3199858) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3199851-3199858"...
% 1.95/0.84 % (3199880)Instruction limit reached!
% 1.95/0.84 % (3199880)------------------------------
% 1.95/0.84 % (3199880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.84 % (3199880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.84 % (3199880)CaDiCaL version: 2.1.3
% 1.95/0.84 % (3199880)Termination reason: Instruction limit
% 1.95/0.84 % (3199880)Termination phase: Finite model building constraint generation
% 1.95/0.84 % (3199880)Time elapsed: 0.162 s
% 1.95/0.84 % (3199880)Peak memory usage: 50 MB
% 1.95/0.84 % (3199880)Instructions burned: 865 (million)
% 1.95/0.84 % (3199858)...printing done.
% 1.95/0.84 % (3199858)Refutation found. Thanks to Tanya!
% 1.95/0.84 % SZS status Theorem for theBenchmark
% 1.95/0.84 % SZS output start Proof for theBenchmark
% See solution above
% 1.95/0.85 % (3199858)------------------------------
% 1.95/0.85 % (3199858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.85 % (3199858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.85 % (3199858)CaDiCaL version: 2.1.3
% 1.95/0.85 % (3199858)Termination reason: Refutation
% 1.95/0.85 % (3199858)Time elapsed: 0.375 s
% 1.95/0.85 % (3199858)Peak memory usage: 18 MB
% 1.95/0.85 % (3199858)Instructions burned: 730 (million)
% 1.95/0.85 % (3199851)Success in time 0.425 s
% 1.95/0.85 % Vampire exiting
%------------------------------------------------------------------------------