%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET105+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 12:40:09 PM UTC 2026
% Result : Theorem 13.76s 2.95s
% Output : Refutation 15.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 26
% Syntax : Number of formulae : 180 ( 34 unt; 18 def)
% Number of atoms : 474 ( 166 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 452 ( 158 ~; 248 |; 28 &)
% ( 16 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 13 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 135 ( 0 sgn 129 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subclass(X0,X1)
<=> ! [X2] :
( member(X2,X0)
=> member(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_defn) ).
fof(f3,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subclass(X0,X1)
& subclass(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality) ).
fof(f4,axiom,
! [X0,X1,X2] :
( member(X0,unordered_pair(X1,X2))
<=> ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_defn) ).
fof(f5,axiom,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair) ).
fof(f6,axiom,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set_defn) ).
fof(f7,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_defn) ).
fof(f41,axiom,
! [X0] :
( X0 != null_class
=> ? [X1] :
( member(X1,universal_class)
& member(X1,X0)
& disjoint(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity) ).
fof(f44,conjecture,
! [X0,X1] :
( unordered_pair(null_class,singleton(null_class)) = ordered_pair(X0,X1)
| member(X0,universal_class)
| member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_3_of_ordered_pair) ).
fof(f45,negated_conjecture,
~ ! [X0,X1] :
( unordered_pair(null_class,singleton(null_class)) = ordered_pair(X0,X1)
| member(X0,universal_class)
| member(X1,universal_class) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f47,plain,
! [X0,X1] :
( subclass(X0,X1)
<=> ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0] :
( ? [X1] :
( member(X1,universal_class)
& member(X1,X0)
& disjoint(X1,X0) )
| null_class = X0 ),
inference(ennf_transformation,[],[f41]) ).
fof(f60,plain,
? [X0,X1] :
( ordered_pair(X0,X1) != unordered_pair(null_class,singleton(null_class))
& ~ member(X0,universal_class)
& ~ member(X1,universal_class) ),
inference(ennf_transformation,[],[f45]) ).
fof(f61,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) )
| ~ subclass(X0,X1) ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f62,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subclass(X0,X1) ) ),
inference(rectify,[],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ( ~ member(sK0(X0,X1),X1)
& member(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subclass(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subclass(X0,X1)
| ~ subclass(X1,X0) )
& ( ( subclass(X0,X1)
& subclass(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f65,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subclass(X0,X1)
| ~ subclass(X1,X0) )
& ( ( subclass(X0,X1)
& subclass(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| ( X0 != X1
& X0 != X2 ) )
& ( ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) )
| ~ member(X0,unordered_pair(X1,X2)) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| ( X0 != X1
& X0 != X2 ) )
& ( ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) )
| ~ member(X0,unordered_pair(X1,X2)) ) ),
inference(flattening,[],[f66]) ).
fof(f101,plain,
! [X0] :
( ( member(sK4(X0),universal_class)
& member(sK4(X0),X0)
& disjoint(sK4(X0),X0) )
| null_class = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f57]) ).
fof(f103,plain,
( unordered_pair(null_class,singleton(null_class)) != ordered_pair(sK6,sK7)
& ~ member(sK6,universal_class)
& ~ member(sK7,universal_class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X1,sK7)],[f60]) ).
fof(f105,plain,
! [X0,X1] :
( member(sK0(X0,X1),X0)
| subclass(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f106,plain,
! [X0,X1] :
( ~ member(sK0(X0,X1),X1)
| subclass(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f110,plain,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f65]) ).
fof(f111,plain,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f67]) ).
fof(f112,plain,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| member(X0,universal_class) ),
inference(cnf_transformation,[],[f67]) ).
fof(f113,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| X0 != X2 ),
inference(cnf_transformation,[],[f67]) ).
fof(f115,plain,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f6]) ).
fof(f117,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))),
inference(cnf_transformation,[],[f7]) ).
fof(f186,plain,
! [X0] :
( member(sK4(X0),X0)
| null_class = X0 ),
inference(cnf_transformation,[],[f101]) ).
fof(f187,plain,
! [X0] :
( member(sK4(X0),universal_class)
| null_class = X0 ),
inference(cnf_transformation,[],[f101]) ).
fof(f191,plain,
~ member(sK7,universal_class),
inference(cnf_transformation,[],[f103]) ).
fof(f192,plain,
~ member(sK6,universal_class),
inference(cnf_transformation,[],[f103]) ).
fof(f193,plain,
unordered_pair(null_class,singleton(null_class)) != ordered_pair(sK6,sK7),
inference(cnf_transformation,[],[f103]) ).
fof(f194,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f117,f116,f116]) ).
fof(f231,plain,
unordered_pair(null_class,unordered_pair(null_class,null_class)) != unordered_pair(unordered_pair(sK6,sK6),unordered_pair(sK6,unordered_pair(sK7,sK7))),
inference(definition_unfolding,[],[f193,f116,f194]) ).
fof(f235,plain,
! [X2,X1] :
( member(X2,unordered_pair(X1,X2))
| ~ member(X2,universal_class) ),
inference(equality_resolution,[],[f113]) ).
fof(f238,definition,
sF8 = unordered_pair(null_class,null_class),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f239,plain,
unordered_pair(null_class,null_class) = sF8,
inference(reorient_equations,[],[f238]) ).
fof(f240,definition,
sF9 = unordered_pair(null_class,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f241,plain,
unordered_pair(null_class,sF8) = sF9,
inference(reorient_equations,[],[f240]) ).
fof(f242,definition,
sF10 = unordered_pair(sK6,sK6),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f243,plain,
unordered_pair(sK6,sK6) = sF10,
inference(reorient_equations,[],[f242]) ).
fof(f244,definition,
sF11 = unordered_pair(sK7,sK7),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f245,plain,
unordered_pair(sK7,sK7) = sF11,
inference(reorient_equations,[],[f244]) ).
fof(f246,definition,
sF12 = unordered_pair(sK6,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f247,plain,
unordered_pair(sK6,sF11) = sF12,
inference(reorient_equations,[],[f246]) ).
fof(f248,definition,
sF13 = unordered_pair(sF10,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f249,plain,
unordered_pair(sF10,sF12) = sF13,
inference(reorient_equations,[],[f248]) ).
fof(f250,plain,
sF9 != sF13,
inference(definition_folding,[],[f231,f249,f247,f245,f243,f241,f239]) ).
fof(f251,plain,
member(sF11,universal_class),
inference(superposition,[],[f115,f245]) ).
fof(f260,plain,
! [X0] :
( ~ member(X0,sF12)
| member(X0,universal_class) ),
inference(superposition,[],[f112,f247]) ).
fof(f264,plain,
! [X0] :
( ~ member(X0,sF8)
| null_class = X0
| null_class = X0 ),
inference(superposition,[],[f111,f239]) ).
fof(f265,plain,
! [X0] :
( ~ member(X0,sF10)
| sK6 = X0
| sK6 = X0 ),
inference(superposition,[],[f111,f243]) ).
fof(f267,plain,
! [X0] :
( ~ member(X0,sF11)
| sK7 = X0
| sK7 = X0 ),
inference(superposition,[],[f111,f245]) ).
fof(f269,plain,
! [X0] :
( ~ member(X0,sF11)
| sK7 = X0 ),
inference(duplicate_literal_removal,[],[f267]) ).
fof(f270,plain,
! [X0] :
( ~ member(X0,sF10)
| sK6 = X0 ),
inference(duplicate_literal_removal,[],[f265]) ).
fof(f271,plain,
! [X0] :
( ~ member(X0,sF8)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f264]) ).
fof(f278,plain,
( null_class = sF10
| sK6 = sK4(sF10) ),
inference(resolution,[],[f186,f270]) ).
fof(f280,plain,
( null_class = sF11
| sK7 = sK4(sF11) ),
inference(resolution,[],[f186,f269]) ).
fof(f298,definition,
( spl14_4
<=> sK7 = sK4(sF11) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f300,plain,
( sK7 = sK4(sF11)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f302,definition,
( spl14_5
<=> null_class = sF11 ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f304,plain,
( null_class = sF11
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f305,plain,
( spl14_4
| spl14_5 ),
inference(avatar_split_clause,[],[f280,f302,f298]) ).
fof(f307,definition,
( spl14_6
<=> sK6 = sK4(sF10) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f309,plain,
( sK6 = sK4(sF10)
| ~ spl14_6 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl14_7
<=> null_class = sF10 ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f313,plain,
( null_class = sF10
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,plain,
( spl14_6
| spl14_7 ),
inference(avatar_split_clause,[],[f278,f311,f307]) ).
fof(f324,plain,
( member(sK7,universal_class)
| null_class = sF11
| ~ spl14_4 ),
inference(superposition,[],[f187,f300]) ).
fof(f331,plain,
( null_class = sF11
| ~ spl14_4 ),
inference(forward_subsumption_resolution,[],[f324,f191]) ).
fof(f332,plain,
( spl14_5
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f331,f298,f302]) ).
fof(f337,plain,
( member(sK6,universal_class)
| null_class = sF10
| ~ spl14_6 ),
inference(superposition,[],[f187,f309]) ).
fof(f344,plain,
( null_class = sF10
| ~ spl14_6 ),
inference(forward_subsumption_resolution,[],[f337,f192]) ).
fof(f345,plain,
( spl14_7
| ~ spl14_6 ),
inference(avatar_split_clause,[],[f344,f307,f311]) ).
fof(f364,plain,
( member(null_class,sF8)
| ~ member(null_class,universal_class) ),
inference(superposition,[],[f235,f239]) ).
fof(f367,plain,
( member(sF11,sF12)
| ~ member(sF11,universal_class) ),
inference(superposition,[],[f235,f247]) ).
fof(f371,plain,
member(sF11,sF12),
inference(forward_subsumption_resolution,[],[f367,f251]) ).
fof(f374,definition,
( spl14_12
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f376,plain,
( ~ member(null_class,universal_class)
| spl14_12 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,definition,
( spl14_13
<=> member(null_class,sF8) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f380,plain,
( member(null_class,sF8)
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f381,plain,
( ~ spl14_12
| spl14_13 ),
inference(avatar_split_clause,[],[f364,f378,f374]) ).
fof(f383,plain,
( member(null_class,sF12)
| ~ spl14_5 ),
inference(forward_demodulation,[],[f371,f304]) ).
fof(f389,plain,
( member(null_class,universal_class)
| ~ spl14_5 ),
inference(superposition,[],[f251,f304]) ).
fof(f390,plain,
( $false
| ~ spl14_5
| spl14_12 ),
inference(forward_subsumption_resolution,[],[f389,f376]) ).
fof(f391,plain,
( ~ spl14_5
| spl14_12 ),
inference(avatar_contradiction_clause,[],[f390]) ).
fof(f421,plain,
! [X2,X0,X1] :
( subclass(unordered_pair(X0,X1),X2)
| sK0(unordered_pair(X0,X1),X2) = X1
| sK0(unordered_pair(X0,X1),X2) = X0 ),
inference(resolution,[],[f105,f111]) ).
fof(f422,plain,
! [X2,X0,X1] :
( member(sK0(unordered_pair(X0,X1),X2),universal_class)
| subclass(unordered_pair(X0,X1),X2) ),
inference(resolution,[],[f105,f112]) ).
fof(f425,plain,
! [X0] :
( subclass(sF8,X0)
| null_class = sK0(sF8,X0) ),
inference(resolution,[],[f105,f271]) ).
fof(f432,plain,
! [X0] :
( member(sK0(sF12,X0),universal_class)
| subclass(sF12,X0) ),
inference(resolution,[],[f105,f260]) ).
fof(f446,plain,
! [X2,X0,X1] :
( ~ subclass(X2,unordered_pair(X0,X1))
| sK0(unordered_pair(X0,X1),X2) = X0
| sK0(unordered_pair(X0,X1),X2) = X1
| unordered_pair(X0,X1) = X2 ),
inference(resolution,[],[f421,f110]) ).
fof(f462,plain,
! [X0] :
( ~ subclass(X0,sF8)
| null_class = sK0(sF8,X0)
| sF8 = X0 ),
inference(resolution,[],[f425,f110]) ).
fof(f915,plain,
! [X2,X3,X0,X1] :
( sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X3
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X0
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(resolution,[],[f446,f421]) ).
fof(f1235,definition,
( spl14_49
<=> sF8 = sF12 ),
introduced(definition,[new_symbols(definition,[spl14_49])],[avatar_definition]) ).
fof(f1236,plain,
( sF8 != sF12
| spl14_49 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1237,plain,
( sF8 = sF12
| ~ spl14_49 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1239,definition,
( spl14_50
<=> null_class = sK0(sF8,sF12) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
fof(f1241,plain,
( null_class = sK0(sF8,sF12)
| ~ spl14_50 ),
inference(avatar_component_clause,[],[f1239]) ).
fof(f1243,definition,
( spl14_51
<=> sK6 = sK0(sF12,sF8) ),
introduced(definition,[new_symbols(definition,[spl14_51])],[avatar_definition]) ).
fof(f1244,plain,
( sK6 != sK0(sF12,sF8)
| spl14_51 ),
inference(avatar_component_clause,[],[f1243]) ).
fof(f1245,plain,
( sK6 = sK0(sF12,sF8)
| ~ spl14_51 ),
inference(avatar_component_clause,[],[f1243]) ).
fof(f1247,definition,
( spl14_52
<=> null_class = sK0(sF12,sF8) ),
introduced(definition,[new_symbols(definition,[spl14_52])],[avatar_definition]) ).
fof(f1248,plain,
( null_class != sK0(sF12,sF8)
| spl14_52 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1249,plain,
( null_class = sK0(sF12,sF8)
| ~ spl14_52 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1554,plain,
( ~ member(null_class,sF8)
| subclass(sF12,sF8)
| ~ spl14_52 ),
inference(superposition,[],[f106,f1249]) ).
fof(f1555,plain,
( subclass(sF12,sF8)
| ~ spl14_13
| ~ spl14_52 ),
inference(forward_subsumption_resolution,[],[f1554,f380]) ).
fof(f1556,plain,
( null_class = sK0(sF8,sF12)
| sF8 = sF12
| ~ spl14_13
| ~ spl14_52 ),
inference(resolution,[],[f1555,f462]) ).
fof(f1557,plain,
( ~ subclass(sF8,sF12)
| sF8 = sF12
| ~ spl14_13
| ~ spl14_52 ),
inference(resolution,[],[f1555,f110]) ).
fof(f1559,definition,
( spl14_62
<=> subclass(sF8,sF12) ),
introduced(definition,[new_symbols(definition,[spl14_62])],[avatar_definition]) ).
fof(f1562,plain,
( spl14_49
| ~ spl14_62
| ~ spl14_13
| ~ spl14_52 ),
inference(avatar_split_clause,[],[f1557,f1247,f378,f1559,f1235]) ).
fof(f1563,plain,
( spl14_49
| spl14_50
| ~ spl14_13
| ~ spl14_52 ),
inference(avatar_split_clause,[],[f1556,f1247,f378,f1239,f1235]) ).
fof(f1569,definition,
( spl14_63
<=> subclass(sF12,sF8) ),
introduced(definition,[new_symbols(definition,[spl14_63])],[avatar_definition]) ).
fof(f1570,plain,
( ~ subclass(sF12,sF8)
| spl14_63 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1571,plain,
( subclass(sF12,sF8)
| ~ spl14_63 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1579,plain,
( null_class = sK0(sF8,sF12)
| sF8 = sF12
| ~ spl14_63 ),
inference(resolution,[],[f1571,f462]) ).
fof(f1580,plain,
( ~ subclass(sF8,sF12)
| sF8 = sF12
| ~ spl14_63 ),
inference(resolution,[],[f1571,f110]) ).
fof(f1581,plain,
( spl14_49
| ~ spl14_62
| ~ spl14_63 ),
inference(avatar_split_clause,[],[f1580,f1569,f1559,f1235]) ).
fof(f1582,plain,
( spl14_49
| spl14_50
| ~ spl14_63 ),
inference(avatar_split_clause,[],[f1579,f1569,f1239,f1235]) ).
fof(f1585,plain,
( ~ member(null_class,sF12)
| subclass(sF8,sF12)
| ~ spl14_50 ),
inference(superposition,[],[f106,f1241]) ).
fof(f1586,plain,
( subclass(sF8,sF12)
| ~ spl14_5
| ~ spl14_50 ),
inference(forward_subsumption_resolution,[],[f1585,f383]) ).
fof(f1590,plain,
( sF13 = unordered_pair(sF10,sF8)
| ~ spl14_49 ),
inference(superposition,[],[f249,f1237]) ).
fof(f1609,plain,
( unordered_pair(null_class,sF8) = sF13
| ~ spl14_7
| ~ spl14_49 ),
inference(forward_demodulation,[],[f1590,f313]) ).
fof(f1612,plain,
( sF9 = sF13
| ~ spl14_7
| ~ spl14_49 ),
inference(forward_demodulation,[],[f1609,f241]) ).
fof(f1613,plain,
( $false
| ~ spl14_7
| ~ spl14_49 ),
inference(forward_subsumption_resolution,[],[f1612,f250]) ).
fof(f1614,plain,
( ~ spl14_7
| ~ spl14_49 ),
inference(avatar_contradiction_clause,[],[f1613]) ).
fof(f1864,plain,
( member(sK6,universal_class)
| subclass(sF12,sF8)
| ~ spl14_51 ),
inference(superposition,[],[f432,f1245]) ).
fof(f1866,plain,
( subclass(sF12,sF8)
| ~ spl14_51 ),
inference(forward_subsumption_resolution,[],[f1864,f192]) ).
fof(f1867,plain,
( $false
| ~ spl14_51
| spl14_63 ),
inference(forward_subsumption_resolution,[],[f1866,f1570]) ).
fof(f1868,plain,
( ~ spl14_51
| spl14_63 ),
inference(avatar_contradiction_clause,[],[f1867]) ).
fof(f1869,plain,
( spl14_62
| ~ spl14_5
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f1586,f1239,f302,f1559]) ).
fof(f2055,plain,
! [X2,X3,X0,X1] :
( member(X0,universal_class)
| subclass(unordered_pair(X0,X1),unordered_pair(X2,X3))
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X3
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(superposition,[],[f422,f915]) ).
fof(f2058,plain,
! [X2,X3,X0,X1] :
( ~ member(X0,unordered_pair(X2,X3))
| subclass(unordered_pair(X0,X1),unordered_pair(X2,X3))
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X3
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(superposition,[],[f106,f915]) ).
fof(f2119,plain,
! [X2,X3,X0,X1] :
( ~ member(X0,unordered_pair(X2,X3))
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X3
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(forward_subsumption_resolution,[],[f2058,f446]) ).
fof(f2122,plain,
! [X2,X3,X0,X1] :
( member(X0,universal_class)
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X3
| sK0(unordered_pair(X2,X3),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X2,X3)) = X1
| unordered_pair(X0,X1) = unordered_pair(X2,X3) ),
inference(forward_subsumption_resolution,[],[f2055,f446]) ).
fof(f2227,plain,
! [X2,X0,X1] :
( sK0(unordered_pair(X0,X1),unordered_pair(X1,X2)) = X1
| sK0(unordered_pair(X0,X1),unordered_pair(X1,X2)) = X0
| sK0(unordered_pair(X1,X2),unordered_pair(X0,X1)) = X2
| unordered_pair(X1,X2) = unordered_pair(X0,X1)
| ~ member(X1,universal_class) ),
inference(resolution,[],[f2119,f235]) ).
fof(f2260,plain,
! [X2,X0,X1] :
( sK0(unordered_pair(X1,X2),unordered_pair(X0,X1)) = X2
| sK0(unordered_pair(X0,X1),unordered_pair(X1,X2)) = X1
| sK0(unordered_pair(X0,X1),unordered_pair(X1,X2)) = X0
| unordered_pair(X1,X2) = unordered_pair(X0,X1) ),
inference(forward_subsumption_resolution,[],[f2227,f2122]) ).
fof(f2340,plain,
! [X2,X0,X1] :
( member(X0,universal_class)
| subclass(unordered_pair(X1,X0),unordered_pair(X2,X1))
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X1
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X2
| unordered_pair(X1,X0) = unordered_pair(X2,X1) ),
inference(superposition,[],[f422,f2260]) ).
fof(f2343,plain,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X2,X1))
| subclass(unordered_pair(X1,X0),unordered_pair(X2,X1))
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X1
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X2
| unordered_pair(X1,X0) = unordered_pair(X2,X1) ),
inference(superposition,[],[f106,f2260]) ).
fof(f2380,plain,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X2,X1))
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X1
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X2
| unordered_pair(X1,X0) = unordered_pair(X2,X1) ),
inference(forward_subsumption_resolution,[],[f2343,f446]) ).
fof(f2383,plain,
! [X2,X0,X1] :
( member(X0,universal_class)
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X1
| sK0(unordered_pair(X2,X1),unordered_pair(X1,X0)) = X2
| unordered_pair(X1,X0) = unordered_pair(X2,X1) ),
inference(forward_subsumption_resolution,[],[f2340,f446]) ).
fof(f2510,plain,
! [X0,X1] :
( sK0(unordered_pair(X0,X1),unordered_pair(X1,X1)) = X1
| sK0(unordered_pair(X0,X1),unordered_pair(X1,X1)) = X0
| unordered_pair(X0,X1) = unordered_pair(X1,X1)
| ~ member(X1,universal_class) ),
inference(resolution,[],[f2380,f235]) ).
fof(f2543,plain,
! [X0,X1] :
( sK0(unordered_pair(X0,X1),unordered_pair(X1,X1)) = X1
| sK0(unordered_pair(X0,X1),unordered_pair(X1,X1)) = X0
| unordered_pair(X0,X1) = unordered_pair(X1,X1) ),
inference(forward_subsumption_resolution,[],[f2510,f2383]) ).
fof(f2553,plain,
( sF11 = sK0(sF12,unordered_pair(sF11,sF11))
| sK6 = sK0(sF12,unordered_pair(sF11,sF11))
| sF12 = unordered_pair(sF11,sF11) ),
inference(superposition,[],[f2543,f247]) ).
fof(f2617,plain,
( null_class = sK0(sF12,unordered_pair(null_class,null_class))
| sK6 = sK0(sF12,unordered_pair(sF11,sF11))
| sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5 ),
inference(forward_demodulation,[],[f2553,f304]) ).
fof(f2629,plain,
( null_class = sK0(sF12,sF8)
| sK6 = sK0(sF12,unordered_pair(sF11,sF11))
| sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5 ),
inference(forward_demodulation,[],[f2617,f239]) ).
fof(f2637,plain,
( sK6 = sK0(sF12,unordered_pair(sF11,sF11))
| sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5
| spl14_52 ),
inference(forward_subsumption_resolution,[],[f2629,f1248]) ).
fof(f2643,plain,
( sK6 = sK0(sF12,unordered_pair(null_class,null_class))
| sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5
| spl14_52 ),
inference(forward_demodulation,[],[f2637,f304]) ).
fof(f2649,plain,
( sK6 = sK0(sF12,sF8)
| sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5
| spl14_52 ),
inference(forward_demodulation,[],[f2643,f239]) ).
fof(f2656,plain,
( sF12 = unordered_pair(sF11,sF11)
| ~ spl14_5
| spl14_51
| spl14_52 ),
inference(forward_subsumption_resolution,[],[f2649,f1244]) ).
fof(f2660,plain,
( unordered_pair(null_class,null_class) = sF12
| ~ spl14_5
| spl14_51
| spl14_52 ),
inference(forward_demodulation,[],[f2656,f304]) ).
fof(f2662,plain,
( sF8 = sF12
| ~ spl14_5
| spl14_51
| spl14_52 ),
inference(forward_demodulation,[],[f2660,f239]) ).
fof(f2665,plain,
( $false
| ~ spl14_5
| spl14_49
| spl14_51
| spl14_52 ),
inference(forward_subsumption_resolution,[],[f2662,f1236]) ).
fof(f2666,plain,
( ~ spl14_5
| spl14_49
| spl14_51
| spl14_52 ),
inference(avatar_contradiction_clause,[],[f2665]) ).
cnf(s2,plain,
( spl14_4
| spl14_5 ),
inference(sat_conversion,[],[f305]) ).
cnf(s3,plain,
( spl14_6
| spl14_7 ),
inference(sat_conversion,[],[f314]) ).
cnf(s6,plain,
( ~ spl14_4
| spl14_5 ),
inference(sat_conversion,[],[f332]) ).
cnf(s8,plain,
( ~ spl14_6
| spl14_7 ),
inference(sat_conversion,[],[f345]) ).
cnf(s9,plain,
( ~ spl14_12
| spl14_13 ),
inference(sat_conversion,[],[f381]) ).
cnf(s10,plain,
( ~ spl14_5
| spl14_12 ),
inference(sat_conversion,[],[f391]) ).
cnf(s79,plain,
( ~ spl14_13
| spl14_49
| ~ spl14_52
| ~ spl14_62 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s80,plain,
( ~ spl14_13
| spl14_49
| spl14_50
| ~ spl14_52 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s84,plain,
( spl14_49
| ~ spl14_62
| ~ spl14_63 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s85,plain,
( spl14_49
| spl14_50
| ~ spl14_63 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s90,plain,
( ~ spl14_7
| ~ spl14_49 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s100,plain,
( ~ spl14_51
| spl14_63 ),
inference(sat_conversion,[],[f1868]) ).
cnf(s101,plain,
( ~ spl14_5
| ~ spl14_50
| spl14_62 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s118,plain,
( ~ spl14_5
| spl14_49
| spl14_51
| spl14_52 ),
inference(sat_conversion,[],[f2666]) ).
cnf(s134,plain,
spl14_5,
inference(rat,[],[s2,s6]) ).
cnf(s136,plain,
spl14_12,
inference(rat,[],[s10,s134]) ).
cnf(s139,plain,
spl14_13,
inference(rat,[],[s9,s136]) ).
cnf(s140,plain,
( spl14_50
| spl14_49 ),
inference(rat,[],[s118,s100,s80,s85,s139,s134]) ).
cnf(s141,plain,
( ~ spl14_62
| spl14_49 ),
inference(rat,[],[s118,s100,s79,s84,s139,s134]) ).
cnf(s142,plain,
spl14_49,
inference(rat,[],[s141,s101,s140,s134]) ).
cnf(s143,plain,
~ spl14_7,
inference(rat,[],[s90,s142]) ).
cnf(s145,plain,
~ spl14_6,
inference(rat,[],[s8,s143]) ).
cnf(s146,plain,
$false,
inference(rat,[],[s3,s143,s145]) ).
fof(f2667,plain,
$false,
inference(avatar_sat_refutation,[],[s146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET105+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n002.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 : Mon Sep 28 00:46:51 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.76/2.94 % (4056736)Detected formulas, will run a generic FOF schedule.
% 13.76/2.94 % (4056789)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3973095124:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.76/2.94 % (4056794)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1390214138:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.76/2.94 % (4056792)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4222588721:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.76/2.94 % (4056793)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1117567882:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.76/2.94 % (4056791)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3563778369:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.76/2.94 % (4056792)Refutation not found, incomplete strategy
% 13.76/2.94 % (4056792)------------------------------
% 13.76/2.94 % (4056792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056792)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056792)Termination reason: Refutation not found, incomplete strategy
% 13.76/2.94 % (4056792)Time elapsed: 0.002 s
% 13.76/2.94 % (4056792)Peak memory usage: 88 MB
% 13.76/2.94 % (4056792)Instructions burned: 1 (million)
% 13.76/2.94 % (4056793)Refutation not found, incomplete strategy
% 13.76/2.94 % (4056793)------------------------------
% 13.76/2.94 % (4056793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056793)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056793)Termination reason: Refutation not found, incomplete strategy
% 13.76/2.94 % (4056793)Time elapsed: 0.002 s
% 13.76/2.94 % (4056793)Peak memory usage: 87 MB
% 13.76/2.94 % (4056793)Instructions burned: 1 (million)
% 13.76/2.94 % (4056795)dis-21_1_sil=8000:lcm=predicate:random_seed=3569609331:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.76/2.94 % (4056790)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2557997935:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.76/2.94 % (4056795)Instruction limit reached!
% 13.76/2.94 % (4056795)------------------------------
% 13.76/2.94 % (4056795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056795)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056795)Termination reason: Instruction limit
% 13.76/2.94 % (4056795)Termination phase: Saturation
% 13.76/2.94 % (4056795)Time elapsed: 0.089 s
% 13.76/2.94 % (4056795)Peak memory usage: 89 MB
% 13.76/2.94 % (4056795)Instructions burned: 130 (million)
% 13.76/2.94 % (4056794)Instruction limit reached!
% 13.76/2.94 % (4056794)------------------------------
% 13.76/2.94 % (4056794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056794)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056794)Termination reason: Instruction limit
% 13.76/2.94 % (4056794)Termination phase: Saturation
% 13.76/2.94 % (4056794)Time elapsed: 0.121 s
% 13.76/2.94 % (4056794)Peak memory usage: 90 MB
% 13.76/2.94 % (4056794)Instructions burned: 142 (million)
% 13.76/2.94 % (4056792)------------------------------
% 13.76/2.94 % (4056792)------------------------------
% 13.76/2.94 % (4056793)------------------------------
% 13.76/2.94 % (4056793)------------------------------
% 13.76/2.94 % (4056811)lrs+10_1_sil=8000:sp=occurrence:random_seed=4116763925:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.76/2.94 % (4056812)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4086336966:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.76/2.94 % (4056817)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1939333019:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 13.76/2.94 % (4056812)Instruction limit reached!
% 13.76/2.94 % (4056812)------------------------------
% 13.76/2.94 % (4056812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056812)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056812)Termination reason: Instruction limit
% 13.76/2.94 % (4056812)Termination phase: Saturation
% 13.76/2.94 % (4056812)Time elapsed: 0.133 s
% 13.76/2.94 % (4056812)Peak memory usage: 89 MB
% 13.76/2.94 % (4056812)Instructions burned: 157 (million)
% 13.76/2.94 % (4056821)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4094781823:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 13.76/2.94 % (4056811)Instruction limit reached!
% 13.76/2.94 % (4056811)------------------------------
% 13.76/2.94 % (4056811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056811)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056811)Termination reason: Instruction limit
% 13.76/2.94 % (4056811)Termination phase: Saturation
% 13.76/2.94 % (4056811)Time elapsed: 0.277 s
% 13.76/2.94 % (4056811)Peak memory usage: 92 MB
% 13.76/2.94 % (4056811)Instructions burned: 286 (million)
% 13.76/2.94 % (4056826)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=59561445:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 13.76/2.94 % (4056821)Instruction limit reached!
% 13.76/2.94 % (4056821)------------------------------
% 13.76/2.94 % (4056821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056821)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056821)Termination reason: Instruction limit
% 13.76/2.94 % (4056821)Termination phase: Saturation
% 13.76/2.94 % (4056821)Time elapsed: 0.145 s
% 13.76/2.94 % (4056821)Peak memory usage: 92 MB
% 13.76/2.94 % (4056821)Instructions burned: 248 (million)
% 13.76/2.94 % (4056831)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1741644188:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 13.76/2.94 % (4056817)Instruction limit reached!
% 13.76/2.94 % (4056817)------------------------------
% 13.76/2.94 % (4056817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056817)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056817)Termination reason: Instruction limit
% 13.76/2.94 % (4056817)Termination phase: Saturation
% 13.76/2.94 % (4056817)Time elapsed: 0.339 s
% 13.76/2.94 % (4056817)Peak memory usage: 92 MB
% 13.76/2.94 % (4056817)Instructions burned: 325 (million)
% 13.76/2.94 % (4056826)Instruction limit reached!
% 13.76/2.94 % (4056826)------------------------------
% 13.76/2.94 % (4056826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056826)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056826)Termination reason: Instruction limit
% 13.76/2.94 % (4056826)Termination phase: Saturation
% 13.76/2.94 % (4056826)Time elapsed: 0.154 s
% 13.76/2.94 % (4056826)Peak memory usage: 89 MB
% 13.76/2.94 % (4056826)Instructions burned: 294 (million)
% 13.76/2.94 % (4056833)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1404005287:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 13.76/2.94 % (4056833)Instruction limit reached!
% 13.76/2.94 % (4056833)------------------------------
% 13.76/2.94 % (4056833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056833)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056833)Termination reason: Instruction limit
% 13.76/2.94 % (4056833)Termination phase: Saturation
% 13.76/2.94 % (4056833)Time elapsed: 0.060 s
% 13.76/2.94 % (4056833)Peak memory usage: 90 MB
% 13.76/2.94 % (4056833)Instructions burned: 115 (million)
% 13.76/2.94 % (4056835)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1017487418:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 13.76/2.94 % (4056836)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2736066340:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 13.76/2.94 % (4056835)Instruction limit reached!
% 13.76/2.94 % (4056835)------------------------------
% 13.76/2.94 % (4056835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056835)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056835)Termination reason: Instruction limit
% 13.76/2.94 % (4056835)Termination phase: Saturation
% 13.76/2.94 % (4056835)Time elapsed: 0.066 s
% 13.76/2.94 % (4056835)Peak memory usage: 89 MB
% 13.76/2.94 % (4056835)Instructions burned: 127 (million)
% 13.76/2.94 % (4056836)Instruction limit reached!
% 13.76/2.94 % (4056836)------------------------------
% 13.76/2.94 % (4056836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.94 % (4056836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.94 % (4056836)CaDiCaL version: 2.1.3
% 13.76/2.94 % (4056836)Termination reason: Instruction limit
% 13.76/2.94 % (4056836)Termination phase: Saturation
% 13.76/2.94 % (4056836)Time elapsed: 0.067 s
% 13.76/2.94 % (4056836)Peak memory usage: 88 MB
% 13.76/2.94 % (4056836)Instructions burned: 115 (million)
% 13.76/2.94 % (4056840)lrs+10_1_sil=8000:sp=occurrence:random_seed=3239112876:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 13.76/2.95 % (4056847)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1928079088:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 13.76/2.95 % (4056847)Refutation not found, incomplete strategy
% 13.76/2.95 % (4056847)------------------------------
% 13.76/2.95 % (4056847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.95 % (4056847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.95 % (4056847)CaDiCaL version: 2.1.3
% 13.76/2.95 % (4056847)Termination reason: Refutation not found, incomplete strategy
% 13.76/2.95 % (4056847)Time elapsed: 0.002 s
% 13.76/2.95 % (4056847)Peak memory usage: 88 MB
% 13.76/2.95 % (4056847)Instructions burned: 1 (million)
% 13.76/2.95 % (4056866)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3061940016:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 13.76/2.95 % (4056847)------------------------------
% 13.76/2.95 % (4056847)------------------------------
% 13.76/2.95 % (4056955)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3255593381:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 13.76/2.95 % (4056831)First to succeed.
% 13.76/2.95 % (4056831)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4056736"
% 13.76/2.95 % (4056955)Instruction limit reached!
% 13.76/2.95 % (4056955)------------------------------
% 13.76/2.95 % (4056955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.95 % (4056955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.95 % (4056955)CaDiCaL version: 2.1.3
% 13.76/2.95 % (4056955)Termination reason: Instruction limit
% 13.76/2.95 % (4056955)Termination phase: Saturation
% 13.76/2.95 % (4056955)Time elapsed: 0.072 s
% 13.76/2.95 % (4056955)Peak memory usage: 89 MB
% 13.76/2.95 % (4056955)Instructions burned: 135 (million)
% 13.76/2.95 % (4056840)Instruction limit reached!
% 13.76/2.95 % (4056840)------------------------------
% 13.76/2.95 % (4056840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.76/2.95 % (4056840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.76/2.95 % (4056840)CaDiCaL version: 2.1.3
% 13.76/2.95 % (4056840)Termination reason: Instruction limit
% 13.76/2.95 % (4056840)Termination phase: Saturation
% 13.76/2.95 % (4056840)Time elapsed: 0.577 s
% 13.76/2.95 % (4056840)Peak memory usage: 97 MB
% 13.76/2.95 % (4056840)Instructions burned: 907 (million)
% 13.76/2.95 % (4057001)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=896588330:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 13.76/2.95 % (4056831)Refutation found. Thanks to Tanya!
% 13.76/2.95 % SZS status Theorem for theBenchmark
% 13.76/2.95 % SZS output start Proof for theBenchmark
% See solution above
% 15.25/3.15 % (4056831)------------------------------
% 15.25/3.15 % (4056831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.25/3.15 % (4056831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.25/3.15 % (4056831)CaDiCaL version: 2.1.3
% 15.25/3.15 % (4056831)Termination reason: Refutation
% 15.25/3.15 % (4056831)Time elapsed: 0.806 s
% 15.25/3.15 % (4056831)Peak memory usage: 132 MB
% 15.25/3.15 % (4056831)Instructions burned: 1195 (million)
% 15.25/3.15 % (4056831)------------------------------
% 15.25/3.15 % (4056831)------------------------------
% 15.25/3.15 % (4056736)Success in time 2.083 s
% 15.25/3.15 % Vampire exiting
%------------------------------------------------------------------------------