%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU213+3 : 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 : n013.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:52:24 PM UTC 2026
% Result : Theorem 38.63s 5.95s
% Output : Refutation 38.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 15
% Syntax : Number of formulae : 176 ( 21 unt; 7 def)
% Number of atoms : 642 ( 53 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 681 ( 215 ~; 399 |; 29 &)
% ( 23 <=>; 13 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 292 ( 0 sgn 282 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f5,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f6,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f7,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
fof(f8,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( relation(X1)
=> ! [X2] :
( relation(X2)
=> ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_relat_1) ).
fof(f9,axiom,
! [X0,X1] :
( ( relation(X0)
& relation(X1) )
=> relation(relation_composition(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_relat_1) ).
fof(f13,axiom,
! [X0,X1] :
( ( relation(X0)
& function(X0)
& relation(X1)
& function(X1) )
=> ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_funct_1) ).
fof(f33,conjecture,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_funct_1) ).
fof(f34,negated_conjecture,
~ ! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f33]) ).
fof(f49,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f50,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f52,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = relation_composition(X0,X1)
<=> ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ? [X5] :
( in(ordered_pair(X3,X5),X0)
& in(ordered_pair(X5,X4),X1) ) ) )
| ~ relation(X2) )
| ~ relation(X1) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f53,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f54,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(flattening,[],[f53]) ).
fof(f57,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f13]) ).
fof(f58,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f57]) ).
fof(f66,plain,
? [X0,X1] :
( ? [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<~> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f67,plain,
? [X0,X1] :
( ? [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<~> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f66]) ).
fof(f80,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(X1,relation_dom(X0))
| ~ in(ordered_pair(X1,X2),X0)
| apply(X0,X1) = X2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f82,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(X1,relation_dom(X0))
| in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f85,plain,
! [X2,X3,X0,X1] :
( ~ relation(X0)
| ~ in(ordered_pair(X2,X3),X0)
| in(X2,X1)
| relation_dom(X0) != X1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f86,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| in(ordered_pair(X2,sK1(X0,X2)),X0)
| ~ in(X2,X1)
| relation_dom(X0) != X1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f89,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f7]) ).
fof(f93,plain,
! [X2,X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| in(ordered_pair(sK5(X0,X1,X3,X4),X4),X1)
| ~ in(ordered_pair(X3,X4),X2)
| relation_composition(X0,X1) != X2 ),
inference(cnf_transformation,[],[f52]) ).
fof(f94,plain,
! [X2,X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| in(ordered_pair(X3,sK5(X0,X1,X3,X4)),X0)
| ~ in(ordered_pair(X3,X4),X2)
| relation_composition(X0,X1) != X2 ),
inference(cnf_transformation,[],[f52]) ).
fof(f95,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ in(ordered_pair(X5,X4),X1)
| ~ in(ordered_pair(X3,X5),X0)
| in(ordered_pair(X3,X4),X2)
| relation_composition(X0,X1) != X2 ),
inference(cnf_transformation,[],[f52]) ).
fof(f96,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ relation(X0)
| relation(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f102,plain,
! [X0,X1] :
( ~ function(X1)
| ~ relation(X1)
| ~ function(X0)
| ~ relation(X0)
| function(relation_composition(X0,X1)) ),
inference(cnf_transformation,[],[f58]) ).
fof(f131,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| ~ in(sK16,relation_dom(sK18))
| ~ in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(cnf_transformation,[],[f67]) ).
fof(f132,plain,
( in(apply(sK18,sK16),relation_dom(sK17))
| in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(cnf_transformation,[],[f67]) ).
fof(f133,plain,
( in(sK16,relation_dom(sK18))
| in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(cnf_transformation,[],[f67]) ).
fof(f134,plain,
function(sK18),
inference(cnf_transformation,[],[f67]) ).
fof(f135,plain,
relation(sK18),
inference(cnf_transformation,[],[f67]) ).
fof(f136,plain,
function(sK17),
inference(cnf_transformation,[],[f67]) ).
fof(f137,plain,
relation(sK17),
inference(cnf_transformation,[],[f67]) ).
fof(f145,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(X1,relation_dom(X0))
| in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) != X2 ),
inference(definition_unfolding,[],[f82,f89]) ).
fof(f146,plain,
! [X2,X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(X1,relation_dom(X0))
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) = X2 ),
inference(definition_unfolding,[],[f81,f89]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ relation(X0)
| in(unordered_pair(unordered_pair(X2,sK1(X0,X2)),singleton(X2)),X0)
| ~ in(X2,X1)
| relation_dom(X0) != X1 ),
inference(definition_unfolding,[],[f86,f89]) ).
fof(f150,plain,
! [X2,X3,X0,X1] :
( ~ relation(X0)
| ~ in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),X0)
| in(X2,X1)
| relation_dom(X0) != X1 ),
inference(definition_unfolding,[],[f85,f89]) ).
fof(f151,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| ~ in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),X1)
| ~ in(unordered_pair(unordered_pair(X3,X5),singleton(X3)),X0)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X2)
| relation_composition(X0,X1) != X2 ),
inference(definition_unfolding,[],[f95,f89,f89,f89]) ).
fof(f152,plain,
! [X2,X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| in(unordered_pair(unordered_pair(X3,sK5(X0,X1,X3,X4)),singleton(X3)),X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X2)
| relation_composition(X0,X1) != X2 ),
inference(definition_unfolding,[],[f94,f89,f89]) ).
fof(f153,plain,
! [X2,X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(X2)
| in(unordered_pair(unordered_pair(sK5(X0,X1,X3,X4),X4),singleton(sK5(X0,X1,X3,X4))),X1)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X2)
| relation_composition(X0,X1) != X2 ),
inference(definition_unfolding,[],[f93,f89,f89]) ).
fof(f160,plain,
! [X0,X1] :
( ~ function(X0)
| ~ relation(X0)
| ~ in(X1,relation_dom(X0))
| in(unordered_pair(unordered_pair(X1,apply(X0,X1)),singleton(X1)),X0) ),
inference(equality_resolution,[],[f145]) ).
fof(f161,plain,
! [X2,X0] :
( ~ relation(X0)
| in(unordered_pair(unordered_pair(X2,sK1(X0,X2)),singleton(X2)),X0)
| ~ in(X2,relation_dom(X0)) ),
inference(equality_resolution,[],[f149]) ).
fof(f162,plain,
! [X2,X3,X0] :
( ~ relation(X0)
| ~ in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),X0)
| in(X2,relation_dom(X0)) ),
inference(equality_resolution,[],[f150]) ).
fof(f163,plain,
! [X3,X0,X1,X4,X5] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(relation_composition(X0,X1))
| ~ in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),X1)
| ~ in(unordered_pair(unordered_pair(X3,X5),singleton(X3)),X0)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(equality_resolution,[],[f151]) ).
fof(f164,plain,
! [X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(relation_composition(X0,X1))
| in(unordered_pair(unordered_pair(X3,sK5(X0,X1,X3,X4)),singleton(X3)),X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(equality_resolution,[],[f152]) ).
fof(f165,plain,
! [X3,X0,X1,X4] :
( ~ relation(X0)
| ~ relation(X1)
| ~ relation(relation_composition(X0,X1))
| in(unordered_pair(unordered_pair(sK5(X0,X1,X3,X4),X4),singleton(sK5(X0,X1,X3,X4))),X1)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(equality_resolution,[],[f153]) ).
fof(f171,plain,
! [X0,X1] :
( function(X0)
| relation(X0)
| in(X1,relation_dom(X0))
| ~ in(unordered_pair(unordered_pair(X1,apply(X0,X1)),singleton(X1)),X0) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f172,plain,
! [X2,X0,X1] :
( function(X0)
| relation(X0)
| in(X1,relation_dom(X0))
| in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) = X2 ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f175,plain,
! [X2,X0] :
( relation(X0)
| ~ in(unordered_pair(unordered_pair(X2,sK1(X0,X2)),singleton(X2)),X0)
| in(X2,relation_dom(X0)) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f176,plain,
! [X2,X3,X0] :
( relation(X0)
| in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),X0)
| ~ in(X2,relation_dom(X0)) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f177,plain,
! [X3,X0,X1,X4,X5] :
( relation(X0)
| relation(X1)
| relation(relation_composition(X0,X1))
| in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),X1)
| in(unordered_pair(unordered_pair(X3,X5),singleton(X3)),X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f178,plain,
! [X3,X0,X1,X4] :
( relation(X0)
| relation(X1)
| relation(relation_composition(X0,X1))
| ~ in(unordered_pair(unordered_pair(X3,sK5(X0,X1,X3,X4)),singleton(X3)),X0)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f179,plain,
! [X3,X0,X1,X4] :
( relation(X0)
| relation(X1)
| relation(relation_composition(X0,X1))
| ~ in(unordered_pair(unordered_pair(sK5(X0,X1,X3,X4),X4),singleton(sK5(X0,X1,X3,X4))),X1)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f183,plain,
! [X0,X1] :
( ~ relation(relation_composition(X0,X1))
| relation(X0)
| relation(X1) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f189,plain,
! [X0,X1] :
( ~ function(relation_composition(X0,X1))
| relation(X1)
| function(X0)
| relation(X0)
| function(X1) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f215,plain,
~ relation(sK17),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f216,plain,
~ function(sK17),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f217,plain,
~ relation(sK18),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f218,plain,
~ function(sK18),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f219,plain,
( ~ in(sK16,relation_dom(sK18))
| ~ in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f220,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| ~ in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f221,plain,
( in(apply(sK18,sK16),relation_dom(sK17))
| in(sK16,relation_dom(sK18))
| in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f229,definition,
( spl19_1
<=> in(sK16,relation_dom(relation_composition(sK18,sK17))) ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f230,plain,
( ~ in(sK16,relation_dom(relation_composition(sK18,sK17)))
| spl19_1 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f231,plain,
( in(sK16,relation_dom(relation_composition(sK18,sK17)))
| ~ spl19_1 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl19_2
<=> in(sK16,relation_dom(sK18)) ),
introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition]) ).
fof(f234,plain,
( ~ in(sK16,relation_dom(sK18))
| spl19_2 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f237,definition,
( spl19_3
<=> in(apply(sK18,sK16),relation_dom(sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition]) ).
fof(f238,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| spl19_3 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,plain,
( spl19_1
| spl19_2
| spl19_3 ),
inference(avatar_split_clause,[],[f221,f237,f233,f229]) ).
fof(f241,plain,
( ~ spl19_1
| ~ spl19_3 ),
inference(avatar_split_clause,[],[f220,f237,f229]) ).
fof(f242,plain,
( ~ spl19_1
| ~ spl19_2 ),
inference(avatar_split_clause,[],[f219,f233,f229]) ).
fof(f392,plain,
! [X2,X3,X0] :
( in(unordered_pair(singleton(X2),unordered_pair(X2,X3)),X0)
| relation(X0)
| ~ in(X2,relation_dom(X0)) ),
inference(forward_demodulation,[],[f176,f80]) ).
fof(f394,plain,
! [X2,X0,X1] :
( in(unordered_pair(singleton(X1),unordered_pair(X0,X1)),X2)
| relation(X2)
| ~ in(X1,relation_dom(X2)) ),
inference(superposition,[],[f392,f80]) ).
fof(f396,plain,
! [X2,X0] :
( ~ in(unordered_pair(singleton(X2),unordered_pair(X2,sK1(X0,X2))),X0)
| relation(X0)
| in(X2,relation_dom(X0)) ),
inference(forward_demodulation,[],[f175,f80]) ).
fof(f406,plain,
! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,apply(X0,X1))),X0)
| function(X0)
| relation(X0)
| in(X1,relation_dom(X0)) ),
inference(forward_demodulation,[],[f171,f80]) ).
fof(f422,plain,
! [X2,X0,X1] :
( in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),X0)
| function(X0)
| relation(X0)
| in(X1,relation_dom(X0))
| apply(X0,X1) = X2 ),
inference(forward_demodulation,[],[f172,f80]) ).
fof(f423,plain,
! [X2,X0,X1] :
( in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),X0)
| function(X0)
| relation(X0)
| apply(X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f422,f392]) ).
fof(f424,plain,
! [X0,X1] :
( function(X0)
| relation(X0)
| apply(X0,X1) = sK1(X0,X1)
| relation(X0)
| in(X1,relation_dom(X0)) ),
inference(resolution,[],[f423,f396]) ).
fof(f430,plain,
! [X0,X1] :
( in(X1,relation_dom(X0))
| relation(X0)
| apply(X0,X1) = sK1(X0,X1)
| function(X0) ),
inference(duplicate_literal_removal,[],[f424]) ).
fof(f455,plain,
! [X3,X0,X1,X4] :
( relation(X0)
| relation(X1)
| ~ in(unordered_pair(unordered_pair(X3,sK5(X0,X1,X3,X4)),singleton(X3)),X0)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f178,f183]) ).
fof(f456,plain,
! [X3,X0,X1,X4] :
( ~ in(unordered_pair(singleton(X3),unordered_pair(X3,sK5(X0,X1,X3,X4))),X0)
| relation(X0)
| relation(X1)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_demodulation,[],[f455,f80]) ).
fof(f457,plain,
! [X3,X0,X1,X4] :
( ~ in(unordered_pair(singleton(X3),unordered_pair(X3,sK5(X0,X1,X3,X4))),X0)
| in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),relation_composition(X0,X1))
| relation(X0)
| relation(X1) ),
inference(forward_demodulation,[],[f456,f80]) ).
fof(f458,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),relation_composition(X2,X3))
| relation(X2)
| relation(X3)
| function(X2)
| relation(X2)
| apply(X2,X0) = sK5(X2,X3,X0,X1) ),
inference(resolution,[],[f457,f423]) ).
fof(f459,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),relation_composition(X2,X3))
| relation(X2)
| relation(X3)
| relation(X2)
| ~ in(X0,relation_dom(X2)) ),
inference(resolution,[],[f457,f392]) ).
fof(f467,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),relation_composition(X2,X3))
| relation(X2)
| relation(X3)
| ~ in(X0,relation_dom(X2)) ),
inference(duplicate_literal_removal,[],[f459]) ).
fof(f468,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),relation_composition(X2,X3))
| relation(X2)
| relation(X3)
| function(X2)
| apply(X2,X0) = sK5(X2,X3,X0,X1) ),
inference(duplicate_literal_removal,[],[f458]) ).
fof(f472,plain,
! [X3,X0,X1,X4,X5] :
( relation(X0)
| relation(X1)
| in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),X1)
| in(unordered_pair(unordered_pair(X3,X5),singleton(X3)),X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f177,f183]) ).
fof(f473,plain,
! [X3,X0,X1,X4,X5] :
( in(unordered_pair(singleton(X5),unordered_pair(X5,X4)),X1)
| relation(X0)
| relation(X1)
| in(unordered_pair(unordered_pair(X3,X5),singleton(X3)),X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_demodulation,[],[f472,f80]) ).
fof(f474,plain,
! [X3,X0,X1,X4,X5] :
( in(unordered_pair(singleton(X3),unordered_pair(X3,X5)),X0)
| in(unordered_pair(singleton(X5),unordered_pair(X5,X4)),X1)
| relation(X0)
| relation(X1)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_demodulation,[],[f473,f80]) ).
fof(f475,plain,
! [X3,X0,X1,X4,X5] :
( ~ in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),relation_composition(X0,X1))
| in(unordered_pair(singleton(X3),unordered_pair(X3,X5)),X0)
| in(unordered_pair(singleton(X5),unordered_pair(X5,X4)),X1)
| relation(X0)
| relation(X1) ),
inference(forward_demodulation,[],[f474,f80]) ).
fof(f477,plain,
! [X2,X3,X0,X1,X4] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),X2)
| in(unordered_pair(singleton(X1),unordered_pair(X1,X3)),X4)
| relation(X2)
| relation(X4)
| relation(relation_composition(X2,X4))
| ~ in(X0,relation_dom(relation_composition(X2,X4))) ),
inference(resolution,[],[f475,f392]) ).
fof(f485,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(X0,relation_dom(relation_composition(X2,X4)))
| in(unordered_pair(singleton(X1),unordered_pair(X1,X3)),X4)
| relation(X2)
| relation(X4)
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),X2) ),
inference(forward_subsumption_resolution,[],[f477,f183]) ).
fof(f487,plain,
! [X3,X0,X1,X4] :
( relation(X0)
| relation(X1)
| ~ in(unordered_pair(unordered_pair(sK5(X0,X1,X3,X4),X4),singleton(sK5(X0,X1,X3,X4))),X1)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f179,f183]) ).
fof(f488,plain,
! [X3,X0,X1,X4] :
( ~ in(unordered_pair(singleton(sK5(X0,X1,X3,X4)),unordered_pair(sK5(X0,X1,X3,X4),X4)),X1)
| relation(X0)
| relation(X1)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_demodulation,[],[f487,f80]) ).
fof(f489,plain,
! [X3,X0,X1,X4] :
( ~ in(unordered_pair(singleton(sK5(X0,X1,X3,X4)),unordered_pair(X4,sK5(X0,X1,X3,X4))),X1)
| relation(X0)
| relation(X1)
| in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),relation_composition(X0,X1)) ),
inference(forward_demodulation,[],[f488,f80]) ).
fof(f490,plain,
! [X3,X0,X1,X4] :
( ~ in(unordered_pair(singleton(sK5(X0,X1,X3,X4)),unordered_pair(X4,sK5(X0,X1,X3,X4))),X1)
| in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),relation_composition(X0,X1))
| relation(X0)
| relation(X1) ),
inference(forward_demodulation,[],[f489,f80]) ).
fof(f832,plain,
! [X2,X3,X0,X1] :
( relation(X0)
| ~ in(sK5(X1,X0,X2,X3),relation_dom(X0))
| in(unordered_pair(singleton(X2),unordered_pair(X2,X3)),relation_composition(X1,X0))
| relation(X1)
| relation(X0) ),
inference(resolution,[],[f394,f490]) ).
fof(f839,plain,
! [X2,X3,X0,X1] :
( ~ in(sK5(X1,X0,X2,X3),relation_dom(X0))
| relation(X0)
| in(unordered_pair(singleton(X2),unordered_pair(X2,X3)),relation_composition(X1,X0))
| relation(X1) ),
inference(duplicate_literal_removal,[],[f832]) ).
fof(f897,plain,
( relation(relation_composition(sK18,sK17))
| apply(relation_composition(sK18,sK17),sK16) = sK1(relation_composition(sK18,sK17),sK16)
| function(relation_composition(sK18,sK17))
| spl19_1 ),
inference(resolution,[],[f430,f230]) ).
fof(f901,definition,
( spl19_8
<=> function(relation_composition(sK18,sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f902,plain,
( ~ function(relation_composition(sK18,sK17))
| spl19_8 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f903,plain,
( function(relation_composition(sK18,sK17))
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f905,definition,
( spl19_9
<=> apply(relation_composition(sK18,sK17),sK16) = sK1(relation_composition(sK18,sK17),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
fof(f907,plain,
( apply(relation_composition(sK18,sK17),sK16) = sK1(relation_composition(sK18,sK17),sK16)
| ~ spl19_9 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f909,definition,
( spl19_10
<=> relation(relation_composition(sK18,sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
fof(f910,plain,
( ~ relation(relation_composition(sK18,sK17))
| spl19_10 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f911,plain,
( relation(relation_composition(sK18,sK17))
| ~ spl19_10 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f913,plain,
( relation(sK18)
| apply(sK18,sK16) = sK1(sK18,sK16)
| function(sK18)
| spl19_2 ),
inference(resolution,[],[f234,f430]) ).
fof(f916,plain,
( apply(sK18,sK16) = sK1(sK18,sK16)
| function(sK18)
| spl19_2 ),
inference(forward_subsumption_resolution,[],[f913,f217]) ).
fof(f917,plain,
( apply(sK18,sK16) = sK1(sK18,sK16)
| spl19_2 ),
inference(forward_subsumption_resolution,[],[f916,f218]) ).
fof(f945,plain,
( relation(sK17)
| function(sK18)
| relation(sK18)
| function(sK17)
| ~ spl19_8 ),
inference(resolution,[],[f903,f189]) ).
fof(f947,plain,
( function(sK18)
| relation(sK18)
| function(sK17)
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f945,f215]) ).
fof(f948,plain,
( relation(sK18)
| function(sK17)
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f947,f218]) ).
fof(f949,plain,
( function(sK17)
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f948,f217]) ).
fof(f950,plain,
( $false
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f949,f216]) ).
fof(f951,plain,
~ spl19_8,
inference(avatar_contradiction_clause,[],[f950]) ).
fof(f963,plain,
! [X2,X0,X1] :
( relation(X0)
| relation(X1)
| ~ in(X2,relation_dom(X0))
| relation(relation_composition(X0,X1))
| in(X2,relation_dom(relation_composition(X0,X1))) ),
inference(resolution,[],[f467,f396]) ).
fof(f982,plain,
! [X2,X0,X1] :
( in(X2,relation_dom(relation_composition(X0,X1)))
| relation(X1)
| ~ in(X2,relation_dom(X0))
| relation(X0) ),
inference(forward_subsumption_resolution,[],[f963,f183]) ).
fof(f985,plain,
( relation(sK18)
| relation(sK17)
| ~ spl19_10 ),
inference(resolution,[],[f911,f183]) ).
fof(f987,plain,
( relation(sK17)
| ~ spl19_10 ),
inference(forward_subsumption_resolution,[],[f985,f217]) ).
fof(f988,plain,
( $false
| ~ spl19_10 ),
inference(forward_subsumption_resolution,[],[f987,f215]) ).
fof(f989,plain,
~ spl19_10,
inference(avatar_contradiction_clause,[],[f988]) ).
fof(f1234,plain,
! [X2,X0,X1] :
( relation(X0)
| relation(X1)
| function(X0)
| apply(X0,X2) = sK5(X0,X1,X2,apply(relation_composition(X0,X1),X2))
| function(relation_composition(X0,X1))
| relation(relation_composition(X0,X1))
| in(X2,relation_dom(relation_composition(X0,X1))) ),
inference(resolution,[],[f468,f406]) ).
fof(f1257,plain,
! [X2,X0,X1] :
( in(X2,relation_dom(relation_composition(X0,X1)))
| relation(X1)
| function(X0)
| apply(X0,X2) = sK5(X0,X1,X2,apply(relation_composition(X0,X1),X2))
| function(relation_composition(X0,X1))
| relation(X0) ),
inference(forward_subsumption_resolution,[],[f1234,f183]) ).
fof(f1324,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| relation(sK18)
| relation(sK17)
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,X0)),sK18) )
| ~ spl19_1 ),
inference(resolution,[],[f485,f231]) ).
fof(f1336,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| relation(sK17)
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,X0)),sK18) )
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f1324,f217]) ).
fof(f1339,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK17)
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,X0)),sK18) )
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f1336,f215]) ).
fof(f2449,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK16),unordered_pair(sK16,X0)),sK18)
| relation(sK17)
| in(X0,relation_dom(sK17)) )
| ~ spl19_1 ),
inference(resolution,[],[f1339,f396]) ).
fof(f2474,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK16),unordered_pair(sK16,X0)),sK18)
| in(X0,relation_dom(sK17)) )
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f2449,f215]) ).
fof(f80455,plain,
( in(sK1(sK18,sK16),relation_dom(sK17))
| relation(sK18)
| in(sK16,relation_dom(sK18))
| ~ spl19_1 ),
inference(resolution,[],[f2474,f396]) ).
fof(f80463,plain,
( in(sK1(sK18,sK16),relation_dom(sK17))
| in(sK16,relation_dom(sK18))
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f80455,f217]) ).
fof(f80467,plain,
( in(sK1(sK18,sK16),relation_dom(sK17))
| ~ spl19_1
| spl19_2 ),
inference(forward_subsumption_resolution,[],[f80463,f234]) ).
fof(f80469,plain,
( in(apply(sK18,sK16),relation_dom(sK17))
| ~ spl19_1
| spl19_2 ),
inference(forward_demodulation,[],[f80467,f917]) ).
fof(f80472,plain,
( $false
| ~ spl19_1
| spl19_2
| spl19_3 ),
inference(forward_subsumption_resolution,[],[f80469,f238]) ).
fof(f80473,plain,
( ~ spl19_1
| spl19_2
| spl19_3 ),
inference(avatar_contradiction_clause,[],[f80472]) ).
fof(f80474,plain,
( apply(relation_composition(sK18,sK17),sK16) = sK1(relation_composition(sK18,sK17),sK16)
| function(relation_composition(sK18,sK17))
| spl19_1
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f897,f910]) ).
fof(f80491,plain,
( apply(relation_composition(sK18,sK17),sK16) = sK1(relation_composition(sK18,sK17),sK16)
| spl19_1
| spl19_8
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f80474,f902]) ).
fof(f80542,plain,
( relation(sK17)
| function(sK18)
| apply(sK18,sK16) = sK5(sK18,sK17,sK16,apply(relation_composition(sK18,sK17),sK16))
| function(relation_composition(sK18,sK17))
| relation(sK18)
| spl19_1 ),
inference(resolution,[],[f230,f1257]) ).
fof(f80544,plain,
( relation(sK17)
| ~ in(sK16,relation_dom(sK18))
| relation(sK18)
| spl19_1 ),
inference(resolution,[],[f230,f982]) ).
fof(f80552,plain,
( function(sK18)
| apply(sK18,sK16) = sK5(sK18,sK17,sK16,apply(relation_composition(sK18,sK17),sK16))
| function(relation_composition(sK18,sK17))
| relation(sK18)
| spl19_1 ),
inference(forward_subsumption_resolution,[],[f80542,f215]) ).
fof(f80555,plain,
( apply(sK18,sK16) = sK5(sK18,sK17,sK16,apply(relation_composition(sK18,sK17),sK16))
| function(relation_composition(sK18,sK17))
| relation(sK18)
| spl19_1 ),
inference(forward_subsumption_resolution,[],[f80552,f218]) ).
fof(f80558,plain,
( apply(sK18,sK16) = sK5(sK18,sK17,sK16,apply(relation_composition(sK18,sK17),sK16))
| relation(sK18)
| spl19_1
| spl19_8 ),
inference(forward_subsumption_resolution,[],[f80555,f902]) ).
fof(f80559,plain,
( apply(sK18,sK16) = sK5(sK18,sK17,sK16,apply(relation_composition(sK18,sK17),sK16))
| spl19_1
| spl19_8 ),
inference(forward_subsumption_resolution,[],[f80558,f217]) ).
fof(f81003,plain,
( spl19_9
| spl19_1
| spl19_8
| spl19_10 ),
inference(avatar_split_clause,[],[f80491,f909,f901,f229,f905]) ).
fof(f81011,plain,
( ~ in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| relation(relation_composition(sK18,sK17))
| in(sK16,relation_dom(relation_composition(sK18,sK17)))
| ~ spl19_9 ),
inference(superposition,[],[f396,f907]) ).
fof(f81024,plain,
( ~ in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| in(sK16,relation_dom(relation_composition(sK18,sK17)))
| ~ spl19_9
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f81011,f910]) ).
fof(f81031,plain,
( ~ in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| spl19_1
| ~ spl19_9
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f81024,f230]) ).
fof(f82276,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| relation(sK17)
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| relation(sK18)
| spl19_1
| spl19_8 ),
inference(superposition,[],[f839,f80559]) ).
fof(f82308,definition,
( spl19_925
<=> in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_925])],[avatar_definition]) ).
fof(f82719,plain,
( ~ spl19_925
| spl19_1
| ~ spl19_9
| spl19_10 ),
inference(avatar_split_clause,[],[f81031,f909,f905,f229,f82308]) ).
fof(f82735,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| relation(sK18)
| spl19_1
| spl19_8 ),
inference(forward_subsumption_resolution,[],[f82276,f215]) ).
fof(f82745,plain,
( ~ in(sK16,relation_dom(sK18))
| relation(sK18)
| spl19_1 ),
inference(forward_subsumption_resolution,[],[f80544,f215]) ).
fof(f82752,plain,
( ~ in(apply(sK18,sK16),relation_dom(sK17))
| in(unordered_pair(singleton(sK16),unordered_pair(sK16,apply(relation_composition(sK18,sK17),sK16))),relation_composition(sK18,sK17))
| spl19_1
| spl19_8 ),
inference(forward_subsumption_resolution,[],[f82735,f217]) ).
fof(f82758,plain,
( ~ in(sK16,relation_dom(sK18))
| spl19_1 ),
inference(forward_subsumption_resolution,[],[f82745,f217]) ).
fof(f82761,plain,
( spl19_925
| ~ spl19_3
| spl19_1
| spl19_8 ),
inference(avatar_split_clause,[],[f82752,f901,f229,f237,f82308]) ).
fof(f82762,plain,
( ~ spl19_2
| spl19_1 ),
inference(avatar_split_clause,[],[f82758,f229,f233]) ).
cnf(s1,plain,
( spl19_1
| spl19_2
| spl19_3 ),
inference(sat_conversion,[],[f240]) ).
cnf(s2,plain,
( ~ spl19_1
| ~ spl19_3 ),
inference(sat_conversion,[],[f241]) ).
cnf(s3,plain,
( ~ spl19_1
| ~ spl19_2 ),
inference(sat_conversion,[],[f242]) ).
cnf(s12,plain,
~ spl19_8,
inference(sat_conversion,[],[f951]) ).
cnf(s13,plain,
~ spl19_10,
inference(sat_conversion,[],[f989]) ).
cnf(s1030,plain,
( ~ spl19_1
| spl19_2
| spl19_3 ),
inference(sat_conversion,[],[f80473]) ).
cnf(s1113,plain,
( spl19_1
| spl19_8
| spl19_9
| spl19_10 ),
inference(sat_conversion,[],[f81003]) ).
cnf(s1251,plain,
( spl19_1
| ~ spl19_9
| spl19_10
| ~ spl19_925 ),
inference(sat_conversion,[],[f82719]) ).
cnf(s1259,plain,
( spl19_1
| ~ spl19_3
| spl19_8
| spl19_925 ),
inference(sat_conversion,[],[f82761]) ).
cnf(s1260,plain,
( spl19_1
| ~ spl19_2 ),
inference(sat_conversion,[],[f82762]) ).
cnf(s1363,plain,
spl19_1,
inference(rat,[],[s1259,s1251,s1,s1113,s1260,s12,s13]) ).
cnf(s1365,plain,
~ spl19_2,
inference(rat,[],[s3,s1363]) ).
cnf(s1366,plain,
~ spl19_3,
inference(rat,[],[s2,s1363]) ).
cnf(s1368,plain,
$false,
inference(rat,[],[s1030,s1363,s1366,s1365]) ).
fof(f82773,plain,
$false,
inference(avatar_sat_refutation,[],[s1368]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU213+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 04:04:37 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 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
% 13.26/2.37 % (790384)Will run a generic schedule for satisfiability detection.
% 13.26/2.37 % (790393)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4170719132:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.26/2.37 % (790390)% WARNING: option uhcvi not known.
% 13.26/2.37 % (790389)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2492637199_2999 on theBenchmark for (2999ds/0Mi)
% 13.26/2.37 % (790390)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1213047290:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.26/2.37 % (790394)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1757265389:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.37 % (790391)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1120493395:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.26/2.37 % (790392)dis+10_1_sil=32000:sp=arity:random_seed=1982935167:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.26/2.37 % (790395)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1963434283:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.26/2.37 % TRYING [1]
% 13.26/2.37 % TRYING [2]
% 13.26/2.37 % TRYING [3]
% 13.26/2.37 % (790393)Instruction limit reached!
% 13.26/2.37 % (790393)------------------------------
% 13.26/2.37 % (790393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.37 % (790393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.37 % (790393)CaDiCaL version: 2.1.3
% 13.26/2.37 % (790393)Termination reason: Instruction limit
% 13.26/2.37 % (790393)Termination phase: Saturation
% 13.26/2.37 % (790393)Time elapsed: 0.041 s
% 13.26/2.37 % (790393)Peak memory usage: 13 MB
% 13.26/2.37 % (790393)Instructions burned: 118 (million)
% 13.26/2.37 % TRYING [4]
% 13.26/2.37 % (790403)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4157196942:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.26/2.37 % TRYING [1]
% 13.26/2.37 % TRYING [2]
% 13.26/2.37 % TRYING [3]
% 13.26/2.37 % TRYING [4]
% 13.26/2.37 % (790392)Instruction limit reached!
% 13.26/2.37 % (790392)------------------------------
% 13.26/2.37 % (790392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.37 % (790392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.37 % (790392)CaDiCaL version: 2.1.3
% 13.26/2.37 % (790392)Termination reason: Instruction limit
% 13.26/2.37 % (790392)Termination phase: Saturation
% 13.26/2.37 % (790392)Time elapsed: 0.064 s
% 13.26/2.37 % (790392)Peak memory usage: 12 MB
% 13.26/2.37 % (790392)Instructions burned: 103 (million)
% 13.26/2.37 % (790394)Instruction limit reached!
% 13.26/2.37 % (790394)------------------------------
% 13.26/2.37 % (790394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.37 % (790394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.37 % (790394)CaDiCaL version: 2.1.3
% 13.26/2.37 % (790394)Termination reason: Instruction limit
% 13.26/2.37 % (790394)Termination phase: Saturation
% 13.26/2.37 % (790394)Time elapsed: 0.074 s
% 13.26/2.37 % (790394)Peak memory usage: 13 MB
% 13.26/2.37 % (790394)Instructions burned: 133 (million)
% 13.26/2.37 % (790405)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2351930957:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.37 % TRYING [5]
% 13.26/2.37 % (790406)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=54161742:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.26/2.37 % (790395)Instruction limit reached!
% 13.26/2.37 % (790395)------------------------------
% 13.26/2.37 % (790395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.37 % (790395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.37 % (790395)CaDiCaL version: 2.1.3
% 13.26/2.37 % (790395)Termination reason: Instruction limit
% 13.26/2.37 % (790395)Termination phase: Saturation
% 13.26/2.37 % (790395)Time elapsed: 0.095 s
% 13.26/2.37 % (790395)Peak memory usage: 13 MB
% 13.26/2.37 % (790395)Instructions burned: 160 (million)
% 13.26/2.37 % (790409)ott-21_1_sil=16000:fs=off:random_seed=3478370358:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.26/2.37 % TRYING [5]
% 13.26/2.37 % (790405)Instruction limit reached!
% 13.26/2.37 % (790405)------------------------------
% 13.26/2.37 % (790405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.37 % (790405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790405)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790405)Termination reason: Instruction limit
% 38.63/5.90 % (790405)Termination phase: Saturation
% 38.63/5.90 % (790405)Time elapsed: 0.083 s
% 38.63/5.90 % (790405)Peak memory usage: 13 MB
% 38.63/5.90 % (790405)Instructions burned: 131 (million)
% 38.63/5.90 % (790411)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3374524006:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 38.63/5.90 % (790403)Instruction limit reached!
% 38.63/5.90 % (790403)------------------------------
% 38.63/5.90 % (790403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.90 % (790403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790403)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790403)Termination reason: Instruction limit
% 38.63/5.90 % (790403)Termination phase: Finite model building constraint generation
% 38.63/5.90 % (790403)Time elapsed: 0.146 s
% 38.63/5.90 % (790403)Peak memory usage: 35 MB
% 38.63/5.90 % (790403)Instructions burned: 717 (million)
% 38.63/5.90 % (790413)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3156491100:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.63/5.90 % TRYING [1]
% 38.63/5.90 % TRYING [2]
% 38.63/5.90 % TRYING [3]
% 38.63/5.90 % (790409)Instruction limit reached!
% 38.63/5.90 % (790409)------------------------------
% 38.63/5.90 % (790409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.90 % (790409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790409)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790409)Termination reason: Instruction limit
% 38.63/5.90 % (790409)Termination phase: Saturation
% 38.63/5.90 % (790409)Time elapsed: 0.100 s
% 38.63/5.90 % (790409)Peak memory usage: 12 MB
% 38.63/5.90 % (790409)Instructions burned: 181 (million)
% 38.63/5.90 % (790415)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3380921858:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 38.63/5.90 % TRYING [4]
% 38.63/5.90 % TRYING [5]
% 38.63/5.90 % (790413)Instruction limit reached!
% 38.63/5.90 % (790413)------------------------------
% 38.63/5.90 % (790413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.90 % (790413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790413)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790413)Termination reason: Instruction limit
% 38.63/5.90 % (790413)Termination phase: Finite model building constraint generation
% 38.63/5.90 % (790413)Time elapsed: 0.178 s
% 38.63/5.90 % (790413)Peak memory usage: 24 MB
% 38.63/5.90 % (790413)Instructions burned: 865 (million)
% 38.63/5.90 % (790417)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2606594582:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.63/5.90 % (790406)Instruction limit reached!
% 38.63/5.90 % (790406)------------------------------
% 38.63/5.90 % (790406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.90 % (790406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790406)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790406)Termination reason: Instruction limit
% 38.63/5.90 % (790406)Termination phase: Saturation
% 38.63/5.90 % (790406)Time elapsed: 0.341 s
% 38.63/5.90 % (790406)Peak memory usage: 18 MB
% 38.63/5.90 % (790406)Instructions burned: 686 (million)
% 38.63/5.90 % TRYING [6]
% 38.63/5.90 % (790419)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=2737380892: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)
% 38.63/5.90 % (790411)Instruction limit reached!
% 38.63/5.90 % (790411)------------------------------
% 38.63/5.90 % (790411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.90 % (790411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.90 % (790411)CaDiCaL version: 2.1.3
% 38.63/5.90 % (790411)Termination reason: Instruction limit
% 38.63/5.90 % (790411)Termination phase: Saturation
% 38.63/5.90 % (790411)Time elapsed: 0.326 s
% 38.63/5.90 % (790411)Peak memory usage: 14 MB
% 38.63/5.90 % (790411)Instructions burned: 477 (million)
% 38.63/5.90 % (790421)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2340851250:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 38.63/5.90 % (790417)Instruction limit reached!
% 38.63/5.90 % (790417)------------------------------
% 38.63/5.90 % (790417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790417)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790417)Termination reason: Instruction limit
% 38.63/5.95 % (790417)Termination phase: Finite model building constraint generation
% 38.63/5.95 % (790417)Time elapsed: 0.237 s
% 38.63/5.95 % (790417)Peak memory usage: 108 MB
% 38.63/5.95 % (790417)Instructions burned: 892 (million)
% 38.63/5.95 % (790423)fmb+10_1_sil=64000:random_seed=2146692529:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 38.63/5.95 % TRYING [1]
% 38.63/5.95 % TRYING [2]
% 38.63/5.95 % TRYING [3]
% 38.63/5.95 % TRYING [4]
% 38.63/5.95 % TRYING [5]
% 38.63/5.95 % (790419)Instruction limit reached!
% 38.63/5.95 % (790419)------------------------------
% 38.63/5.95 % (790419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790419)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790419)Termination reason: Instruction limit
% 38.63/5.95 % (790419)Termination phase: Saturation
% 38.63/5.95 % (790419)Time elapsed: 0.395 s
% 38.63/5.95 % (790419)Peak memory usage: 19 MB
% 38.63/5.95 % (790419)Instructions burned: 692 (million)
% 38.63/5.95 % (790425)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3520844682:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 38.63/5.95 % (790415)Instruction limit reached!
% 38.63/5.95 % (790415)------------------------------
% 38.63/5.95 % (790415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790415)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790415)Termination reason: Instruction limit
% 38.63/5.95 % (790415)Termination phase: Saturation
% 38.63/5.95 % (790415)Time elapsed: 0.638 s
% 38.63/5.95 % (790415)Peak memory usage: 25 MB
% 38.63/5.95 % (790415)Instructions burned: 1180 (million)
% 38.63/5.95 % TRYING [20]
% 38.63/5.95 % (790427)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1898840383:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 38.63/5.95 % TRYING [8]
% 38.63/5.95 % (790421)Instruction limit reached!
% 38.63/5.95 % (790421)------------------------------
% 38.63/5.95 % (790421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790421)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790421)Termination reason: Instruction limit
% 38.63/5.95 % (790421)Termination phase: Saturation
% 38.63/5.95 % (790421)Time elapsed: 0.492 s
% 38.63/5.95 % (790421)Peak memory usage: 19 MB
% 38.63/5.95 % (790421)Instructions burned: 880 (million)
% 38.63/5.95 % (790429)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3426760680:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 38.63/5.95 % TRYING [6]
% 38.63/5.95 % (790427)Instruction limit reached!
% 38.63/5.95 % (790427)------------------------------
% 38.63/5.95 % (790427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790427)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790427)Termination reason: Instruction limit
% 38.63/5.95 % (790427)Termination phase: Finite model building constraint generation
% 38.63/5.95 % (790427)Time elapsed: 0.307 s
% 38.63/5.95 % (790427)Peak memory usage: 62 MB
% 38.63/5.95 % (790427)Instructions burned: 922 (million)
% 38.63/5.95 % (790431)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=296013806:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 38.63/5.95 % TRYING [7]
% 38.63/5.95 % (790431)Instruction limit reached!
% 38.63/5.95 % (790431)------------------------------
% 38.63/5.95 % (790431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790431)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790431)Termination reason: Instruction limit
% 38.63/5.95 % (790431)Termination phase: Saturation
% 38.63/5.95 % (790431)Time elapsed: 0.651 s
% 38.63/5.95 % (790431)Peak memory usage: 24 MB
% 38.63/5.95 % (790431)Instructions burned: 1474 (million)
% 38.63/5.95 % (790433)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3884757412:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 38.63/5.95 % (790433)Cannot represent all propositional literals internally
% 38.63/5.95 % (790433)Refutation not found, incomplete strategy
% 38.63/5.95 % (790433)------------------------------
% 38.63/5.95 % (790433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790433)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790433)Termination reason: Refutation not found, incomplete strategy
% 38.63/5.95 % (790433)Time elapsed: 0.008 s
% 38.63/5.95 % (790433)Peak memory usage: 11 MB
% 38.63/5.95 % (790433)Instructions burned: 14 (million)
% 38.63/5.95 % (790433)------------------------------
% 38.63/5.95 % (790433)------------------------------
% 38.63/5.95 % (790435)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2428236311:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 38.63/5.95 % TRYING [16]
% 38.63/5.95 % TRYING [7]
% 38.63/5.95 % (790435)Instruction limit reached!
% 38.63/5.95 % (790435)------------------------------
% 38.63/5.95 % (790435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790435)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790435)Termination reason: Instruction limit
% 38.63/5.95 % (790435)Termination phase: Finite model building constraint generation
% 38.63/5.95 % (790435)Time elapsed: 0.740 s
% 38.63/5.95 % (790435)Peak memory usage: 132 MB
% 38.63/5.95 % (790435)Instructions burned: 2176 (million)
% 38.63/5.95 % (790437)ott-2_1_sil=16000:newcnf=on:random_seed=122788979:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 38.63/5.95 % (790437)Instruction limit reached!
% 38.63/5.95 % (790437)------------------------------
% 38.63/5.95 % (790437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790437)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790437)Termination reason: Instruction limit
% 38.63/5.95 % (790437)Termination phase: Saturation
% 38.63/5.95 % (790437)Time elapsed: 0.504 s
% 38.63/5.95 % (790437)Peak memory usage: 20 MB
% 38.63/5.95 % (790437)Instructions burned: 870 (million)
% 38.63/5.95 % (790439)ott+10_1_sil=32000:tgt=ground:random_seed=1306999468:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 38.63/5.95 % (790429)Instruction limit reached!
% 38.63/5.95 % (790429)------------------------------
% 38.63/5.95 % (790429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790429)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790429)Termination reason: Instruction limit
% 38.63/5.95 % (790429)Termination phase: Saturation
% 38.63/5.95 % (790429)Time elapsed: 2.936 s
% 38.63/5.95 % (790429)Peak memory usage: 33 MB
% 38.63/5.95 % (790429)Instructions burned: 5131 (million)
% 38.63/5.95 % (790441)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2892963520:i=54282_2959 on theBenchmark for (2959ds/54282Mi)
% 38.63/5.95 % TRYING [1]
% 38.63/5.95 % TRYING [2]
% 38.63/5.95 % TRYING [3]
% 38.63/5.95 % TRYING [4]
% 38.63/5.95 % TRYING [8]
% 38.63/5.95 % TRYING [5]
% 38.63/5.95 % (790425)Instruction limit reached!
% 38.63/5.95 % (790425)------------------------------
% 38.63/5.95 % (790425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790425)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790425)Termination reason: Instruction limit
% 38.63/5.95 % (790425)Termination phase: Finite model building constraint generation
% 38.63/5.95 % (790425)Time elapsed: 3.365 s
% 38.63/5.95 % (790425)Peak memory usage: 602 MB
% 38.63/5.95 % (790425)Instructions burned: 9516 (million)
% 38.63/5.95 % (790443)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1884723690:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 38.63/5.95 % TRYING [6]
% 38.63/5.95 % TRYING [8]
% 38.63/5.95 % (790423)Instruction limit reached!
% 38.63/5.95 % (790423)------------------------------
% 38.63/5.95 % (790423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.95 % (790423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.95 % (790423)CaDiCaL version: 2.1.3
% 38.63/5.95 % (790423)Termination reason: Instruction limit
% 38.63/5.95 % (790423)Termination phase: Finite model building constraint generation
% 38.63/5.95 % (790423)Time elapsed: 4.607 s
% 38.63/5.95 % (790423)Peak memory usage: 184 MB
% 38.63/5.95 % (790423)Instructions burned: 22064 (million)
% 38.63/5.95 % (790445)dis+21_1_sil=32000:sas=cadical:random_seed=2257933396:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi)
% 38.63/5.95 % TRYING [7]
% 38.63/5.95 % (790390) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-790384-790390"...
% 38.63/5.95 % (790390)...printing done.
% 38.63/5.95 % (790390)Refutation found. Thanks to Tanya!
% 38.63/5.95 % SZS status Theorem for theBenchmark
% 38.63/5.95 % SZS output start Proof for theBenchmark
% See solution above
% 38.63/5.96 % (790390)------------------------------
% 38.63/5.96 % (790390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.63/5.96 % (790390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/5.96 % (790390)CaDiCaL version: 2.1.3
% 38.63/5.96 % (790390)Termination reason: Refutation
% 38.63/5.96 % (790390)Time elapsed: 5.444 s
% 38.63/5.96 % (790390)Peak memory usage: 56 MB
% 38.63/5.96 % (790390)Instructions burned: 9978 (million)
% 38.63/5.96 % (790384)Success in time 5.528 s
% 38.63/5.96 % Vampire exiting
%------------------------------------------------------------------------------