%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU078+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:51:53 PM UTC 2026
% Result : Theorem 49.22s 14.85s
% Output : Refutation 49.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 30
% Syntax : Number of formulae : 185 ( 25 unt; 12 def)
% Number of atoms : 513 ( 72 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 525 ( 197 ~; 255 |; 24 &)
% ( 34 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 13 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-2 aty)
% Number of variables : 189 ( 1 sgn 178 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] :
( empty(X0)
=> function(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_funct_1) ).
fof(f3,axiom,
! [X0] :
( empty(X0)
=> relation(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relat_1) ).
fof(f5,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_funct_1) ).
fof(f6,axiom,
! [X0,X1] :
( X1 = singleton(X0)
<=> ! [X2] :
( in(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
fof(f7,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f9,axiom,
( empty(empty_set)
& relation(empty_set)
& relation_empty_yielding(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(f16,axiom,
! [X0] :
( empty(X0)
=> ( empty(relation_dom(X0))
& relation(relation_dom(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_relat_1) ).
fof(f17,axiom,
! [X0] :
( empty(X0)
=> ( empty(relation_rng(X0))
& relation(relation_rng(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc8_relat_1) ).
fof(f28,axiom,
! [X0,X1] : subset(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f29,axiom,
! [X0,X1] :
( disjoint(X0,X1)
=> disjoint(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r1_xboole_0) ).
fof(f30,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( ! [X1] :
~ ( in(X1,relation_rng(X0))
& ! [X2] : relation_inverse_image(X0,singleton(X1)) != singleton(X2) )
<=> one_to_one(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t144_funct_1) ).
fof(f31,conjecture,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
<=> ! [X1] :
? [X2] : subset(relation_inverse_image(X0,singleton(X1)),singleton(X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t159_funct_1) ).
fof(f32,negated_conjecture,
~ ! [X0] :
( ( relation(X0)
& function(X0) )
=> ( one_to_one(X0)
<=> ! [X1] :
? [X2] : subset(relation_inverse_image(X0,singleton(X1)),singleton(X2)) ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f33,axiom,
! [X0,X1] :
( relation(X1)
=> ( relation_inverse_image(X1,X0) = empty_set
<=> disjoint(relation_rng(X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t173_relat_1) ).
fof(f36,axiom,
! [X0] : subset(empty_set,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_xboole_1) ).
fof(f37,axiom,
! [X0,X1] :
( subset(X0,singleton(X1))
<=> ( X0 = empty_set
| X0 = singleton(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_zfmisc_1) ).
fof(f40,axiom,
! [X0,X1] :
( ~ in(X0,X1)
=> disjoint(singleton(X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_zfmisc_1) ).
fof(f42,axiom,
! [X0] :
( empty(X0)
=> X0 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(f43,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f45,plain,
! [X0] : subset(X0,X0),
inference(rectify,[],[f28]) ).
fof(f46,plain,
( empty(empty_set)
& relation(empty_set) ),
inference(pure_predicate_removal,[],[f9]) ).
fof(f49,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f50,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f53,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f54,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f53]) ).
fof(f55,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f56,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f55]) ).
fof(f61,plain,
! [X0] :
( ( empty(relation_dom(X0))
& relation(relation_dom(X0)) )
| ~ empty(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f62,plain,
! [X0] :
( ( empty(relation_rng(X0))
& relation(relation_rng(X0)) )
| ~ empty(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f64,plain,
! [X0,X1] :
( disjoint(X1,X0)
| ~ disjoint(X0,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f65,plain,
! [X0] :
( ( ! [X1] :
( ~ in(X1,relation_rng(X0))
| ? [X2] : relation_inverse_image(X0,singleton(X1)) = singleton(X2) )
<=> one_to_one(X0) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f66,plain,
! [X0] :
( ( ! [X1] :
( ~ in(X1,relation_rng(X0))
| ? [X2] : relation_inverse_image(X0,singleton(X1)) = singleton(X2) )
<=> one_to_one(X0) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f65]) ).
fof(f67,plain,
? [X0] :
( ( one_to_one(X0)
<~> ! [X1] :
? [X2] : subset(relation_inverse_image(X0,singleton(X1)),singleton(X2)) )
& relation(X0)
& function(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f68,plain,
? [X0] :
( ( one_to_one(X0)
<~> ! [X1] :
? [X2] : subset(relation_inverse_image(X0,singleton(X1)),singleton(X2)) )
& relation(X0)
& function(X0) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( ( relation_inverse_image(X1,X0) = empty_set
<=> disjoint(relation_rng(X1),X0) )
| ~ relation(X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f75,plain,
! [X0,X1] :
( disjoint(singleton(X0),X1)
| in(X0,X1) ),
inference(ennf_transformation,[],[f40]) ).
fof(f77,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f78,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f43]) ).
fof(f81,plain,
! [X0] :
( ~ empty(X0)
| function(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f82,plain,
! [X0] :
( ~ empty(X0)
| relation(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f89,plain,
! [X2,X3,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(apply(X0,X3),X1)
| ~ in(X3,relation_dom(X0))
| in(X3,X2)
| relation_inverse_image(X0,X1) != X2 ),
inference(cnf_transformation,[],[f54]) ).
fof(f90,plain,
! [X2,X0,X1] :
( X0 != X2
| in(X2,X1)
| singleton(X0) != X1 ),
inference(cnf_transformation,[],[f6]) ).
fof(f97,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| apply(X0,sK3(X0,X2)) = X2
| ~ in(X2,X1)
| relation_rng(X0) != X1 ),
inference(cnf_transformation,[],[f56]) ).
fof(f98,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| in(sK3(X0,X2),relation_dom(X0))
| ~ in(X2,X1)
| relation_rng(X0) != X1 ),
inference(cnf_transformation,[],[f56]) ).
fof(f102,plain,
empty(empty_set),
inference(cnf_transformation,[],[f46]) ).
fof(f111,plain,
! [X0] :
( empty(relation_dom(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f113,plain,
! [X0] :
( empty(relation_rng(X0))
| ~ empty(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f133,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[],[f45]) ).
fof(f134,plain,
! [X0,X1] :
( ~ disjoint(X0,X1)
| disjoint(X1,X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f135,plain,
! [X2,X0] :
( ~ function(X0)
| ~ relation(X0)
| one_to_one(X0)
| singleton(X2) != relation_inverse_image(X0,singleton(sK16(X0))) ),
inference(cnf_transformation,[],[f66]) ).
fof(f136,plain,
! [X0] :
( ~ function(X0)
| ~ relation(X0)
| one_to_one(X0)
| in(sK16(X0),relation_rng(X0)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f137,plain,
! [X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ one_to_one(X0)
| relation_inverse_image(X0,singleton(X1)) = singleton(sK17(X0,X1))
| ~ in(X1,relation_rng(X0)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f138,plain,
! [X1] :
( subset(relation_inverse_image(sK18,singleton(X1)),singleton(sK20(X1)))
| one_to_one(sK18) ),
inference(cnf_transformation,[],[f68]) ).
fof(f139,plain,
! [X2] :
( ~ subset(relation_inverse_image(sK18,singleton(sK19)),singleton(X2))
| ~ one_to_one(sK18) ),
inference(cnf_transformation,[],[f68]) ).
fof(f140,plain,
function(sK18),
inference(cnf_transformation,[],[f68]) ).
fof(f141,plain,
relation(sK18),
inference(cnf_transformation,[],[f68]) ).
fof(f142,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ disjoint(relation_rng(X1),X0)
| empty_set = relation_inverse_image(X1,X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f146,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f147,plain,
! [X0,X1] :
( ~ subset(X0,singleton(X1))
| empty_set = X0
| singleton(X1) = X0 ),
inference(cnf_transformation,[],[f37]) ).
fof(f153,plain,
! [X0,X1] :
( in(X0,X1)
| disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f155,plain,
! [X0] :
( ~ empty(X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f77]) ).
fof(f156,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f158,plain,
! [X3,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(apply(X0,X3),X1)
| ~ in(X3,relation_dom(X0))
| in(X3,relation_inverse_image(X0,X1)) ),
inference(equality_resolution,[],[f89]) ).
fof(f162,plain,
! [X2,X1] :
( in(X2,X1)
| singleton(X2) != X1 ),
inference(equality_resolution,[],[f90]) ).
fof(f163,plain,
! [X2] : in(X2,singleton(X2)),
inference(equality_resolution,[],[f162]) ).
fof(f166,plain,
! [X2,X0] :
( ~ function(X0)
| ~ relation(X0)
| in(sK3(X0,X2),relation_dom(X0))
| ~ in(X2,relation_rng(X0)) ),
inference(equality_resolution,[],[f98]) ).
fof(f167,plain,
! [X2,X0] :
( ~ function(X0)
| ~ relation(X0)
| apply(X0,sK3(X0,X2)) = X2
| ~ in(X2,relation_rng(X0)) ),
inference(equality_resolution,[],[f97]) ).
fof(f171,plain,
! [X0] :
( ~ function(X0)
| ~ empty(X0) ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f172,plain,
! [X0] :
( ~ relation(X0)
| ~ empty(X0) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f174,plain,
! [X3,X0,X1] :
( in(apply(X0,X3),X1)
| relation(X0)
| function(X0)
| in(X3,relation_dom(X0))
| ~ in(X3,relation_inverse_image(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f183,plain,
! [X2] : ~ in(X2,singleton(X2)),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f185,plain,
! [X2,X0] :
( ~ in(sK3(X0,X2),relation_dom(X0))
| relation(X0)
| function(X0)
| in(X2,relation_rng(X0)) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f186,plain,
! [X2,X0] :
( in(X2,relation_rng(X0))
| relation(X0)
| apply(X0,sK3(X0,X2)) = X2
| function(X0) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f205,plain,
! [X0,X1] :
( ~ one_to_one(X0)
| relation(X0)
| function(X0)
| relation_inverse_image(X0,singleton(X1)) = singleton(sK17(X0,X1))
| in(X1,relation_rng(X0)) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f206,plain,
! [X0] :
( ~ in(sK16(X0),relation_rng(X0))
| relation(X0)
| one_to_one(X0)
| function(X0) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f207,plain,
! [X2,X0] :
( singleton(X2) != relation_inverse_image(X0,singleton(sK16(X0)))
| relation(X0)
| one_to_one(X0)
| function(X0) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f208,plain,
~ relation(sK18),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f209,plain,
~ function(sK18),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f211,plain,
! [X0,X1] :
( ~ disjoint(relation_rng(X1),X0)
| relation(X1)
| empty_set = relation_inverse_image(X1,X0) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f215,plain,
! [X0,X1] :
( disjoint(singleton(X0),X1)
| ~ in(X0,X1) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f217,plain,
! [X0,X1] :
( in(X0,X1)
| ~ empty(X1) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f219,definition,
( spl21_1
<=> one_to_one(sK18) ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
fof(f220,plain,
( ~ one_to_one(sK18)
| spl21_1 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f221,plain,
( one_to_one(sK18)
| ~ spl21_1 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f223,definition,
( spl21_2
<=> ! [X1] : subset(relation_inverse_image(sK18,singleton(X1)),singleton(sK20(X1))) ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
fof(f224,plain,
( ! [X1] : subset(relation_inverse_image(sK18,singleton(X1)),singleton(sK20(X1)))
| ~ spl21_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( spl21_1
| spl21_2 ),
inference(avatar_split_clause,[],[f138,f223,f219]) ).
fof(f227,definition,
( spl21_3
<=> ! [X2] : ~ subset(relation_inverse_image(sK18,singleton(sK19)),singleton(X2)) ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
fof(f228,plain,
( ! [X2] : ~ subset(relation_inverse_image(sK18,singleton(sK19)),singleton(X2))
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f227]) ).
fof(f229,plain,
( ~ spl21_1
| spl21_3 ),
inference(avatar_split_clause,[],[f139,f227,f219]) ).
fof(f231,plain,
! [X0] :
( ~ empty(X0)
| relation_rng(X0) = empty_set ),
inference(resolution,[],[f155,f113]) ).
fof(f282,plain,
! [X0,X1] :
( disjoint(X1,singleton(X0))
| ~ in(X0,X1) ),
inference(resolution,[],[f215,f134]) ).
fof(f300,definition,
( spl21_4
<=> ! [X1] : in(X1,empty_set) ),
introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition]) ).
fof(f301,plain,
( ! [X1] : in(X1,empty_set)
| ~ spl21_4 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f316,plain,
( ! [X0] :
( relation_inverse_image(sK18,singleton(X0)) = singleton(sK20(X0))
| empty_set = relation_inverse_image(sK18,singleton(X0)) )
| ~ spl21_2 ),
inference(resolution,[],[f147,f224]) ).
fof(f367,plain,
! [X0,X1] :
( ~ empty(relation_dom(X0))
| function(X0)
| in(X1,relation_rng(X0))
| relation(X0) ),
inference(resolution,[],[f185,f217]) ).
fof(f378,definition,
( spl21_8
<=> empty_set = relation_inverse_image(sK18,singleton(sK16(sK18))) ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f380,plain,
( empty_set = relation_inverse_image(sK18,singleton(sK16(sK18)))
| ~ spl21_8 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl21_9
<=> ! [X0] : singleton(X0) != singleton(sK20(sK16(sK18))) ),
introduced(definition,[new_symbols(definition,[spl21_9])],[avatar_definition]) ).
fof(f383,plain,
( ! [X0] : singleton(X0) != singleton(sK20(sK16(sK18)))
| ~ spl21_9 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f391,definition,
( spl21_10
<=> empty_set = relation_inverse_image(sK18,singleton(sK19)) ),
introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition]) ).
fof(f393,plain,
( empty_set = relation_inverse_image(sK18,singleton(sK19))
| ~ spl21_10 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f402,plain,
! [X0] :
( relation(X0)
| sK16(X0) = apply(X0,sK3(X0,sK16(X0)))
| function(X0)
| relation(X0)
| one_to_one(X0)
| function(X0) ),
inference(resolution,[],[f186,f206]) ).
fof(f403,plain,
! [X0] :
( one_to_one(X0)
| sK16(X0) = apply(X0,sK3(X0,sK16(X0)))
| function(X0)
| relation(X0) ),
inference(duplicate_literal_removal,[],[f402]) ).
fof(f407,plain,
! [X0,X1] :
( ~ in(X1,relation_inverse_image(X0,singleton(apply(X0,X1))))
| function(X0)
| in(X1,relation_dom(X0))
| relation(X0) ),
inference(resolution,[],[f174,f183]) ).
fof(f420,plain,
( ! [X0] :
( relation(sK18)
| function(sK18)
| relation_inverse_image(sK18,singleton(X0)) = singleton(sK17(sK18,X0))
| in(X0,relation_rng(sK18)) )
| ~ spl21_1 ),
inference(resolution,[],[f205,f221]) ).
fof(f421,plain,
( ! [X0] :
( function(sK18)
| relation_inverse_image(sK18,singleton(X0)) = singleton(sK17(sK18,X0))
| in(X0,relation_rng(sK18)) )
| ~ spl21_1 ),
inference(forward_subsumption_resolution,[],[f420,f208]) ).
fof(f424,plain,
( ! [X0] :
( in(X0,relation_rng(sK18))
| relation_inverse_image(sK18,singleton(X0)) = singleton(sK17(sK18,X0)) )
| ~ spl21_1 ),
inference(forward_subsumption_resolution,[],[f421,f209]) ).
fof(f479,plain,
empty_set = relation_rng(empty_set),
inference(resolution,[],[f231,f102]) ).
fof(f517,plain,
! [X0,X1] :
( ~ in(X0,relation_rng(X1))
| relation(X1)
| empty_set = relation_inverse_image(X1,singleton(X0)) ),
inference(resolution,[],[f282,f211]) ).
fof(f658,plain,
! [X0,X1] :
( function(X0)
| in(X1,relation_rng(X0))
| relation(X0)
| ~ empty(X0) ),
inference(resolution,[],[f367,f111]) ).
fof(f661,plain,
! [X0,X1] :
( in(X1,relation_rng(X0))
| relation(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[],[f658,f171]) ).
fof(f663,plain,
! [X0,X1] :
( ~ empty(X0)
| in(X1,relation_rng(X0)) ),
inference(forward_subsumption_resolution,[],[f661,f172]) ).
fof(f2804,plain,
( ! [X0] :
( relation(sK18)
| empty_set = relation_inverse_image(sK18,singleton(X0))
| relation_inverse_image(sK18,singleton(X0)) = singleton(sK17(sK18,X0)) )
| ~ spl21_1 ),
inference(resolution,[],[f517,f424]) ).
fof(f2832,plain,
( ! [X0] :
( relation_inverse_image(sK18,singleton(X0)) = singleton(sK17(sK18,X0))
| empty_set = relation_inverse_image(sK18,singleton(X0)) )
| ~ spl21_1 ),
inference(forward_subsumption_resolution,[],[f2804,f208]) ).
fof(f18200,plain,
( ! [X0] :
( ~ subset(singleton(sK17(sK18,sK19)),singleton(X0))
| empty_set = relation_inverse_image(sK18,singleton(sK19)) )
| ~ spl21_1
| ~ spl21_3 ),
inference(superposition,[],[f228,f2832]) ).
fof(f18336,definition,
( spl21_298
<=> ! [X0] : ~ subset(singleton(sK17(sK18,sK19)),singleton(X0)) ),
introduced(definition,[new_symbols(definition,[spl21_298])],[avatar_definition]) ).
fof(f18337,plain,
( ! [X0] : ~ subset(singleton(sK17(sK18,sK19)),singleton(X0))
| ~ spl21_298 ),
inference(avatar_component_clause,[],[f18336]) ).
fof(f18338,plain,
( spl21_10
| spl21_298
| ~ spl21_1
| ~ spl21_3 ),
inference(avatar_split_clause,[],[f18200,f227,f219,f18336,f391]) ).
fof(f19953,definition,
( spl21_309
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[spl21_309])],[avatar_definition]) ).
fof(f19955,plain,
( empty(empty_set)
| ~ spl21_309 ),
inference(avatar_component_clause,[],[f19953]) ).
fof(f20011,plain,
spl21_309,
inference(avatar_split_clause,[],[f102,f19953]) ).
fof(f20045,plain,
( ! [X0] : in(X0,relation_rng(empty_set))
| ~ spl21_309 ),
inference(resolution,[],[f19955,f663]) ).
fof(f20071,plain,
( ! [X0] : in(X0,empty_set)
| ~ spl21_309 ),
inference(forward_demodulation,[],[f20045,f479]) ).
fof(f20094,plain,
( spl21_4
| ~ spl21_309 ),
inference(avatar_split_clause,[],[f20071,f19953,f300]) ).
fof(f20177,definition,
( spl21_324
<=> sK16(sK18) = apply(sK18,sK3(sK18,sK16(sK18))) ),
introduced(definition,[new_symbols(definition,[spl21_324])],[avatar_definition]) ).
fof(f20179,plain,
( sK16(sK18) = apply(sK18,sK3(sK18,sK16(sK18)))
| ~ spl21_324 ),
inference(avatar_component_clause,[],[f20177]) ).
fof(f25379,plain,
( $false
| ~ spl21_298 ),
inference(resolution,[],[f18337,f133]) ).
fof(f25382,plain,
~ spl21_298,
inference(avatar_contradiction_clause,[],[f25379]) ).
fof(f25387,plain,
( ! [X0] : ~ subset(empty_set,singleton(X0))
| ~ spl21_3
| ~ spl21_10 ),
inference(superposition,[],[f228,f393]) ).
fof(f25496,plain,
( $false
| ~ spl21_3
| ~ spl21_10 ),
inference(forward_subsumption_resolution,[],[f25387,f146]) ).
fof(f25497,plain,
( ~ spl21_3
| ~ spl21_10 ),
inference(avatar_contradiction_clause,[],[f25496]) ).
fof(f25544,plain,
( sK16(sK18) = apply(sK18,sK3(sK18,sK16(sK18)))
| function(sK18)
| relation(sK18)
| spl21_1 ),
inference(resolution,[],[f220,f403]) ).
fof(f25546,plain,
( sK16(sK18) = apply(sK18,sK3(sK18,sK16(sK18)))
| relation(sK18)
| spl21_1 ),
inference(forward_subsumption_resolution,[],[f25544,f209]) ).
fof(f25547,plain,
( sK16(sK18) = apply(sK18,sK3(sK18,sK16(sK18)))
| spl21_1 ),
inference(forward_subsumption_resolution,[],[f25546,f208]) ).
fof(f25548,plain,
( spl21_324
| spl21_1 ),
inference(avatar_split_clause,[],[f25547,f219,f20177]) ).
fof(f25733,plain,
( ! [X0] :
( singleton(X0) != singleton(sK20(sK16(sK18)))
| relation(sK18)
| one_to_one(sK18)
| function(sK18)
| empty_set = relation_inverse_image(sK18,singleton(sK16(sK18))) )
| ~ spl21_2 ),
inference(superposition,[],[f207,f316]) ).
fof(f237400,plain,
( ~ in(sK3(sK18,sK16(sK18)),relation_inverse_image(sK18,singleton(sK16(sK18))))
| function(sK18)
| in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| relation(sK18)
| ~ spl21_324 ),
inference(superposition,[],[f407,f20179]) ).
fof(f237671,plain,
( ~ in(sK3(sK18,sK16(sK18)),relation_inverse_image(sK18,singleton(sK16(sK18))))
| in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| relation(sK18)
| ~ spl21_324 ),
inference(forward_subsumption_resolution,[],[f237400,f209]) ).
fof(f237683,definition,
( spl21_4388
<=> in(sK3(sK18,sK16(sK18)),relation_dom(sK18)) ),
introduced(definition,[new_symbols(definition,[spl21_4388])],[avatar_definition]) ).
fof(f237685,plain,
( in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| ~ spl21_4388 ),
inference(avatar_component_clause,[],[f237683]) ).
fof(f237826,plain,
( ~ in(sK3(sK18,sK16(sK18)),relation_inverse_image(sK18,singleton(sK16(sK18))))
| in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| ~ spl21_324 ),
inference(forward_subsumption_resolution,[],[f237671,f208]) ).
fof(f237997,plain,
( ~ in(sK3(sK18,sK16(sK18)),empty_set)
| in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| ~ spl21_8
| ~ spl21_324 ),
inference(forward_demodulation,[],[f237826,f380]) ).
fof(f238008,definition,
( spl21_4426
<=> in(sK16(sK18),relation_rng(sK18)) ),
introduced(definition,[new_symbols(definition,[spl21_4426])],[avatar_definition]) ).
fof(f238009,plain,
( in(sK16(sK18),relation_rng(sK18))
| ~ spl21_4426 ),
inference(avatar_component_clause,[],[f238008]) ).
fof(f238010,plain,
( ~ in(sK16(sK18),relation_rng(sK18))
| spl21_4426 ),
inference(avatar_component_clause,[],[f238008]) ).
fof(f238074,plain,
( in(sK3(sK18,sK16(sK18)),relation_dom(sK18))
| ~ spl21_4
| ~ spl21_8
| ~ spl21_324 ),
inference(forward_subsumption_resolution,[],[f237997,f301]) ).
fof(f238081,plain,
( spl21_4388
| ~ spl21_4
| ~ spl21_8
| ~ spl21_324 ),
inference(avatar_split_clause,[],[f238074,f20177,f378,f300,f237683]) ).
fof(f238082,plain,
( relation(sK18)
| one_to_one(sK18)
| function(sK18)
| ~ spl21_4426 ),
inference(resolution,[],[f238009,f206]) ).
fof(f238086,plain,
( one_to_one(sK18)
| function(sK18)
| ~ spl21_4426 ),
inference(forward_subsumption_resolution,[],[f238082,f208]) ).
fof(f238087,plain,
( function(sK18)
| spl21_1
| ~ spl21_4426 ),
inference(forward_subsumption_resolution,[],[f238086,f220]) ).
fof(f238088,plain,
( $false
| spl21_1
| ~ spl21_4426 ),
inference(forward_subsumption_resolution,[],[f238087,f209]) ).
fof(f238089,plain,
( spl21_1
| ~ spl21_4426 ),
inference(avatar_contradiction_clause,[],[f238088]) ).
fof(f238992,plain,
( relation(sK18)
| function(sK18)
| in(sK16(sK18),relation_rng(sK18))
| ~ spl21_4388 ),
inference(resolution,[],[f237685,f185]) ).
fof(f239013,plain,
( function(sK18)
| in(sK16(sK18),relation_rng(sK18))
| ~ spl21_4388 ),
inference(forward_subsumption_resolution,[],[f238992,f208]) ).
fof(f239020,plain,
( in(sK16(sK18),relation_rng(sK18))
| ~ spl21_4388 ),
inference(forward_subsumption_resolution,[],[f239013,f209]) ).
fof(f239023,plain,
( $false
| ~ spl21_4388
| spl21_4426 ),
inference(forward_subsumption_resolution,[],[f239020,f238010]) ).
fof(f239024,plain,
( ~ spl21_4388
| spl21_4426 ),
inference(avatar_contradiction_clause,[],[f239023]) ).
fof(f239028,plain,
( ! [X0] :
( singleton(X0) != singleton(sK20(sK16(sK18)))
| one_to_one(sK18)
| function(sK18)
| empty_set = relation_inverse_image(sK18,singleton(sK16(sK18))) )
| ~ spl21_2 ),
inference(forward_subsumption_resolution,[],[f25733,f208]) ).
fof(f239117,plain,
( ! [X0] :
( singleton(X0) != singleton(sK20(sK16(sK18)))
| function(sK18)
| empty_set = relation_inverse_image(sK18,singleton(sK16(sK18))) )
| spl21_1
| ~ spl21_2 ),
inference(forward_subsumption_resolution,[],[f239028,f220]) ).
fof(f239118,plain,
( ! [X0] :
( singleton(X0) != singleton(sK20(sK16(sK18)))
| empty_set = relation_inverse_image(sK18,singleton(sK16(sK18))) )
| spl21_1
| ~ spl21_2 ),
inference(forward_subsumption_resolution,[],[f239117,f209]) ).
fof(f239119,plain,
( spl21_8
| spl21_9
| spl21_1
| ~ spl21_2 ),
inference(avatar_split_clause,[],[f239118,f223,f219,f382,f378]) ).
fof(f239121,plain,
( $false
| ~ spl21_9 ),
inference(equality_resolution,[],[f383]) ).
fof(f239122,plain,
~ spl21_9,
inference(avatar_contradiction_clause,[],[f239121]) ).
cnf(s1,plain,
( spl21_1
| spl21_2 ),
inference(sat_conversion,[],[f225]) ).
cnf(s2,plain,
( ~ spl21_1
| spl21_3 ),
inference(sat_conversion,[],[f229]) ).
cnf(s464,plain,
( ~ spl21_1
| ~ spl21_3
| spl21_10
| spl21_298 ),
inference(sat_conversion,[],[f18338]) ).
cnf(s504,plain,
spl21_309,
inference(sat_conversion,[],[f20011]) ).
cnf(s507,plain,
( spl21_4
| ~ spl21_309 ),
inference(sat_conversion,[],[f20094]) ).
cnf(s720,plain,
~ spl21_298,
inference(sat_conversion,[],[f25382]) ).
cnf(s722,plain,
( ~ spl21_3
| ~ spl21_10 ),
inference(sat_conversion,[],[f25497]) ).
cnf(s726,plain,
( spl21_1
| spl21_324 ),
inference(sat_conversion,[],[f25548]) ).
cnf(s7695,plain,
( ~ spl21_4
| ~ spl21_8
| ~ spl21_324
| spl21_4388 ),
inference(sat_conversion,[],[f238081]) ).
cnf(s7696,plain,
( spl21_1
| ~ spl21_4426 ),
inference(sat_conversion,[],[f238089]) ).
cnf(s7705,plain,
( ~ spl21_4388
| spl21_4426 ),
inference(sat_conversion,[],[f239024]) ).
cnf(s7729,plain,
( spl21_1
| ~ spl21_2
| spl21_8
| spl21_9 ),
inference(sat_conversion,[],[f239119]) ).
cnf(s7730,plain,
~ spl21_9,
inference(sat_conversion,[],[f239122]) ).
cnf(s7731,plain,
( spl21_1
| ~ spl21_2
| spl21_8 ),
inference(rat,[],[s7729,s7730]) ).
cnf(s7766,plain,
spl21_4,
inference(rat,[],[s507,s504]) ).
cnf(s7787,plain,
( ~ spl21_1
| ~ spl21_3
| spl21_10 ),
inference(rat,[],[s464,s720]) ).
cnf(s7803,plain,
spl21_1,
inference(rat,[],[s7695,s7731,s7705,s1,s726,s7696,s7766]) ).
cnf(s7805,plain,
spl21_3,
inference(rat,[],[s2,s7803]) ).
cnf(s7806,plain,
~ spl21_10,
inference(rat,[],[s722,s7805]) ).
cnf(s7807,plain,
$false,
inference(rat,[],[s7787,s7803,s7806,s7805]) ).
fof(f239123,plain,
$false,
inference(avatar_sat_refutation,[],[s7807]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU078+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 03:36:47 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.47/2.67 % (3234820)Will run a generic schedule for satisfiability detection.
% 15.47/2.67 % (3234829)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3925756936:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.47/2.67 % (3234825)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=733330789_2999 on theBenchmark for (2999ds/0Mi)
% 15.47/2.67 % (3234827)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1938916647:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.47/2.67 % (3234828)dis+10_1_sil=32000:sp=arity:random_seed=1422957426:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.47/2.67 % (3234830)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2898867129:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.47/2.67 % (3234831)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4264604993:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.47/2.67 % (3234826)% WARNING: option uhcvi not known.
% 15.47/2.67 % TRYING [1]
% 15.47/2.67 % TRYING [2]
% 15.47/2.67 % TRYING [3]
% 15.47/2.67 % (3234826)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1619844410:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.47/2.67 % TRYING [4]
% 15.47/2.67 % TRYING [5]
% 15.47/2.67 % (3234829)Instruction limit reached!
% 15.47/2.67 % (3234829)------------------------------
% 15.47/2.67 % (3234829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.67 % (3234829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.67 % (3234829)CaDiCaL version: 2.1.3
% 15.47/2.67 % (3234829)Termination reason: Instruction limit
% 15.47/2.67 % (3234829)Termination phase: Saturation
% 15.47/2.67 % (3234829)Time elapsed: 0.040 s
% 15.47/2.67 % (3234829)Peak memory usage: 13 MB
% 15.47/2.67 % (3234829)Instructions burned: 119 (million)
% 15.47/2.67 % (3234840)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1321979849:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.47/2.67 % TRYING [1]
% 15.47/2.67 % TRYING [2]
% 15.47/2.67 % TRYING [3]
% 15.47/2.67 % TRYING [4]
% 15.47/2.67 % TRYING [6]
% 15.47/2.67 % TRYING [5]
% 15.47/2.67 % (3234828)Instruction limit reached!
% 15.47/2.67 % (3234828)------------------------------
% 15.47/2.67 % (3234828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.67 % (3234828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.67 % (3234828)CaDiCaL version: 2.1.3
% 15.47/2.67 % (3234828)Termination reason: Instruction limit
% 15.47/2.67 % (3234828)Termination phase: Saturation
% 15.47/2.67 % (3234828)Time elapsed: 0.064 s
% 15.47/2.67 % (3234828)Peak memory usage: 12 MB
% 15.47/2.67 % (3234828)Instructions burned: 104 (million)
% 15.47/2.67 % TRYING [6]
% 15.47/2.67 % (3234830)Instruction limit reached!
% 15.47/2.67 % (3234830)------------------------------
% 15.47/2.67 % (3234830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.67 % (3234830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.67 % (3234830)CaDiCaL version: 2.1.3
% 15.47/2.67 % (3234830)Termination reason: Instruction limit
% 15.47/2.67 % (3234830)Termination phase: Saturation
% 15.47/2.67 % (3234830)Time elapsed: 0.081 s
% 15.47/2.67 % (3234830)Peak memory usage: 12 MB
% 15.47/2.67 % (3234830)Instructions burned: 131 (million)
% 15.47/2.67 % (3234842)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1336634943:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.47/2.67 % TRYING [7]
% 15.47/2.67 % (3234843)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=2532560180:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.47/2.67 % (3234831)Instruction limit reached!
% 15.47/2.67 % (3234831)------------------------------
% 15.47/2.67 % (3234831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.67 % (3234831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.67 % (3234831)CaDiCaL version: 2.1.3
% 15.47/2.67 % (3234831)Termination reason: Instruction limit
% 15.47/2.67 % (3234831)Termination phase: Saturation
% 15.47/2.67 % (3234831)Time elapsed: 0.104 s
% 15.47/2.67 % (3234831)Peak memory usage: 14 MB
% 15.47/2.67 % (3234831)Instructions burned: 160 (million)
% 15.47/2.67 % TRYING [7]
% 15.47/2.67 % (3234846)ott-21_1_sil=16000:fs=off:random_seed=2269931166:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.47/2.67 % TRYING [8]
% 15.47/2.67 % (3234842)Instruction limit reached!
% 15.47/2.67 % (3234842)------------------------------
% 15.47/2.67 % (3234842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234842)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234842)Termination reason: Instruction limit
% 44.53/6.81 % (3234842)Termination phase: Saturation
% 44.53/6.81 % (3234842)Time elapsed: 0.087 s
% 44.53/6.81 % (3234842)Peak memory usage: 12 MB
% 44.53/6.81 % (3234842)Instructions burned: 132 (million)
% 44.53/6.81 % (3234848)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=72031544:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.53/6.81 % (3234840)Instruction limit reached!
% 44.53/6.81 % (3234840)------------------------------
% 44.53/6.81 % (3234840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234840)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234840)Termination reason: Instruction limit
% 44.53/6.81 % (3234840)Termination phase: Finite model building constraint generation
% 44.53/6.81 % (3234840)Time elapsed: 0.151 s
% 44.53/6.81 % (3234840)Peak memory usage: 26 MB
% 44.53/6.81 % (3234840)Instructions burned: 717 (million)
% 44.53/6.81 % TRYING [8]
% 44.53/6.81 % (3234850)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=312913088:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.53/6.81 % (3234846)Instruction limit reached!
% 44.53/6.81 % (3234846)------------------------------
% 44.53/6.81 % (3234846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234846)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234846)Termination reason: Instruction limit
% 44.53/6.81 % (3234846)Termination phase: Saturation
% 44.53/6.81 % (3234846)Time elapsed: 0.084 s
% 44.53/6.81 % (3234846)Peak memory usage: 12 MB
% 44.53/6.81 % (3234846)Instructions burned: 180 (million)
% 44.53/6.81 % TRYING [1]
% 44.53/6.81 % TRYING [2]
% 44.53/6.81 % TRYING [3]
% 44.53/6.81 % TRYING [4]
% 44.53/6.81 % (3234852)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3249283296:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 44.53/6.81 % TRYING [5]
% 44.53/6.81 % TRYING [6]
% 44.53/6.81 % (3234850)Instruction limit reached!
% 44.53/6.81 % (3234850)------------------------------
% 44.53/6.81 % (3234850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234850)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234850)Termination reason: Instruction limit
% 44.53/6.81 % (3234850)Termination phase: Finite model building constraint generation
% 44.53/6.81 % (3234850)Time elapsed: 0.176 s
% 44.53/6.81 % (3234850)Peak memory usage: 20 MB
% 44.53/6.81 % (3234850)Instructions burned: 869 (million)
% 44.53/6.81 % (3234854)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=862497012:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 44.53/6.81 % (3234843)Instruction limit reached!
% 44.53/6.81 % (3234843)------------------------------
% 44.53/6.81 % (3234843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234843)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234843)Termination reason: Instruction limit
% 44.53/6.81 % (3234843)Termination phase: Saturation
% 44.53/6.81 % (3234843)Time elapsed: 0.311 s
% 44.53/6.81 % (3234843)Peak memory usage: 16 MB
% 44.53/6.81 % (3234843)Instructions burned: 686 (million)
% 44.53/6.81 % TRYING [14]
% 44.53/6.81 % (3234856)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=2623633686:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 44.53/6.81 % TRYING [9]
% 44.53/6.81 % (3234848)Instruction limit reached!
% 44.53/6.81 % (3234848)------------------------------
% 44.53/6.81 % (3234848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.53/6.81 % (3234848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.53/6.81 % (3234848)CaDiCaL version: 2.1.3
% 44.53/6.81 % (3234848)Termination reason: Instruction limit
% 44.53/6.81 % (3234848)Termination phase: Saturation
% 44.53/6.81 % (3234848)Time elapsed: 0.334 s
% 44.53/6.81 % (3234848)Peak memory usage: 14 MB
% 44.53/6.81 % (3234848)Instructions burned: 478 (million)
% 44.53/6.81 % (3234858)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1675668269:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 89.48/13.08 % (3234854)Instruction limit reached!
% 89.48/13.08 % (3234854)------------------------------
% 89.48/13.08 % (3234854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234854)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234854)Termination reason: Instruction limit
% 89.48/13.08 % (3234854)Termination phase: Finite model building constraint generation
% 89.48/13.08 % (3234854)Time elapsed: 0.170 s
% 89.48/13.08 % (3234854)Peak memory usage: 72 MB
% 89.48/13.08 % (3234854)Instructions burned: 890 (million)
% 89.48/13.08 % (3234860)fmb+10_1_sil=64000:random_seed=780345251:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 89.48/13.08 % TRYING [1]
% 89.48/13.08 % TRYING [2]
% 89.48/13.08 % TRYING [3]
% 89.48/13.08 % TRYING [4]
% 89.48/13.08 % TRYING [5]
% 89.48/13.08 % TRYING [6]
% 89.48/13.08 % TRYING [7]
% 89.48/13.08 % TRYING [8]
% 89.48/13.08 % (3234856)Instruction limit reached!
% 89.48/13.08 % (3234856)------------------------------
% 89.48/13.08 % (3234856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234856)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234856)Termination reason: Instruction limit
% 89.48/13.08 % (3234856)Termination phase: Saturation
% 89.48/13.08 % (3234856)Time elapsed: 0.412 s
% 89.48/13.08 % (3234856)Peak memory usage: 19 MB
% 89.48/13.08 % (3234856)Instructions burned: 693 (million)
% 89.48/13.08 % (3234862)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=719039402:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 89.48/13.08 % TRYING [20]
% 89.48/13.08 % (3234852)Instruction limit reached!
% 89.48/13.08 % (3234852)------------------------------
% 89.48/13.08 % (3234852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234852)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234852)Termination reason: Instruction limit
% 89.48/13.08 % (3234852)Termination phase: Saturation
% 89.48/13.08 % (3234852)Time elapsed: 0.693 s
% 89.48/13.08 % (3234852)Peak memory usage: 21 MB
% 89.48/13.08 % (3234852)Instructions burned: 1180 (million)
% 89.48/13.08 % (3234864)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1073081373:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 89.48/13.08 % TRYING [8]
% 89.48/13.08 % TRYING [9]
% 89.48/13.08 % (3234858)Instruction limit reached!
% 89.48/13.08 % (3234858)------------------------------
% 89.48/13.08 % (3234858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234858)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234858)Termination reason: Instruction limit
% 89.48/13.08 % (3234858)Termination phase: Saturation
% 89.48/13.08 % (3234858)Time elapsed: 0.510 s
% 89.48/13.08 % (3234858)Peak memory usage: 19 MB
% 89.48/13.08 % (3234858)Instructions burned: 880 (million)
% 89.48/13.08 % (3234866)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1795628737:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 89.48/13.08 % TRYING [9]
% 89.48/13.08 % (3234864)Instruction limit reached!
% 89.48/13.08 % (3234864)------------------------------
% 89.48/13.08 % (3234864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234864)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234864)Termination reason: Instruction limit
% 89.48/13.08 % (3234864)Termination phase: Finite model building constraint generation
% 89.48/13.08 % (3234864)Time elapsed: 0.386 s
% 89.48/13.08 % (3234864)Peak memory usage: 41 MB
% 89.48/13.08 % (3234864)Instructions burned: 920 (million)
% 89.48/13.08 % (3234868)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1004283047:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 89.48/13.08 % TRYING [10]
% 89.48/13.08 % TRYING [10]
% 89.48/13.08 % (3234868)Instruction limit reached!
% 89.48/13.08 % (3234868)------------------------------
% 89.48/13.08 % (3234868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.48/13.08 % (3234868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.48/13.08 % (3234868)CaDiCaL version: 2.1.3
% 89.48/13.08 % (3234868)Termination reason: Instruction limit
% 89.48/13.08 % (3234868)Termination phase: Saturation
% 89.48/13.08 % (3234868)Time elapsed: 0.867 s
% 89.48/13.08 % (3234868)Peak memory usage: 34 MB
% 89.48/13.08 % (3234868)Instructions burned: 1472 (million)
% 49.22/14.84 % (3234870)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4166648148:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 49.22/14.84 % TRYING [77]
% 49.22/14.84 % TRYING [11]
% 49.22/14.84 % (3234866)Instruction limit reached!
% 49.22/14.84 % (3234866)------------------------------
% 49.22/14.84 % (3234866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234866)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234866)Termination reason: Instruction limit
% 49.22/14.84 % (3234866)Termination phase: Saturation
% 49.22/14.84 % (3234866)Time elapsed: 2.768 s
% 49.22/14.84 % (3234866)Peak memory usage: 33 MB
% 49.22/14.84 % (3234866)Instructions burned: 5131 (million)
% 49.22/14.84 % (3234872)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2858727639:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 49.22/14.84 % TRYING [16]
% 49.22/14.84 % (3234870)Instruction limit reached!
% 49.22/14.84 % (3234870)------------------------------
% 49.22/14.84 % (3234870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234870)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234870)Termination reason: Instruction limit
% 49.22/14.84 % (3234870)Termination phase: Finite model building constraint generation
% 49.22/14.84 % (3234870)Time elapsed: 2.325 s
% 49.22/14.84 % (3234870)Peak memory usage: 516 MB
% 49.22/14.84 % (3234870)Instructions burned: 6325 (million)
% 49.22/14.84 % (3234872)Instruction limit reached!
% 49.22/14.84 % (3234872)------------------------------
% 49.22/14.84 % (3234872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234872)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234872)Termination reason: Instruction limit
% 49.22/14.84 % (3234872)Termination phase: Finite model building constraint generation
% 49.22/14.84 % (3234872)Time elapsed: 0.743 s
% 49.22/14.84 % (3234872)Peak memory usage: 138 MB
% 49.22/14.84 % (3234872)Instructions burned: 2175 (million)
% 49.22/14.84 % (3234874)ott-2_1_sil=16000:newcnf=on:random_seed=2674246904:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 49.22/14.84 % (3234875)ott+10_1_sil=32000:tgt=ground:random_seed=3773425968:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 49.22/14.84 % (3234874)Instruction limit reached!
% 49.22/14.84 % (3234874)------------------------------
% 49.22/14.84 % (3234874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234874)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234874)Termination reason: Instruction limit
% 49.22/14.84 % (3234874)Termination phase: Saturation
% 49.22/14.84 % (3234874)Time elapsed: 0.498 s
% 49.22/14.84 % (3234874)Peak memory usage: 20 MB
% 49.22/14.84 % (3234874)Instructions burned: 869 (million)
% 49.22/14.84 % (3234878)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2014976862:i=54282_2948 on theBenchmark for (2948ds/54282Mi)
% 49.22/14.84 % TRYING [1]
% 49.22/14.84 % TRYING [2]
% 49.22/14.84 % TRYING [3]
% 49.22/14.84 % TRYING [4]
% 49.22/14.84 % TRYING [5]
% 49.22/14.84 % TRYING [6]
% 49.22/14.84 % TRYING [7]
% 49.22/14.84 % TRYING [8]
% 49.22/14.84 % (3234862)Instruction limit reached!
% 49.22/14.84 % (3234862)------------------------------
% 49.22/14.84 % (3234862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234862)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234862)Termination reason: Instruction limit
% 49.22/14.84 % (3234862)Termination phase: Finite model building constraint generation
% 49.22/14.84 % (3234862)Time elapsed: 4.674 s
% 49.22/14.84 % (3234862)Peak memory usage: 666 MB
% 49.22/14.84 % (3234862)Instructions burned: 9515 (million)
% 49.22/14.84 % (3234880)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4062970551:i=3512:aac=none_2943 on theBenchmark for (2943ds/3512Mi)
% 49.22/14.84 % TRYING [9]
% 49.22/14.84 % (3234860)Instruction limit reached!
% 49.22/14.84 % (3234860)------------------------------
% 49.22/14.84 % (3234860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.84 % (3234860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.84 % (3234860)CaDiCaL version: 2.1.3
% 49.22/14.84 % (3234860)Termination reason: Instruction limit
% 49.22/14.84 % (3234860)Termination phase: Finite model building SAT solving
% 49.22/14.85 % (3234860)Time elapsed: 5.777 s
% 49.22/14.85 % (3234860)Peak memory usage: 68 MB
% 49.22/14.85 % (3234860)Instructions burned: 22061 (million)
% 49.22/14.85 % (3234882)dis+21_1_sil=32000:sas=cadical:random_seed=3251671609:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi)
% 49.22/14.85 % TRYING [10]
% 49.22/14.85 % (3234875)Instruction limit reached!
% 49.22/14.85 % (3234875)------------------------------
% 49.22/14.85 % (3234875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234875)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234875)Termination reason: Instruction limit
% 49.22/14.85 % (3234875)Termination phase: Saturation
% 49.22/14.85 % (3234875)Time elapsed: 2.764 s
% 49.22/14.85 % (3234875)Peak memory usage: 45 MB
% 49.22/14.85 % (3234875)Instructions burned: 5114 (million)
% 49.22/14.85 % (3234884)ott+11_1_sil=16000:gs=on:random_seed=539170134:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2925 on theBenchmark for (2925ds/2251Mi)
% 49.22/14.85 % (3234882)Instruction limit reached!
% 49.22/14.85 % (3234882)------------------------------
% 49.22/14.85 % (3234882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234882)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234882)Termination reason: Instruction limit
% 49.22/14.85 % (3234882)Termination phase: Saturation
% 49.22/14.85 % (3234882)Time elapsed: 1.105 s
% 49.22/14.85 % (3234882)Peak memory usage: 35 MB
% 49.22/14.85 % (3234882)Instructions burned: 3776 (million)
% 49.22/14.85 % (3234886)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=189579981:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 49.22/14.85 % TRYING [7]
% 49.22/14.85 % (3234880)Instruction limit reached!
% 49.22/14.85 % (3234880)------------------------------
% 49.22/14.85 % (3234880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234880)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234880)Termination reason: Instruction limit
% 49.22/14.85 % (3234880)Termination phase: Saturation
% 49.22/14.85 % (3234880)Time elapsed: 1.973 s
% 49.22/14.85 % (3234880)Peak memory usage: 25 MB
% 49.22/14.85 % (3234880)Instructions burned: 3513 (million)
% 49.22/14.85 % TRYING [8]
% 49.22/14.85 % (3234888)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=574052915:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2923 on theBenchmark for (2923ds/4591Mi)
% 49.22/14.85 % TRYING [9]
% 49.22/14.85 % (3234884)Instruction limit reached!
% 49.22/14.85 % (3234884)------------------------------
% 49.22/14.85 % (3234884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234884)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234884)Termination reason: Instruction limit
% 49.22/14.85 % (3234884)Termination phase: Saturation
% 49.22/14.85 % (3234884)Time elapsed: 1.191 s
% 49.22/14.85 % (3234884)Peak memory usage: 26 MB
% 49.22/14.85 % (3234884)Instructions burned: 2251 (million)
% 49.22/14.85 % (3234890)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=822652269:i=29340_2913 on theBenchmark for (2913ds/29340Mi)
% 49.22/14.85 % TRYING [10]
% 49.22/14.85 % (3234888)Instruction limit reached!
% 49.22/14.85 % (3234888)------------------------------
% 49.22/14.85 % (3234888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234888)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234888)Termination reason: Instruction limit
% 49.22/14.85 % (3234888)Termination phase: Saturation
% 49.22/14.85 % (3234888)Time elapsed: 2.267 s
% 49.22/14.85 % (3234888)Peak memory usage: 43 MB
% 49.22/14.85 % (3234888)Instructions burned: 4593 (million)
% 49.22/14.85 % (3234892)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=391454056:i=5211_2900 on theBenchmark for (2900ds/5211Mi)
% 49.22/14.85 % TRYING [11]
% 49.22/14.85 % (3234892)Instruction limit reached!
% 49.22/14.85 % (3234892)------------------------------
% 49.22/14.85 % (3234892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234892)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234892)Termination reason: Instruction limit
% 49.22/14.85 % (3234892)Termination phase: Saturation
% 49.22/14.85 % (3234892)Time elapsed: 2.685 s
% 49.22/14.85 % (3234892)Peak memory usage: 49 MB
% 49.22/14.85 % (3234892)Instructions burned: 5213 (million)
% 49.22/14.85 % (3234894)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3375425139:i=5497:nm=2_2873 on theBenchmark for (2873ds/5497Mi)
% 49.22/14.85 % TRYING [17]
% 49.22/14.85 % TRYING [11]
% 49.22/14.85 % (3234826) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3234820-3234826"...
% 49.22/14.85 % (3234826)...printing done.
% 49.22/14.85 % (3234826)Refutation found. Thanks to Tanya!
% 49.22/14.85 % SZS status Theorem for theBenchmark
% 49.22/14.85 % SZS output start Proof for theBenchmark
% See solution above
% 49.22/14.85 % (3234826)------------------------------
% 49.22/14.85 % (3234826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.22/14.85 % (3234826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.22/14.85 % (3234826)CaDiCaL version: 2.1.3
% 49.22/14.85 % (3234826)Termination reason: Refutation
% 49.22/14.85 % (3234826)Time elapsed: 14.324 s
% 49.22/14.85 % (3234826)Peak memory usage: 100 MB
% 49.22/14.85 % (3234826)Instructions burned: 24530 (million)
% 49.22/14.85 % (3234820)Success in time 14.433 s
% 49.22/14.85 % Vampire exiting
%------------------------------------------------------------------------------