%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR108+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:45:20 AM UTC 2026
% Result : Theorem 89.07s 21.07s
% Output : Refutation 89.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 110 ( 30 unt; 4 def)
% Number of atoms : 294 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 345 ( 161 ~; 160 |; 16 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 5 prp; 0-10 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 116 ( 0 sgn 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_27) ).
fof(f7117,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7191) ).
fof(f7146,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7220) ).
fof(f7150,axiom,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7224) ).
fof(f7153,axiom,
s__subclass(s__Amphibian,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7227) ).
fof(f7157,axiom,
s__subclass(s__Bird,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7231) ).
fof(f7166,axiom,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7240) ).
fof(f7220,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_7294) ).
fof(f16771,axiom,
s__testPred44_1__10(s__Entity44_1,s__Entity44_2,s__Entity44_3,s__Entity44_4,s__Entity44_5,s__Entity44_6,s__Entity44_7,s__Entity44_8,s__Entity44_9,s__Entity44_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_23) ).
fof(f16772,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
=> ( s__instance(X0,s__Amphibian)
& s__instance(X1,s__Bird)
& s__instance(X8,s__Mammal)
& s__instance(X9,s__Reptile) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_24) ).
fof(f16773,conjecture,
( s__instance(s__Entity44_1,s__Animal)
& s__instance(s__Entity44_2,s__Animal)
& s__instance(s__Entity44_9,s__Animal)
& s__instance(s__Entity44_10,s__Animal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f16774,negated_conjecture,
~ ( s__instance(s__Entity44_1,s__Animal)
& s__instance(s__Entity44_2,s__Animal)
& s__instance(s__Entity44_9,s__Animal)
& s__instance(s__Entity44_10,s__Animal) ),
inference(negated_conjecture,[status(cth)],[f16773]) ).
fof(f17041,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f17042,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f17043,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f17042]) ).
fof(f27142,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( s__instance(X0,s__Amphibian)
& s__instance(X1,s__Bird)
& s__instance(X8,s__Mammal)
& s__instance(X9,s__Reptile) )
| ~ s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(ennf_transformation,[],[f16772]) ).
fof(f27143,plain,
( ~ s__instance(s__Entity44_1,s__Animal)
| ~ s__instance(s__Entity44_2,s__Animal)
| ~ s__instance(s__Entity44_9,s__Animal)
| ~ s__instance(s__Entity44_10,s__Animal) ),
inference(ennf_transformation,[],[f16774]) ).
fof(f28703,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17041]) ).
fof(f28704,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f17041]) ).
fof(f28705,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f17043]) ).
fof(f36632,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(cnf_transformation,[],[f7117]) ).
fof(f36661,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f7146]) ).
fof(f36665,plain,
s__subclass(s__WarmBloodedVertebrate,s__Vertebrate),
inference(cnf_transformation,[],[f7150]) ).
fof(f36668,plain,
s__subclass(s__Amphibian,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f7153]) ).
fof(f36672,plain,
s__subclass(s__Bird,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f7157]) ).
fof(f36683,plain,
s__subclass(s__Mammal,s__WarmBloodedVertebrate),
inference(cnf_transformation,[],[f7166]) ).
fof(f36737,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(cnf_transformation,[],[f7220]) ).
fof(f48622,plain,
s__testPred44_1__10(s__Entity44_1,s__Entity44_2,s__Entity44_3,s__Entity44_4,s__Entity44_5,s__Entity44_6,s__Entity44_7,s__Entity44_8,s__Entity44_9,s__Entity44_10),
inference(cnf_transformation,[],[f16771]) ).
fof(f48623,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| s__instance(X9,s__Reptile) ),
inference(cnf_transformation,[],[f27142]) ).
fof(f48624,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| s__instance(X8,s__Mammal) ),
inference(cnf_transformation,[],[f27142]) ).
fof(f48625,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| s__instance(X1,s__Bird) ),
inference(cnf_transformation,[],[f27142]) ).
fof(f48626,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ s__testPred44_1__10(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9)
| s__instance(X0,s__Amphibian) ),
inference(cnf_transformation,[],[f27142]) ).
fof(f48627,plain,
( ~ s__instance(s__Entity44_1,s__Animal)
| ~ s__instance(s__Entity44_2,s__Animal)
| ~ s__instance(s__Entity44_9,s__Animal)
| ~ s__instance(s__Entity44_10,s__Animal) ),
inference(cnf_transformation,[],[f27143]) ).
fof(f49200,definition,
( spl1514_1
<=> s__instance(s__Entity44_10,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl1514_1])],[avatar_definition]) ).
fof(f49202,plain,
( ~ s__instance(s__Entity44_10,s__Animal)
| spl1514_1 ),
inference(avatar_component_clause,[],[f49200]) ).
fof(f49204,definition,
( spl1514_2
<=> s__instance(s__Entity44_9,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl1514_2])],[avatar_definition]) ).
fof(f49206,plain,
( ~ s__instance(s__Entity44_9,s__Animal)
| spl1514_2 ),
inference(avatar_component_clause,[],[f49204]) ).
fof(f49208,definition,
( spl1514_3
<=> s__instance(s__Entity44_2,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl1514_3])],[avatar_definition]) ).
fof(f49210,plain,
( ~ s__instance(s__Entity44_2,s__Animal)
| spl1514_3 ),
inference(avatar_component_clause,[],[f49208]) ).
fof(f49212,definition,
( spl1514_4
<=> s__instance(s__Entity44_1,s__Animal) ),
introduced(definition,[new_symbols(definition,[spl1514_4])],[avatar_definition]) ).
fof(f49214,plain,
( ~ s__instance(s__Entity44_1,s__Animal)
| spl1514_4 ),
inference(avatar_component_clause,[],[f49212]) ).
fof(f49215,plain,
( ~ spl1514_1
| ~ spl1514_2
| ~ spl1514_3
| ~ spl1514_4 ),
inference(avatar_split_clause,[],[f48627,f49212,f49208,f49204,f49200]) ).
fof(f265022,plain,
s__instance(s__Entity44_10,s__Reptile),
inference(resolution,[],[f48623,f48622]) ).
fof(f265025,plain,
s__instance(s__Entity44_9,s__Mammal),
inference(resolution,[],[f48624,f48622]) ).
fof(f265028,plain,
s__instance(s__Entity44_2,s__Bird),
inference(resolution,[],[f48625,f48622]) ).
fof(f265031,plain,
s__instance(s__Entity44_1,s__Amphibian),
inference(resolution,[],[f48626,f48622]) ).
fof(f266155,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(resolution,[],[f28705,f49206]) ).
fof(f266461,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f266155,f28703]) ).
fof(f267262,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_9,X0) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f266461,f28704]) ).
fof(f268081,plain,
( ~ s__instance(s__Entity44_9,s__Vertebrate)
| spl1514_2 ),
inference(resolution,[],[f267262,f36632]) ).
fof(f268084,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(resolution,[],[f268081,f28705]) ).
fof(f268085,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f268084,f28703]) ).
fof(f268086,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_9,X0) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f268085,f28704]) ).
fof(f268092,plain,
( ~ s__instance(s__Entity44_9,s__WarmBloodedVertebrate)
| spl1514_2 ),
inference(resolution,[],[f268086,f36665]) ).
fof(f268096,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(resolution,[],[f268092,f28705]) ).
fof(f268097,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_9,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f268096,f28703]) ).
fof(f268098,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_9,X0) )
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f268097,f28704]) ).
fof(f274078,plain,
( ~ s__instance(s__Entity44_9,s__Mammal)
| spl1514_2 ),
inference(resolution,[],[f268098,f36683]) ).
fof(f274079,plain,
( $false
| spl1514_2 ),
inference(forward_subsumption_resolution,[],[f274078,f265025]) ).
fof(f274080,plain,
spl1514_2,
inference(avatar_contradiction_clause,[],[f274079]) ).
fof(f274084,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(resolution,[],[f49202,f28705]) ).
fof(f274085,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274084,f28703]) ).
fof(f274086,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_10,X0) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274085,f28704]) ).
fof(f274099,plain,
( ~ s__instance(s__Entity44_10,s__Vertebrate)
| spl1514_1 ),
inference(resolution,[],[f274086,f36632]) ).
fof(f274102,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(resolution,[],[f274099,f28705]) ).
fof(f274103,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274102,f28703]) ).
fof(f274104,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_10,X0) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274103,f28704]) ).
fof(f274227,plain,
( ~ s__instance(s__Entity44_10,s__ColdBloodedVertebrate)
| spl1514_1 ),
inference(resolution,[],[f274104,f36661]) ).
fof(f274229,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(resolution,[],[f274227,f28705]) ).
fof(f274230,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_10,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274229,f28703]) ).
fof(f274231,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_10,X0) )
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274230,f28704]) ).
fof(f274447,plain,
( ~ s__instance(s__Entity44_10,s__Reptile)
| spl1514_1 ),
inference(resolution,[],[f274231,f36737]) ).
fof(f274448,plain,
( $false
| spl1514_1 ),
inference(forward_subsumption_resolution,[],[f274447,f265022]) ).
fof(f274449,plain,
spl1514_1,
inference(avatar_contradiction_clause,[],[f274448]) ).
fof(f274455,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(resolution,[],[f49210,f28705]) ).
fof(f274456,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274455,f28703]) ).
fof(f274457,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_2,X0) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274456,f28704]) ).
fof(f274468,plain,
( ~ s__instance(s__Entity44_2,s__Vertebrate)
| spl1514_3 ),
inference(resolution,[],[f274457,f36632]) ).
fof(f274471,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(resolution,[],[f274468,f28705]) ).
fof(f274472,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274471,f28703]) ).
fof(f274473,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_2,X0) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274472,f28704]) ).
fof(f274515,plain,
( ~ s__instance(s__Entity44_2,s__WarmBloodedVertebrate)
| spl1514_3 ),
inference(resolution,[],[f274473,f36665]) ).
fof(f274529,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(s__WarmBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(resolution,[],[f274515,f28705]) ).
fof(f274530,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_2,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274529,f28703]) ).
fof(f274531,plain,
( ! [X0] :
( ~ s__subclass(X0,s__WarmBloodedVertebrate)
| ~ s__instance(s__Entity44_2,X0) )
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274530,f28704]) ).
fof(f274565,plain,
( ~ s__instance(s__Entity44_2,s__Bird)
| spl1514_3 ),
inference(resolution,[],[f274531,f36672]) ).
fof(f274567,plain,
( $false
| spl1514_3 ),
inference(forward_subsumption_resolution,[],[f274565,f265028]) ).
fof(f274568,plain,
spl1514_3,
inference(avatar_contradiction_clause,[],[f274567]) ).
fof(f274574,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(resolution,[],[f49214,f28705]) ).
fof(f274575,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274574,f28703]) ).
fof(f274576,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Animal)
| ~ s__instance(s__Entity44_1,X0) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274575,f28704]) ).
fof(f274588,plain,
( ~ s__instance(s__Entity44_1,s__Vertebrate)
| spl1514_4 ),
inference(resolution,[],[f274576,f36632]) ).
fof(f274600,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(resolution,[],[f274588,f28705]) ).
fof(f274601,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274600,f28703]) ).
fof(f274602,plain,
( ! [X0] :
( ~ s__subclass(X0,s__Vertebrate)
| ~ s__instance(s__Entity44_1,X0) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274601,f28704]) ).
fof(f274612,plain,
( ~ s__instance(s__Entity44_1,s__ColdBloodedVertebrate)
| spl1514_4 ),
inference(resolution,[],[f274602,f36661]) ).
fof(f274620,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(resolution,[],[f274612,f28705]) ).
fof(f274621,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_1,X0)
| ~ s__instance(X0,s__SetOrClass) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274620,f28703]) ).
fof(f274622,plain,
( ! [X0] :
( ~ s__subclass(X0,s__ColdBloodedVertebrate)
| ~ s__instance(s__Entity44_1,X0) )
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f274621,f28704]) ).
fof(f275120,plain,
( ~ s__instance(s__Entity44_1,s__Amphibian)
| spl1514_4 ),
inference(resolution,[],[f274622,f36668]) ).
fof(f275123,plain,
( $false
| spl1514_4 ),
inference(forward_subsumption_resolution,[],[f275120,f265031]) ).
fof(f275124,plain,
spl1514_4,
inference(avatar_contradiction_clause,[],[f275123]) ).
cnf(s1,plain,
( ~ spl1514_1
| ~ spl1514_2
| ~ spl1514_3
| ~ spl1514_4 ),
inference(sat_conversion,[],[f49215]) ).
cnf(s57324,plain,
spl1514_2,
inference(sat_conversion,[],[f274080]) ).
cnf(s57333,plain,
spl1514_1,
inference(sat_conversion,[],[f274449]) ).
cnf(s57337,plain,
spl1514_3,
inference(sat_conversion,[],[f274568]) ).
cnf(s57338,plain,
spl1514_4,
inference(sat_conversion,[],[f275124]) ).
cnf(s57504,plain,
$false,
inference(rat,[],[s1,s57338,s57337,s57324,s57333]) ).
fof(f275125,plain,
$false,
inference(avatar_sat_refutation,[],[s57504]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR108+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.18 % Computer : n005.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Mon Sep 28 22:59:47 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 Running first-order model finding
% 0.10/0.21 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
% 20.14/3.46 % (1267194)Will run a generic schedule for satisfiability detection.
% 20.14/3.46 % (1267203)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1797796899:i=116_2995 on theBenchmark for (2995ds/116Mi)
% 20.14/3.46 % (1267200)% WARNING: option uhcvi not known.
% 20.14/3.46 % (1267199)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=838483640_2995 on theBenchmark for (2995ds/0Mi)
% 20.14/3.46 % (1267200)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3733222589:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi)
% 20.14/3.46 % (1267201)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3955822618:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi)
% 20.14/3.46 % (1267202)dis+10_1_sil=32000:sp=arity:random_seed=4034907407:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi)
% 20.14/3.46 % (1267204)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=449609943:i=131_2995 on theBenchmark for (2995ds/131Mi)
% 20.14/3.46 % (1267205)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3673514183:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi)
% 20.14/3.46 % (1267203)Instruction limit reached!
% 20.14/3.46 % (1267203)------------------------------
% 20.14/3.46 % (1267203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.14/3.46 % (1267203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.46 % (1267203)CaDiCaL version: 2.1.3
% 20.14/3.46 % (1267203)Termination reason: Instruction limit
% 20.14/3.46 % (1267203)Termination phase: NewCNF
% 20.14/3.46 % (1267203)Time elapsed: 0.056 s
% 20.14/3.46 % (1267203)Peak memory usage: 38 MB
% 20.14/3.46 % (1267203)Instructions burned: 116 (million)
% 20.14/3.46 % (1267213)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=178321117:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 20.14/3.46 % (1267202)Instruction limit reached!
% 20.14/3.46 % (1267202)------------------------------
% 20.14/3.46 % (1267202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.14/3.46 % (1267202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.46 % (1267202)CaDiCaL version: 2.1.3
% 20.14/3.46 % (1267202)Termination reason: Instruction limit
% 20.14/3.46 % (1267202)Termination phase: Preprocessing 3
% 20.14/3.46 % (1267202)Time elapsed: 0.079 s
% 20.14/3.46 % (1267202)Peak memory usage: 36 MB
% 20.14/3.46 % (1267202)Instructions burned: 104 (million)
% 20.14/3.46 % (1267204)Instruction limit reached!
% 20.14/3.46 % (1267204)------------------------------
% 20.14/3.46 % (1267204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.14/3.46 % (1267204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.46 % (1267204)CaDiCaL version: 2.1.3
% 20.14/3.46 % (1267204)Termination reason: Instruction limit
% 20.14/3.46 % (1267204)Termination phase: Preprocessing 3
% 20.14/3.46 % (1267204)Time elapsed: 0.091 s
% 20.14/3.46 % (1267204)Peak memory usage: 36 MB
% 20.14/3.46 % (1267204)Instructions burned: 132 (million)
% 20.14/3.46 % (1267215)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2485242555:i=131:bd=preordered:fsd=on_2994 on theBenchmark for (2994ds/131Mi)
% 20.14/3.46 % (1267205)Instruction limit reached!
% 20.14/3.46 % (1267205)------------------------------
% 20.14/3.46 % (1267205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.14/3.46 % (1267205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.14/3.46 % (1267205)CaDiCaL version: 2.1.3
% 20.14/3.46 % (1267205)Termination reason: Instruction limit
% 20.14/3.46 % (1267205)Termination phase: Preprocessing 3
% 20.14/3.46 % (1267205)Time elapsed: 0.105 s
% 20.14/3.46 % (1267205)Peak memory usage: 38 MB
% 20.14/3.46 % (1267205)Instructions burned: 161 (million)
% 20.14/3.46 % (1267216)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=3108997565:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2994 on theBenchmark for (2994ds/684Mi)
% 20.14/3.46 % (1267218)ott-21_1_sil=16000:fs=off:random_seed=4028092199:i=180:av=off:fsr=off_2994 on theBenchmark for (2994ds/180Mi)
% 20.14/3.46 % (1267215)Instruction limit reached!
% 20.14/3.46 % (1267215)------------------------------
% 20.14/3.46 % (1267215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.14/3.46 % (1267215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267215)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267215)Termination reason: Instruction limit
% 26.22/4.31 % (1267215)Termination phase: Preprocessing 3
% 26.22/4.31 % (1267215)Time elapsed: 0.087 s
% 26.22/4.31 % (1267215)Peak memory usage: 36 MB
% 26.22/4.31 % (1267215)Instructions burned: 132 (million)
% 26.22/4.31 % (1267221)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=761161446:i=477:bd=all_2993 on theBenchmark for (2993ds/477Mi)
% 26.22/4.31 % (1267218)Instruction limit reached!
% 26.22/4.31 % (1267218)------------------------------
% 26.22/4.31 % (1267218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267218)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267218)Termination reason: Instruction limit
% 26.22/4.31 % (1267218)Termination phase: Preprocessing 3
% 26.22/4.31 % (1267218)Time elapsed: 0.120 s
% 26.22/4.31 % (1267218)Peak memory usage: 38 MB
% 26.22/4.31 % (1267218)Instructions burned: 181 (million)
% 26.22/4.31 % (1267223)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1175120378:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 26.22/4.31 % (1267213)Instruction limit reached!
% 26.22/4.31 % (1267213)------------------------------
% 26.22/4.31 % (1267213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267213)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267213)Termination reason: Instruction limit
% 26.22/4.31 % (1267213)Termination phase: Property scanning
% 26.22/4.31 % (1267213)Time elapsed: 0.228 s
% 26.22/4.31 % (1267213)Peak memory usage: 73 MB
% 26.22/4.31 % (1267213)Instructions burned: 714 (million)
% 26.22/4.31 % (1267225)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=702962266:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 26.22/4.31 % (1267216)Instruction limit reached!
% 26.22/4.31 % (1267216)------------------------------
% 26.22/4.31 % (1267216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267216)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267216)Termination reason: Instruction limit
% 26.22/4.31 % (1267216)Termination phase: Saturation
% 26.22/4.31 % (1267216)Time elapsed: 0.356 s
% 26.22/4.31 % (1267216)Peak memory usage: 46 MB
% 26.22/4.31 % (1267216)Instructions burned: 686 (million)
% 26.22/4.31 % (1267221)Instruction limit reached!
% 26.22/4.31 % (1267221)------------------------------
% 26.22/4.31 % (1267221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267221)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267221)Termination reason: Instruction limit
% 26.22/4.31 % (1267221)Termination phase: Saturation
% 26.22/4.31 % (1267221)Time elapsed: 0.259 s
% 26.22/4.31 % (1267221)Peak memory usage: 43 MB
% 26.22/4.31 % (1267221)Instructions burned: 478 (million)
% 26.22/4.31 % (1267227)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=347330738:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 26.22/4.31 % (1267228)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=3390682234:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 26.22/4.31 % (1267225)Instruction limit reached!
% 26.22/4.31 % (1267225)------------------------------
% 26.22/4.31 % (1267225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.22/4.31 % (1267225)CaDiCaL version: 2.1.3
% 26.22/4.31 % (1267225)Termination reason: Instruction limit
% 26.22/4.31 % (1267225)Termination phase: Saturation
% 26.22/4.31 % (1267225)Time elapsed: 0.352 s
% 26.22/4.31 % (1267225)Peak memory usage: 54 MB
% 26.22/4.31 % (1267225)Instructions burned: 1183 (million)
% 26.22/4.31 % (1267231)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2586815586:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 26.22/4.31 % (1267223)Instruction limit reached!
% 26.22/4.31 % (1267223)------------------------------
% 26.22/4.31 % (1267223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.22/4.31 % (1267223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267223)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267223)Termination reason: Instruction limit
% 42.41/6.77 % (1267223)Termination phase: Property scanning
% 42.41/6.77 % (1267223)Time elapsed: 0.453 s
% 42.41/6.77 % (1267223)Peak memory usage: 71 MB
% 42.41/6.77 % (1267223)Instructions burned: 865 (million)
% 42.41/6.77 % (1267233)fmb+10_1_sil=64000:random_seed=2279354648:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 42.41/6.77 % (1267228)Instruction limit reached!
% 42.41/6.77 % (1267228)------------------------------
% 42.41/6.77 % (1267228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267228)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267228)Termination reason: Instruction limit
% 42.41/6.77 % (1267228)Termination phase: Saturation
% 42.41/6.77 % (1267228)Time elapsed: 0.364 s
% 42.41/6.77 % (1267228)Peak memory usage: 48 MB
% 42.41/6.77 % (1267228)Instructions burned: 693 (million)
% 42.41/6.77 % (1267235)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3177053102:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 42.41/6.77 % (1267231)Instruction limit reached!
% 42.41/6.77 % (1267231)------------------------------
% 42.41/6.77 % (1267231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267231)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267231)Termination reason: Instruction limit
% 42.41/6.77 % (1267231)Termination phase: Saturation
% 42.41/6.77 % (1267231)Time elapsed: 0.265 s
% 42.41/6.77 % (1267231)Peak memory usage: 58 MB
% 42.41/6.77 % (1267231)Instructions burned: 881 (million)
% 42.41/6.77 % (1267237)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2045127086:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 42.41/6.77 % (1267227)Instruction limit reached!
% 42.41/6.77 % (1267227)------------------------------
% 42.41/6.77 % (1267227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267227)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267227)Termination reason: Instruction limit
% 42.41/6.77 % (1267227)Termination phase: Property scanning
% 42.41/6.77 % (1267227)Time elapsed: 0.471 s
% 42.41/6.77 % (1267227)Peak memory usage: 71 MB
% 42.41/6.77 % (1267227)Instructions burned: 891 (million)
% 42.41/6.77 % (1267239)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2866897727:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 42.41/6.77 % (1267237)Instruction limit reached!
% 42.41/6.77 % (1267237)------------------------------
% 42.41/6.77 % (1267237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267237)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267237)Termination reason: Instruction limit
% 42.41/6.77 % (1267237)Termination phase: Property scanning
% 42.41/6.77 % (1267237)Time elapsed: 0.267 s
% 42.41/6.77 % (1267237)Peak memory usage: 71 MB
% 42.41/6.77 % (1267237)Instructions burned: 923 (million)
% 42.41/6.77 % (1267241)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4024913168:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 42.41/6.77 % (1267241)Instruction limit reached!
% 42.41/6.77 % (1267241)------------------------------
% 42.41/6.77 % (1267241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.41/6.77 % (1267241)CaDiCaL version: 2.1.3
% 42.41/6.77 % (1267241)Termination reason: Instruction limit
% 42.41/6.77 % (1267241)Termination phase: Saturation
% 42.41/6.77 % (1267241)Time elapsed: 0.459 s
% 42.41/6.77 % (1267241)Peak memory usage: 60 MB
% 42.41/6.77 % (1267241)Instructions burned: 1473 (million)
% 42.41/6.77 % (1267243)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2884459603:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 42.41/6.77 % Detected minimum model sizes of [447]
% 42.41/6.77 % Detected maximum model sizes of [max]
% 42.41/6.77 % (1267199)Cannot represent all propositional literals internally
% 42.41/6.77 % (1267199)Refutation not found, incomplete strategy
% 42.41/6.77 % (1267199)------------------------------
% 42.41/6.77 % (1267199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.41/6.77 % (1267199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267199)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267199)Termination reason: Refutation not found, incomplete strategy
% 62.73/9.40 % (1267199)Time elapsed: 2.807 s
% 62.73/9.40 % (1267199)Peak memory usage: 148 MB
% 62.73/9.40 % (1267199)Instructions burned: 5798 (million)
% 62.73/9.40 % (1267199)------------------------------
% 62.73/9.40 % (1267199)------------------------------
% 62.73/9.40 % (1267245)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=142794168:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 62.73/9.40 % Detected minimum model sizes of [447]
% 62.73/9.40 % Detected maximum model sizes of [max]
% 62.73/9.40 % (1267233)Cannot represent all propositional literals internally
% 62.73/9.40 % (1267233)Refutation not found, incomplete strategy
% 62.73/9.40 % (1267233)------------------------------
% 62.73/9.40 % (1267233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.73/9.40 % (1267233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267233)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267233)Termination reason: Refutation not found, incomplete strategy
% 62.73/9.40 % (1267233)Time elapsed: 2.327 s
% 62.73/9.40 % (1267233)Peak memory usage: 132 MB
% 62.73/9.40 % (1267233)Instructions burned: 5026 (million)
% 62.73/9.40 % (1267233)------------------------------
% 62.73/9.40 % (1267233)------------------------------
% 62.73/9.40 % (1267247)ott-2_1_sil=16000:newcnf=on:random_seed=1921367554:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi)
% 62.73/9.40 % Detected minimum model sizes of [447]
% 62.73/9.40 % Detected maximum model sizes of [max]
% 62.73/9.40 % (1267243)Cannot represent all propositional literals internally
% 62.73/9.40 % (1267243)Refutation not found, incomplete strategy
% 62.73/9.40 % (1267243)------------------------------
% 62.73/9.40 % (1267243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.73/9.40 % (1267243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267243)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267243)Termination reason: Refutation not found, incomplete strategy
% 62.73/9.40 % (1267243)Time elapsed: 1.509 s
% 62.73/9.40 % (1267243)Peak memory usage: 147 MB
% 62.73/9.40 % (1267243)Instructions burned: 5786 (million)
% 62.73/9.40 % (1267243)------------------------------
% 62.73/9.40 % (1267243)------------------------------
% 62.73/9.40 % (1267249)ott+10_1_sil=32000:tgt=ground:random_seed=3845678526:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 62.73/9.40 % Detected minimum model sizes of [447]
% 62.73/9.40 % Detected maximum model sizes of [max]
% 62.73/9.40 % (1267235)Cannot represent all propositional literals internally
% 62.73/9.40 % (1267235)Refutation not found, incomplete strategy
% 62.73/9.40 % (1267235)------------------------------
% 62.73/9.40 % (1267235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.73/9.40 % (1267235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267235)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267235)Termination reason: Refutation not found, incomplete strategy
% 62.73/9.40 % (1267235)Time elapsed: 2.426 s
% 62.73/9.40 % (1267235)Peak memory usage: 137 MB
% 62.73/9.40 % (1267235)Instructions burned: 5228 (million)
% 62.73/9.40 % (1267235)------------------------------
% 62.73/9.40 % (1267235)------------------------------
% 62.73/9.40 % (1267251)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3010704180:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 62.73/9.40 % (1267247)Instruction limit reached!
% 62.73/9.40 % (1267247)------------------------------
% 62.73/9.40 % (1267247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.73/9.40 % (1267247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267247)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267247)Termination reason: Instruction limit
% 62.73/9.40 % (1267247)Termination phase: Saturation
% 62.73/9.40 % (1267247)Time elapsed: 0.454 s
% 62.73/9.40 % (1267247)Peak memory usage: 51 MB
% 62.73/9.40 % (1267247)Instructions burned: 870 (million)
% 62.73/9.40 % (1267253)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=571017517:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 62.73/9.40 % (1267239)Instruction limit reached!
% 62.73/9.40 % (1267239)------------------------------
% 62.73/9.40 % (1267239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.73/9.40 % (1267239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.73/9.40 % (1267239)CaDiCaL version: 2.1.3
% 62.73/9.40 % (1267239)Termination reason: Instruction limit
% 143.64/20.84 % (1267239)Termination phase: Saturation
% 143.64/20.84 % (1267239)Time elapsed: 2.664 s
% 143.64/20.84 % (1267239)Peak memory usage: 93 MB
% 143.64/20.84 % (1267239)Instructions burned: 5133 (million)
% 143.64/20.84 % (1267255)dis+21_1_sil=32000:sas=cadical:random_seed=3702902499:i=3773:amm=off_2958 on theBenchmark for (2958ds/3773Mi)
% 143.64/20.84 % (1267245)Instruction limit reached!
% 143.64/20.84 % (1267245)------------------------------
% 143.64/20.84 % (1267245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.64/20.84 % (1267245)CaDiCaL version: 2.1.3
% 143.64/20.84 % (1267245)Termination reason: Instruction limit
% 143.64/20.84 % (1267245)Termination phase: Finite model building preprocessing
% 143.64/20.84 % (1267245)Time elapsed: 1.077 s
% 143.64/20.84 % (1267245)Peak memory usage: 110 MB
% 143.64/20.84 % (1267245)Instructions burned: 2175 (million)
% 143.64/20.84 % (1267257)ott+11_1_sil=16000:gs=on:random_seed=3776640558:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2955 on theBenchmark for (2955ds/2251Mi)
% 143.64/20.84 % (1267249)Instruction limit reached!
% 143.64/20.84 % (1267249)------------------------------
% 143.64/20.84 % (1267249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.64/20.84 % (1267249)CaDiCaL version: 2.1.3
% 143.64/20.84 % (1267249)Termination reason: Instruction limit
% 143.64/20.84 % (1267249)Termination phase: Saturation
% 143.64/20.84 % (1267249)Time elapsed: 1.454 s
% 143.64/20.84 % (1267249)Peak memory usage: 76 MB
% 143.64/20.84 % (1267249)Instructions burned: 5116 (million)
% 143.64/20.84 % (1267259)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=428484542:fmbsr=1.6:i=67534_2948 on theBenchmark for (2948ds/67534Mi)
% 143.64/20.84 % (1267255)Instruction limit reached!
% 143.64/20.84 % (1267255)------------------------------
% 143.64/20.84 % (1267255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.64/20.84 % (1267255)CaDiCaL version: 2.1.3
% 143.64/20.84 % (1267255)Termination reason: Instruction limit
% 143.64/20.84 % (1267255)Termination phase: Saturation
% 143.64/20.84 % (1267255)Time elapsed: 1.461 s
% 143.64/20.84 % (1267255)Peak memory usage: 68 MB
% 143.64/20.84 % (1267255)Instructions burned: 3773 (million)
% 143.64/20.84 % (1267261)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2589714558:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2944 on theBenchmark for (2944ds/4591Mi)
% 143.64/20.84 % (1267257)Instruction limit reached!
% 143.64/20.84 % (1267257)------------------------------
% 143.64/20.84 % (1267257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.64/20.84 % (1267257)CaDiCaL version: 2.1.3
% 143.64/20.84 % (1267257)Termination reason: Instruction limit
% 143.64/20.84 % (1267257)Termination phase: Saturation
% 143.64/20.84 % (1267257)Time elapsed: 1.446 s
% 143.64/20.84 % (1267257)Peak memory usage: 92 MB
% 143.64/20.84 % (1267257)Instructions burned: 2251 (million)
% 143.64/20.84 % (1267263)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2784373847:i=29340_2941 on theBenchmark for (2941ds/29340Mi)
% 143.64/20.84 % (1267253)Instruction limit reached!
% 143.64/20.84 % (1267253)------------------------------
% 143.64/20.84 % (1267253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.64/20.84 % (1267253)CaDiCaL version: 2.1.3
% 143.64/20.84 % (1267253)Termination reason: Instruction limit
% 143.64/20.84 % (1267253)Termination phase: Saturation
% 143.64/20.84 % (1267253)Time elapsed: 1.859 s
% 143.64/20.84 % (1267253)Peak memory usage: 108 MB
% 143.64/20.84 % (1267253)Instructions burned: 3512 (million)
% 143.64/20.84 % (1267265)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2785535935:i=5211_2940 on theBenchmark for (2940ds/5211Mi)
% 143.64/20.84 % Detected minimum model sizes of [447]
% 143.64/20.84 % Detected maximum model sizes of [max]
% 143.64/20.84 % (1267251)Cannot represent all propositional literals internally
% 143.64/20.84 % (1267251)Refutation not found, incomplete strategy
% 143.64/20.84 % (1267251)------------------------------
% 143.64/20.84 % (1267251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.64/20.84 % (1267251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267251)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267251)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267251)Time elapsed: 2.743 s
% 89.07/21.07 % (1267251)Peak memory usage: 148 MB
% 89.07/21.07 % (1267251)Instructions burned: 5814 (million)
% 89.07/21.07 % (1267251)------------------------------
% 89.07/21.07 % (1267251)------------------------------
% 89.07/21.07 % Detected minimum model sizes of [447]
% 89.07/21.07 % Detected maximum model sizes of [max]
% 89.07/21.07 % (1267259)Cannot represent all propositional literals internally
% 89.07/21.07 % (1267259)Refutation not found, incomplete strategy
% 89.07/21.07 % (1267259)------------------------------
% 89.07/21.07 % (1267259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267259)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267259)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267259)Time elapsed: 1.443 s
% 89.07/21.07 % (1267259)Peak memory usage: 141 MB
% 89.07/21.07 % (1267259)Instructions burned: 5820 (million)
% 89.07/21.07 % (1267267)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4113282931:i=5497:nm=2_2933 on theBenchmark for (2933ds/5497Mi)
% 89.07/21.07 % (1267259)------------------------------
% 89.07/21.07 % (1267259)------------------------------
% 89.07/21.07 % (1267269)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3325759470:fmbsr=2:i=46332_2933 on theBenchmark for (2933ds/46332Mi)
% 89.07/21.07 % (1267261)Instruction limit reached!
% 89.07/21.07 % (1267261)------------------------------
% 89.07/21.07 % (1267261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267261)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267261)Termination reason: Instruction limit
% 89.07/21.07 % (1267261)Termination phase: Saturation
% 89.07/21.07 % (1267261)Time elapsed: 2.335 s
% 89.07/21.07 % (1267261)Peak memory usage: 70 MB
% 89.07/21.07 % (1267261)Instructions burned: 4593 (million)
% 89.07/21.07 % (1267271)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1988487661:i=14071_2920 on theBenchmark for (2920ds/14071Mi)
% 89.07/21.07 % Detected minimum model sizes of [447]
% 89.07/21.07 % Detected maximum model sizes of [max]
% 89.07/21.07 % (1267269)Cannot represent all propositional literals internally
% 89.07/21.07 % (1267269)Refutation not found, incomplete strategy
% 89.07/21.07 % (1267269)------------------------------
% 89.07/21.07 % (1267269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267269)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267269)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267269)Time elapsed: 1.437 s
% 89.07/21.07 % (1267269)Peak memory usage: 141 MB
% 89.07/21.07 % (1267269)Instructions burned: 5820 (million)
% 89.07/21.07 % (1267269)------------------------------
% 89.07/21.07 % (1267269)------------------------------
% 89.07/21.07 % (1267273)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=223215567:i=22565:add=on:rawr=on_2918 on theBenchmark for (2918ds/22565Mi)
% 89.07/21.07 % (1267265)Instruction limit reached!
% 89.07/21.07 % (1267265)------------------------------
% 89.07/21.07 % (1267265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267265)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267265)Termination reason: Instruction limit
% 89.07/21.07 % (1267265)Termination phase: Saturation
% 89.07/21.07 % (1267265)Time elapsed: 2.436 s
% 89.07/21.07 % (1267265)Peak memory usage: 70 MB
% 89.07/21.07 % (1267265)Instructions burned: 5211 (million)
% 89.07/21.07 % (1267275)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1429617114:i=8173:av=off_2915 on theBenchmark for (2915ds/8173Mi)
% 89.07/21.07 % Detected minimum model sizes of [447]
% 89.07/21.07 % Detected maximum model sizes of [max]
% 89.07/21.07 % (1267267)Cannot represent all propositional literals internally
% 89.07/21.07 % (1267267)Refutation not found, incomplete strategy
% 89.07/21.07 % (1267267)------------------------------
% 89.07/21.07 % (1267267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267267)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267267)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267267)Time elapsed: 2.558 s
% 89.07/21.07 % (1267267)Peak memory usage: 141 MB
% 89.07/21.07 % (1267267)Instructions burned: 5382 (million)
% 89.07/21.07 % (1267267)------------------------------
% 89.07/21.07 % (1267267)------------------------------
% 89.07/21.07 % (1267277)dis+10_16:1_sil=16000:random_seed=815885660:i=9155:fsr=off_2907 on theBenchmark for (2907ds/9155Mi)
% 89.07/21.07 % Detected minimum model sizes of [447]
% 89.07/21.07 % Detected maximum model sizes of [max]
% 89.07/21.07 % (1267271)Cannot represent all propositional literals internally
% 89.07/21.07 % (1267271)Refutation not found, incomplete strategy
% 89.07/21.07 % (1267271)------------------------------
% 89.07/21.07 % (1267271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267271)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267271)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267271)Time elapsed: 2.484 s
% 89.07/21.07 % (1267271)Peak memory usage: 139 MB
% 89.07/21.07 % (1267271)Instructions burned: 5353 (million)
% 89.07/21.07 % (1267271)------------------------------
% 89.07/21.07 % (1267271)------------------------------
% 89.07/21.07 % (1267279)ott-3_8_sil=64000:random_seed=1895626409:i=20139:bs=on_2894 on theBenchmark for (2894ds/20139Mi)
% 89.07/21.07 % (1267275)Instruction limit reached!
% 89.07/21.07 % (1267275)------------------------------
% 89.07/21.07 % (1267275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267275)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267275)Termination reason: Instruction limit
% 89.07/21.07 % (1267275)Termination phase: Saturation
% 89.07/21.07 % (1267275)Time elapsed: 5.062 s
% 89.07/21.07 % (1267275)Peak memory usage: 93 MB
% 89.07/21.07 % (1267275)Instructions burned: 8173 (million)
% 89.07/21.07 % (1267281)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=721286889:fmbsr=2:i=32576_2865 on theBenchmark for (2865ds/32576Mi)
% 89.07/21.07 % (1267277)Instruction limit reached!
% 89.07/21.07 % (1267277)------------------------------
% 89.07/21.07 % (1267277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267277)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267277)Termination reason: Instruction limit
% 89.07/21.07 % (1267277)Termination phase: Saturation
% 89.07/21.07 % (1267277)Time elapsed: 4.613 s
% 89.07/21.07 % (1267277)Peak memory usage: 130 MB
% 89.07/21.07 % (1267277)Instructions burned: 9155 (million)
% 89.07/21.07 % (1267283)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=521533244:i=11404_2861 on theBenchmark for (2861ds/11404Mi)
% 89.07/21.07 % Detected minimum model sizes of [447]
% 89.07/21.07 % Detected maximum model sizes of [max]
% 89.07/21.07 % (1267281)Cannot represent all propositional literals internally
% 89.07/21.07 % (1267281)Refutation not found, incomplete strategy
% 89.07/21.07 % (1267281)------------------------------
% 89.07/21.07 % (1267281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267281)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267281)Termination reason: Refutation not found, incomplete strategy
% 89.07/21.07 % (1267281)Time elapsed: 2.780 s
% 89.07/21.07 % (1267281)Peak memory usage: 147 MB
% 89.07/21.07 % (1267281)Instructions burned: 5787 (million)
% 89.07/21.07 % (1267281)------------------------------
% 89.07/21.07 % (1267281)------------------------------
% 89.07/21.07 % (1267285)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=472973494:i=14134_2836 on theBenchmark for (2836ds/14134Mi)
% 89.07/21.07 % (1267273)Instruction limit reached!
% 89.07/21.07 % (1267273)------------------------------
% 89.07/21.07 % (1267273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.07 % (1267273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.07 % (1267273)CaDiCaL version: 2.1.3
% 89.07/21.07 % (1267273)Termination reason: Instruction limit
% 89.07/21.07 % (1267273)Termination phase: Saturation
% 89.07/21.07 % (1267273)Time elapsed: 8.466 s
% 89.07/21.07 % (1267273)Peak memory usage: 914 MB
% 89.07/21.07 % (1267273)Instructions burned: 22566 (million)
% 89.07/21.07 % (1267287)dis+33_16_sil=32000:sac=on:random_seed=1310191824:i=15851:nm=0_2833 on theBenchmark for (2833ds/15851Mi)
% 89.07/21.07 % (1267285) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1267194-1267285"...
% 89.07/21.07 % (1267285)...printing done.
% 89.07/21.07 % (1267285)Refutation found. Thanks to Tanya!
% 89.07/21.07 % SZS status Theorem for theBenchmark
% 89.07/21.07 % SZS output start Proof for theBenchmark
% See solution above
% 89.07/21.08 % (1267285)------------------------------
% 89.07/21.08 % (1267285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.07/21.08 % (1267285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.07/21.08 % (1267285)CaDiCaL version: 2.1.3
% 89.07/21.08 % (1267285)Termination reason: Refutation
% 89.07/21.08 % (1267285)Time elapsed: 4.262 s
% 89.07/21.08 % (1267285)Peak memory usage: 125 MB
% 89.07/21.08 % (1267285)Instructions burned: 7553 (million)
% 89.07/21.08 % (1267194)Success in time 20.852 s
% 89.07/21.08 % Vampire exiting
%------------------------------------------------------------------------------