%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU231+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:47:53 PM UTC 2026
% Result : Theorem 19.93s 3.74s
% Output : Refutation 21.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 42
% Syntax : Number of formulae : 328 ( 46 unt; 29 def)
% Number of atoms : 962 ( 77 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1017 ( 383 ~; 505 |; 79 &)
% ( 40 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 30 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 258 ( 2 sgn 242 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f4,axiom,
! [X0] :
( ordinal(X0)
=> ( epsilon_transitive(X0)
& epsilon_connected(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_ordinal1) ).
fof(f8,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f9,axiom,
! [X0] :
( epsilon_transitive(X0)
<=> ! [X1] :
( in(X1,X0)
=> subset(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_ordinal1) ).
fof(f10,axiom,
! [X0] :
( epsilon_connected(X0)
<=> ! [X1,X2] :
~ ( in(X1,X0)
& in(X2,X0)
& ~ in(X1,X2)
& X1 != X2
& ~ in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_ordinal1) ).
fof(f11,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f12,axiom,
! [X0,X1,X2] :
( X2 = set_difference(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
& ~ in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f13,axiom,
! [X0,X1] :
( proper_subset(X0,X1)
<=> ( subset(X0,X1)
& X0 != X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f23,axiom,
! [X0,X1] : ~ proper_subset(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f34,axiom,
! [X0,X1] : subset(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f36,conjecture,
! [X0] :
( epsilon_transitive(X0)
=> ! [X1] :
( ordinal(X1)
=> ( proper_subset(X0,X1)
=> in(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_ordinal1) ).
fof(f37,negated_conjecture,
~ ! [X0] :
( epsilon_transitive(X0)
=> ! [X1] :
( ordinal(X1)
=> ( proper_subset(X0,X1)
=> in(X0,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f39,axiom,
! [X0,X1] :
( set_difference(X0,X1) = empty_set
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_xboole_1) ).
fof(f48,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& ! [X2] :
~ ( in(X2,X1)
& ! [X3] :
~ ( in(X3,X1)
& in(X3,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_tarski) ).
fof(f50,plain,
! [X0] : ~ proper_subset(X0,X0),
inference(rectify,[],[f23]) ).
fof(f51,plain,
! [X0] : subset(X0,X0),
inference(rectify,[],[f34]) ).
fof(f57,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f60,plain,
! [X0] :
( ( epsilon_transitive(X0)
& epsilon_connected(X0) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f66,plain,
! [X0] :
( epsilon_transitive(X0)
<=> ! [X1] :
( subset(X1,X0)
| ~ in(X1,X0) ) ),
inference(ennf_transformation,[],[f9]) ).
fof(f67,plain,
! [X0] :
( epsilon_connected(X0)
<=> ! [X1,X2] :
( ~ in(X1,X0)
| ~ in(X2,X0)
| in(X1,X2)
| X1 = X2
| in(X2,X1) ) ),
inference(ennf_transformation,[],[f10]) ).
fof(f68,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f72,plain,
? [X0] :
( ? [X1] :
( ~ in(X0,X1)
& proper_subset(X0,X1)
& ordinal(X1) )
& epsilon_transitive(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f73,plain,
? [X0] :
( ? [X1] :
( ~ in(X0,X1)
& proper_subset(X0,X1)
& ordinal(X1) )
& epsilon_transitive(X0) ),
inference(flattening,[],[f72]) ).
fof(f82,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ? [X2] :
( in(X2,X1)
& ! [X3] :
( ~ in(X3,X1)
| ~ in(X3,X2) ) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f84,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f85,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] :
( ( epsilon_transitive(X0)
| ? [X1] :
( ~ subset(X1,X0)
& in(X1,X0) ) )
& ( ! [X1] :
( subset(X1,X0)
| ~ in(X1,X0) )
| ~ epsilon_transitive(X0) ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f87,plain,
! [X0] :
( ( epsilon_transitive(X0)
| ? [X1] :
( ~ subset(X1,X0)
& in(X1,X0) ) )
& ( ! [X2] :
( subset(X2,X0)
| ~ in(X2,X0) )
| ~ epsilon_transitive(X0) ) ),
inference(rectify,[],[f86]) ).
fof(f88,plain,
! [X0] :
( ( epsilon_transitive(X0)
| ( ~ subset(sK0(X0),X0)
& in(sK0(X0),X0) ) )
& ( ! [X2] :
( subset(X2,X0)
| ~ in(X2,X0) )
| ~ epsilon_transitive(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f87]) ).
fof(f89,plain,
! [X0] :
( ( epsilon_connected(X0)
| ? [X1,X2] :
( in(X1,X0)
& in(X2,X0)
& ~ in(X1,X2)
& X1 != X2
& ~ in(X2,X1) ) )
& ( ! [X1,X2] :
( ~ in(X1,X0)
| ~ in(X2,X0)
| in(X1,X2)
| X1 = X2
| in(X2,X1) )
| ~ epsilon_connected(X0) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f90,plain,
! [X0] :
( ( epsilon_connected(X0)
| ? [X1,X2] :
( in(X1,X0)
& in(X2,X0)
& ~ in(X1,X2)
& X1 != X2
& ~ in(X2,X1) ) )
& ( ! [X3,X4] :
( ~ in(X3,X0)
| ~ in(X4,X0)
| in(X3,X4)
| X3 = X4
| in(X4,X3) )
| ~ epsilon_connected(X0) ) ),
inference(rectify,[],[f89]) ).
fof(f91,plain,
! [X0] :
( ( epsilon_connected(X0)
| ( in(sK1(X0),X0)
& in(sK2(X0),X0)
& ~ in(sK1(X0),sK2(X0))
& sK1(X0) != sK2(X0)
& ~ in(sK2(X0),sK1(X0)) ) )
& ( ! [X3,X4] :
( ~ in(X3,X0)
| ~ in(X4,X0)
| in(X3,X4)
| X3 = X4
| in(X4,X3) )
| ~ epsilon_connected(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X1,sK1(X0)),skolemize(X2,sK2(X0))],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f93,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK3(X0,X1),X1)
& in(sK3(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f93]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| in(X3,X1) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f96,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,X0)
| in(X3,X1) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ? [X3] :
( ( ~ in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) )
& ( ( in(X3,X0)
& ~ in(X3,X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1) )
& ( ( in(X4,X0)
& ~ in(X4,X1) )
| ~ in(X4,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(rectify,[],[f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( X2 = set_difference(X0,X1)
| ( ( ~ in(sK4(X0,X1,X2),X0)
| in(sK4(X0,X1,X2),X1)
| ~ in(sK4(X0,X1,X2),X2) )
& ( ( in(sK4(X0,X1,X2),X0)
& ~ in(sK4(X0,X1,X2),X1) )
| in(sK4(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1) )
& ( ( in(X4,X0)
& ~ in(X4,X1) )
| ~ in(X4,X2) ) )
| set_difference(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( ( proper_subset(X0,X1)
| ~ subset(X0,X1)
| X0 = X1 )
& ( ( subset(X0,X1)
& X0 != X1 )
| ~ proper_subset(X0,X1) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f100,plain,
! [X0,X1] :
( ( proper_subset(X0,X1)
| ~ subset(X0,X1)
| X0 = X1 )
& ( ( subset(X0,X1)
& X0 != X1 )
| ~ proper_subset(X0,X1) ) ),
inference(flattening,[],[f99]) ).
fof(f112,plain,
( ~ in(sK16,sK17)
& proper_subset(sK16,sK17)
& ordinal(sK17)
& epsilon_transitive(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X0,sK16),skolemize(X1,sK17)],[f73]) ).
fof(f113,plain,
! [X0,X1] :
( ( set_difference(X0,X1) = empty_set
| ~ subset(X0,X1) )
& ( subset(X0,X1)
| set_difference(X0,X1) != empty_set ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ( in(sK18(X1),X1)
& ! [X3] :
( ~ in(X3,X1)
| ~ in(X3,sK18(X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X1))],[f82]) ).
fof(f116,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
fof(f119,plain,
! [X0] :
( ~ ordinal(X0)
| epsilon_connected(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f120,plain,
! [X0] :
( ~ ordinal(X0)
| epsilon_transitive(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f127,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f85]) ).
fof(f128,plain,
! [X2,X0] :
( ~ in(X2,X0)
| subset(X2,X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[],[f88]) ).
fof(f131,plain,
! [X3,X0,X4] :
( ~ in(X4,X0)
| ~ in(X3,X0)
| in(X3,X4)
| X3 = X4
| in(X4,X3)
| ~ epsilon_connected(X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f137,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f138,plain,
! [X0,X1] :
( in(sK3(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f139,plain,
! [X0,X1] :
( ~ in(sK3(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f140,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,X1)
| ~ in(X4,X2)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f98]) ).
fof(f141,plain,
! [X2,X0,X1,X4] :
( in(X4,X0)
| ~ in(X4,X2)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f98]) ).
fof(f142,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| in(X4,X1)
| set_difference(X0,X1) != X2 ),
inference(cnf_transformation,[],[f98]) ).
fof(f147,plain,
! [X0,X1] :
( ~ proper_subset(X0,X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f156,plain,
! [X0] : ~ proper_subset(X0,X0),
inference(cnf_transformation,[],[f50]) ).
fof(f176,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[],[f51]) ).
fof(f178,plain,
epsilon_transitive(sK16),
inference(cnf_transformation,[],[f112]) ).
fof(f179,plain,
ordinal(sK17),
inference(cnf_transformation,[],[f112]) ).
fof(f180,plain,
proper_subset(sK16,sK17),
inference(cnf_transformation,[],[f112]) ).
fof(f181,plain,
~ in(sK16,sK17),
inference(cnf_transformation,[],[f112]) ).
fof(f183,plain,
! [X0,X1] :
( set_difference(X0,X1) != empty_set
| subset(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f184,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ),
inference(cnf_transformation,[],[f113]) ).
fof(f194,plain,
! [X3,X0,X1] :
( ~ in(X3,sK18(X1))
| ~ in(X3,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f195,plain,
! [X0,X1] :
( ~ in(X0,X1)
| in(sK18(X1),X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f199,plain,
! [X0,X1,X4] :
( in(X4,set_difference(X0,X1))
| ~ in(X4,X0)
| in(X4,X1) ),
inference(equality_resolution,[],[f142]) ).
fof(f200,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,X1))
| in(X4,X0) ),
inference(equality_resolution,[],[f141]) ).
fof(f201,plain,
! [X0,X1,X4] :
( ~ in(X4,set_difference(X0,X1))
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f140]) ).
fof(f203,plain,
! [X0,X1] :
( subset(sK3(X0,X1),X0)
| subset(X0,X1)
| ~ epsilon_transitive(X0) ),
inference(resolution,[],[f138,f128]) ).
fof(f206,plain,
epsilon_connected(sK17),
inference(resolution,[],[f119,f179]) ).
fof(f214,plain,
! [X2,X0,X1] :
( ~ in(X2,X0)
| in(sK18(set_difference(X0,X1)),set_difference(X0,X1))
| in(X2,X1) ),
inference(resolution,[],[f195,f199]) ).
fof(f215,plain,
subset(sK16,sK17),
inference(resolution,[],[f147,f180]) ).
fof(f216,plain,
! [X0] :
( ~ in(X0,sK16)
| in(X0,sK17) ),
inference(resolution,[],[f215,f137]) ).
fof(f217,plain,
( ~ subset(sK17,sK16)
| sK16 = sK17 ),
inference(resolution,[],[f215,f127]) ).
fof(f219,definition,
( spl19_1
<=> sK16 = sK17 ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f221,plain,
( sK16 = sK17
| ~ spl19_1 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f223,definition,
( spl19_2
<=> subset(sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition]) ).
fof(f225,plain,
( ~ subset(sK17,sK16)
| spl19_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,plain,
( spl19_1
| ~ spl19_2 ),
inference(avatar_split_clause,[],[f217,f223,f219]) ).
fof(f236,plain,
! [X0] :
( in(sK3(sK16,X0),sK17)
| subset(sK16,X0) ),
inference(resolution,[],[f216,f138]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ in(sK3(sK18(X0),X1),X0)
| ~ in(X2,X0)
| subset(sK18(X0),X1) ),
inference(resolution,[],[f194,f138]) ).
fof(f276,definition,
( spl19_8
<=> epsilon_transitive(sK17) ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f277,plain,
( epsilon_transitive(sK17)
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f278,plain,
( ~ epsilon_transitive(sK17)
| spl19_8 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f286,plain,
! [X2,X0,X1] :
( ~ in(X2,sK3(X0,X1))
| ~ epsilon_transitive(X0)
| subset(X0,X1)
| in(X2,X0) ),
inference(resolution,[],[f203,f137]) ).
fof(f295,plain,
! [X0,X1] :
( subset(X0,X1)
| empty_set = set_difference(sK3(X0,X1),X0)
| ~ epsilon_transitive(X0) ),
inference(resolution,[],[f184,f203]) ).
fof(f309,plain,
! [X2,X0,X1] :
( in(sK18(set_difference(X0,X1)),set_difference(X0,X1))
| in(sK3(X0,X2),X1)
| subset(X0,X2) ),
inference(resolution,[],[f214,f138]) ).
fof(f328,plain,
! [X0] : empty_set = set_difference(X0,X0),
inference(resolution,[],[f176,f184]) ).
fof(f333,plain,
! [X0,X1] :
( ~ in(X0,empty_set)
| ~ in(X0,X1) ),
inference(superposition,[],[f201,f328]) ).
fof(f335,plain,
! [X0,X1] :
( ~ in(X0,empty_set)
| in(X0,X1) ),
inference(superposition,[],[f200,f328]) ).
fof(f337,plain,
! [X0] : ~ in(X0,empty_set),
inference(forward_subsumption_resolution,[],[f333,f335]) ).
fof(f347,plain,
! [X2,X0,X1] :
( in(sK18(set_difference(X0,X1)),X0)
| in(sK3(X0,X2),X1)
| subset(X0,X2) ),
inference(resolution,[],[f309,f200]) ).
fof(f352,plain,
! [X2,X3,X0,X1] :
( in(sK18(set_difference(X2,X3)),set_difference(X2,X3))
| in(sK18(set_difference(X0,X2)),set_difference(X0,X2))
| in(sK3(X0,X1),X3)
| subset(X0,X1) ),
inference(resolution,[],[f309,f214]) ).
fof(f377,plain,
! [X0,X1] :
( ~ in(X0,sK17)
| in(X0,sK3(sK16,X1))
| sK3(sK16,X1) = X0
| in(sK3(sK16,X1),X0)
| ~ epsilon_connected(sK17)
| subset(sK16,X1) ),
inference(resolution,[],[f131,f236]) ).
fof(f378,plain,
! [X0,X1] :
( in(sK3(sK16,X1),X0)
| in(X0,sK3(sK16,X1))
| sK3(sK16,X1) = X0
| ~ in(X0,sK17)
| subset(sK16,X1) ),
inference(forward_subsumption_resolution,[],[f377,f206]) ).
fof(f394,plain,
epsilon_transitive(sK17),
inference(resolution,[],[f120,f179]) ).
fof(f395,plain,
( $false
| spl19_8 ),
inference(forward_subsumption_resolution,[],[f394,f278]) ).
fof(f396,plain,
spl19_8,
inference(avatar_contradiction_clause,[],[f395]) ).
fof(f558,plain,
! [X0,X1] :
( ~ in(X0,sK3(X0,X1))
| subset(X0,X1) ),
inference(resolution,[],[f116,f138]) ).
fof(f593,plain,
! [X0,X1] :
( in(sK18(set_difference(X0,X1)),X0)
| subset(X0,X1)
| subset(X0,X1) ),
inference(resolution,[],[f347,f139]) ).
fof(f612,plain,
! [X0,X1] :
( in(sK18(set_difference(X0,X1)),X0)
| subset(X0,X1) ),
inference(duplicate_literal_removal,[],[f593]) ).
fof(f912,plain,
! [X0] :
( in(X0,sK3(sK16,X0))
| sK3(sK16,X0) = X0
| ~ in(X0,sK17)
| subset(sK16,X0)
| subset(sK16,X0) ),
inference(resolution,[],[f378,f139]) ).
fof(f945,plain,
! [X0] :
( in(X0,sK3(sK16,X0))
| sK3(sK16,X0) = X0
| ~ in(X0,sK17)
| subset(sK16,X0) ),
inference(duplicate_literal_removal,[],[f912]) ).
fof(f1002,plain,
! [X2,X3,X0,X1] :
( ~ in(sK3(sK18(set_difference(X1,X2)),X3),X1)
| subset(sK18(set_difference(X1,X2)),X3)
| ~ in(X0,set_difference(X1,X2))
| in(sK3(sK18(set_difference(X1,X2)),X3),X2) ),
inference(resolution,[],[f271,f199]) ).
fof(f1050,plain,
( empty_set = set_difference(sK3(sK17,sK16),sK17)
| ~ epsilon_transitive(sK17)
| spl19_2 ),
inference(resolution,[],[f295,f225]) ).
fof(f1053,plain,
( empty_set = set_difference(sK3(sK17,sK16),sK17)
| spl19_2
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f1050,f277]) ).
fof(f1277,plain,
! [X2,X0,X1] :
( in(sK18(set_difference(X2,X1)),set_difference(X2,X1))
| in(sK18(set_difference(X0,X2)),set_difference(X0,X2))
| subset(X0,X1)
| subset(X0,X1) ),
inference(resolution,[],[f352,f139]) ).
fof(f1311,plain,
! [X2,X0,X1] :
( in(sK18(set_difference(X2,X1)),set_difference(X2,X1))
| in(sK18(set_difference(X0,X2)),set_difference(X0,X2))
| subset(X0,X1) ),
inference(duplicate_literal_removal,[],[f1277]) ).
fof(f1329,plain,
! [X2,X0,X1] :
( ~ in(sK18(set_difference(X0,X1)),X1)
| subset(X0,X2)
| in(sK18(set_difference(X1,X2)),set_difference(X1,X2)) ),
inference(resolution,[],[f1311,f201]) ).
fof(f1330,plain,
! [X2,X0,X1] :
( in(sK18(set_difference(X1,X2)),set_difference(X1,X2))
| subset(X0,X2)
| in(sK18(set_difference(X0,X1)),X0) ),
inference(resolution,[],[f1311,f200]) ).
fof(f2501,definition,
( spl19_29
<=> in(sK17,sK17) ),
introduced(definition,[new_symbols(definition,[spl19_29])],[avatar_definition]) ).
fof(f2803,plain,
( empty_set != empty_set
| subset(sK3(sK17,sK16),sK17)
| spl19_2
| ~ spl19_8 ),
inference(superposition,[],[f183,f1053]) ).
fof(f2820,plain,
( ! [X0] :
( in(sK18(empty_set),empty_set)
| in(sK3(sK3(sK17,sK16),X0),sK17)
| subset(sK3(sK17,sK16),X0) )
| spl19_2
| ~ spl19_8 ),
inference(superposition,[],[f309,f1053]) ).
fof(f2850,plain,
( subset(sK3(sK17,sK16),sK17)
| spl19_2
| ~ spl19_8 ),
inference(trivial_inequality_removal,[],[f2803]) ).
fof(f2877,definition,
( spl19_52
<=> subset(sK3(sK17,sK16),sK17) ),
introduced(definition,[new_symbols(definition,[spl19_52])],[avatar_definition]) ).
fof(f2879,plain,
( subset(sK3(sK17,sK16),sK17)
| ~ spl19_52 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2889,definition,
( spl19_54
<=> ! [X0] :
( in(sK3(sK3(sK17,sK16),X0),sK17)
| subset(sK3(sK17,sK16),X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_54])],[avatar_definition]) ).
fof(f2890,plain,
( ! [X0] :
( in(sK3(sK3(sK17,sK16),X0),sK17)
| subset(sK3(sK17,sK16),X0) )
| ~ spl19_54 ),
inference(avatar_component_clause,[],[f2889]) ).
fof(f2892,plain,
( ! [X0] :
( in(sK3(sK3(sK17,sK16),X0),sK17)
| subset(sK3(sK17,sK16),X0) )
| spl19_2
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f2820,f337]) ).
fof(f2906,plain,
( spl19_52
| spl19_2
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f2850,f276,f223,f2877]) ).
fof(f2909,plain,
( spl19_54
| spl19_2
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f2892,f276,f223,f2889]) ).
fof(f2914,plain,
( proper_subset(sK16,sK16)
| ~ spl19_1 ),
inference(superposition,[],[f180,f221]) ).
fof(f2938,plain,
( $false
| ~ spl19_1 ),
inference(forward_subsumption_resolution,[],[f2914,f156]) ).
fof(f2939,plain,
~ spl19_1,
inference(avatar_contradiction_clause,[],[f2938]) ).
fof(f2962,plain,
( ~ subset(sK17,sK3(sK17,sK16))
| sK17 = sK3(sK17,sK16)
| ~ spl19_52 ),
inference(resolution,[],[f2879,f127]) ).
fof(f2964,definition,
( spl19_57
<=> sK17 = sK3(sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl19_57])],[avatar_definition]) ).
fof(f2966,plain,
( sK17 = sK3(sK17,sK16)
| ~ spl19_57 ),
inference(avatar_component_clause,[],[f2964]) ).
fof(f2968,definition,
( spl19_58
<=> subset(sK17,sK3(sK17,sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_58])],[avatar_definition]) ).
fof(f2970,plain,
( ~ subset(sK17,sK3(sK17,sK16))
| spl19_58 ),
inference(avatar_component_clause,[],[f2968]) ).
fof(f2971,plain,
( spl19_57
| ~ spl19_58
| ~ spl19_52 ),
inference(avatar_split_clause,[],[f2962,f2877,f2968,f2964]) ).
fof(f2981,plain,
( in(sK17,sK17)
| subset(sK17,sK16)
| ~ spl19_57 ),
inference(superposition,[],[f138,f2966]) ).
fof(f2990,plain,
( ~ in(sK17,sK17)
| subset(sK17,sK16)
| ~ spl19_57 ),
inference(superposition,[],[f558,f2966]) ).
fof(f2994,plain,
( ~ in(sK17,sK17)
| spl19_2
| ~ spl19_57 ),
inference(forward_subsumption_resolution,[],[f2990,f225]) ).
fof(f2996,plain,
( in(sK17,sK17)
| spl19_2
| ~ spl19_57 ),
inference(forward_subsumption_resolution,[],[f2981,f225]) ).
fof(f2997,plain,
( ~ spl19_29
| spl19_2
| ~ spl19_57 ),
inference(avatar_split_clause,[],[f2994,f2964,f223,f2501]) ).
fof(f2998,plain,
( spl19_29
| spl19_2
| ~ spl19_57 ),
inference(avatar_split_clause,[],[f2996,f2964,f223,f2501]) ).
fof(f3068,plain,
! [X0] :
( sK3(sK16,X0) = X0
| ~ in(X0,sK17)
| subset(sK16,X0)
| ~ epsilon_transitive(sK16)
| subset(sK16,X0)
| in(X0,sK16) ),
inference(resolution,[],[f945,f286]) ).
fof(f3078,plain,
! [X0] :
( sK3(sK16,X0) = X0
| ~ in(X0,sK17)
| subset(sK16,X0)
| ~ epsilon_transitive(sK16)
| in(X0,sK16) ),
inference(duplicate_literal_removal,[],[f3068]) ).
fof(f3079,plain,
! [X0] :
( ~ in(X0,sK17)
| sK3(sK16,X0) = X0
| subset(sK16,X0)
| in(X0,sK16) ),
inference(forward_subsumption_resolution,[],[f3078,f178]) ).
fof(f3941,definition,
( spl19_113
<=> in(sK18(set_difference(sK17,sK16)),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_113])],[avatar_definition]) ).
fof(f3942,plain,
( ~ in(sK18(set_difference(sK17,sK16)),sK16)
| spl19_113 ),
inference(avatar_component_clause,[],[f3941]) ).
fof(f3943,plain,
( in(sK18(set_difference(sK17,sK16)),sK16)
| ~ spl19_113 ),
inference(avatar_component_clause,[],[f3941]) ).
fof(f3945,definition,
( spl19_114
<=> subset(sK16,sK18(set_difference(sK17,sK16))) ),
introduced(definition,[new_symbols(definition,[spl19_114])],[avatar_definition]) ).
fof(f3946,plain,
( ~ subset(sK16,sK18(set_difference(sK17,sK16)))
| spl19_114 ),
inference(avatar_component_clause,[],[f3945]) ).
fof(f3947,plain,
( subset(sK16,sK18(set_difference(sK17,sK16)))
| ~ spl19_114 ),
inference(avatar_component_clause,[],[f3945]) ).
fof(f3949,definition,
( spl19_115
<=> sK18(set_difference(sK17,sK16)) = sK3(sK16,sK18(set_difference(sK17,sK16))) ),
introduced(definition,[new_symbols(definition,[spl19_115])],[avatar_definition]) ).
fof(f3951,plain,
( sK18(set_difference(sK17,sK16)) = sK3(sK16,sK18(set_difference(sK17,sK16)))
| ~ spl19_115 ),
inference(avatar_component_clause,[],[f3949]) ).
fof(f4086,plain,
( ~ subset(sK18(set_difference(sK17,sK16)),sK16)
| sK16 = sK18(set_difference(sK17,sK16))
| ~ spl19_114 ),
inference(resolution,[],[f3947,f127]) ).
fof(f4088,definition,
( spl19_118
<=> sK16 = sK18(set_difference(sK17,sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_118])],[avatar_definition]) ).
fof(f4090,plain,
( sK16 = sK18(set_difference(sK17,sK16))
| ~ spl19_118 ),
inference(avatar_component_clause,[],[f4088]) ).
fof(f4092,definition,
( spl19_119
<=> subset(sK18(set_difference(sK17,sK16)),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_119])],[avatar_definition]) ).
fof(f4094,plain,
( ~ subset(sK18(set_difference(sK17,sK16)),sK16)
| spl19_119 ),
inference(avatar_component_clause,[],[f4092]) ).
fof(f4095,plain,
( spl19_118
| ~ spl19_119
| ~ spl19_114 ),
inference(avatar_split_clause,[],[f4086,f3945,f4092,f4088]) ).
fof(f4120,plain,
( in(sK16,sK17)
| subset(sK17,sK16)
| ~ spl19_118 ),
inference(superposition,[],[f612,f4090]) ).
fof(f4182,definition,
( spl19_129
<=> ! [X1] : ~ in(X1,set_difference(sK17,sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_129])],[avatar_definition]) ).
fof(f4183,plain,
( ! [X1] : ~ in(X1,set_difference(sK17,sK16))
| ~ spl19_129 ),
inference(avatar_component_clause,[],[f4182]) ).
fof(f4201,definition,
( spl19_133
<=> ! [X0] :
( subset(sK17,X0)
| in(sK18(set_difference(sK16,X0)),set_difference(sK16,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl19_133])],[avatar_definition]) ).
fof(f4202,plain,
( ! [X0] :
( in(sK18(set_difference(sK16,X0)),set_difference(sK16,X0))
| subset(sK17,X0) )
| ~ spl19_133 ),
inference(avatar_component_clause,[],[f4201]) ).
fof(f4222,plain,
( subset(sK17,sK16)
| ~ spl19_118 ),
inference(forward_subsumption_resolution,[],[f4120,f181]) ).
fof(f4248,plain,
( $false
| spl19_2
| ~ spl19_118 ),
inference(forward_subsumption_resolution,[],[f4222,f225]) ).
fof(f4249,plain,
( spl19_2
| ~ spl19_118 ),
inference(avatar_contradiction_clause,[],[f4248]) ).
fof(f4562,definition,
( spl19_149
<=> in(sK3(sK17,sK16),sK17) ),
introduced(definition,[new_symbols(definition,[spl19_149])],[avatar_definition]) ).
fof(f4563,plain,
( in(sK3(sK17,sK16),sK17)
| ~ spl19_149 ),
inference(avatar_component_clause,[],[f4562]) ).
fof(f4564,plain,
( ~ in(sK3(sK17,sK16),sK17)
| spl19_149 ),
inference(avatar_component_clause,[],[f4562]) ).
fof(f5526,definition,
( spl19_196
<=> subset(sK16,sK3(sK17,sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_196])],[avatar_definition]) ).
fof(f5527,plain,
( ~ subset(sK16,sK3(sK17,sK16))
| spl19_196 ),
inference(avatar_component_clause,[],[f5526]) ).
fof(f5528,plain,
( subset(sK16,sK3(sK17,sK16))
| ~ spl19_196 ),
inference(avatar_component_clause,[],[f5526]) ).
fof(f5831,plain,
( sK3(sK17,sK16) = sK3(sK16,sK3(sK17,sK16))
| subset(sK16,sK3(sK17,sK16))
| in(sK3(sK17,sK16),sK16)
| ~ spl19_149 ),
inference(resolution,[],[f4563,f3079]) ).
fof(f5833,plain,
( ~ in(sK17,sK3(sK17,sK16))
| ~ spl19_149 ),
inference(resolution,[],[f4563,f116]) ).
fof(f6321,plain,
( ~ subset(sK3(sK17,sK16),sK16)
| sK16 = sK3(sK17,sK16)
| ~ spl19_196 ),
inference(resolution,[],[f5528,f127]) ).
fof(f6323,definition,
( spl19_237
<=> sK16 = sK3(sK17,sK16) ),
introduced(definition,[new_symbols(definition,[spl19_237])],[avatar_definition]) ).
fof(f6325,plain,
( sK16 = sK3(sK17,sK16)
| ~ spl19_237 ),
inference(avatar_component_clause,[],[f6323]) ).
fof(f6327,definition,
( spl19_238
<=> subset(sK3(sK17,sK16),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_238])],[avatar_definition]) ).
fof(f6329,plain,
( ~ subset(sK3(sK17,sK16),sK16)
| spl19_238 ),
inference(avatar_component_clause,[],[f6327]) ).
fof(f6330,plain,
( spl19_237
| ~ spl19_238
| ~ spl19_196 ),
inference(avatar_split_clause,[],[f6321,f5526,f6327,f6323]) ).
fof(f6393,plain,
( in(sK16,sK17)
| subset(sK17,sK16)
| ~ spl19_237 ),
inference(superposition,[],[f138,f6325]) ).
fof(f6408,plain,
( subset(sK17,sK16)
| ~ spl19_237 ),
inference(forward_subsumption_resolution,[],[f6393,f181]) ).
fof(f6436,plain,
( $false
| spl19_2
| ~ spl19_237 ),
inference(forward_subsumption_resolution,[],[f6408,f225]) ).
fof(f6437,plain,
( spl19_2
| ~ spl19_237 ),
inference(avatar_contradiction_clause,[],[f6436]) ).
fof(f6522,plain,
( sK3(sK17,sK16) = sK3(sK16,sK3(sK17,sK16))
| in(sK3(sK17,sK16),sK16)
| ~ spl19_149
| spl19_196 ),
inference(forward_subsumption_resolution,[],[f5831,f5527]) ).
fof(f6631,definition,
( spl19_259
<=> in(sK3(sK17,sK16),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_259])],[avatar_definition]) ).
fof(f6632,plain,
( ~ in(sK3(sK17,sK16),sK16)
| spl19_259 ),
inference(avatar_component_clause,[],[f6631]) ).
fof(f6633,plain,
( in(sK3(sK17,sK16),sK16)
| ~ spl19_259 ),
inference(avatar_component_clause,[],[f6631]) ).
fof(f6635,definition,
( spl19_260
<=> sK3(sK17,sK16) = sK3(sK16,sK3(sK17,sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_260])],[avatar_definition]) ).
fof(f6637,plain,
( sK3(sK17,sK16) = sK3(sK16,sK3(sK17,sK16))
| ~ spl19_260 ),
inference(avatar_component_clause,[],[f6635]) ).
fof(f6638,plain,
( spl19_259
| spl19_260
| ~ spl19_149
| spl19_196 ),
inference(avatar_split_clause,[],[f6522,f5526,f4562,f6635,f6631]) ).
fof(f6659,plain,
( subset(sK17,sK16)
| spl19_149 ),
inference(resolution,[],[f4564,f138]) ).
fof(f6662,plain,
( $false
| spl19_2
| spl19_149 ),
inference(forward_subsumption_resolution,[],[f6659,f225]) ).
fof(f6663,plain,
( spl19_2
| spl19_149 ),
inference(avatar_contradiction_clause,[],[f6662]) ).
fof(f6668,plain,
( subset(sK17,sK16)
| ~ spl19_259 ),
inference(resolution,[],[f6633,f139]) ).
fof(f6680,plain,
( $false
| spl19_2
| ~ spl19_259 ),
inference(forward_subsumption_resolution,[],[f6668,f225]) ).
fof(f6681,plain,
( spl19_2
| ~ spl19_259 ),
inference(avatar_contradiction_clause,[],[f6680]) ).
fof(f6688,plain,
( in(sK3(sK17,sK16),sK16)
| subset(sK16,sK3(sK17,sK16))
| ~ spl19_260 ),
inference(superposition,[],[f138,f6637]) ).
fof(f6709,plain,
( subset(sK16,sK3(sK17,sK16))
| spl19_259
| ~ spl19_260 ),
inference(forward_subsumption_resolution,[],[f6688,f6632]) ).
fof(f6719,plain,
( $false
| spl19_196
| spl19_259
| ~ spl19_260 ),
inference(forward_subsumption_resolution,[],[f6709,f5527]) ).
fof(f6720,plain,
( spl19_196
| spl19_259
| ~ spl19_260 ),
inference(avatar_contradiction_clause,[],[f6719]) ).
fof(f6727,plain,
( ! [X0] :
( in(X0,sK3(sK17,sK16))
| ~ in(X0,sK16) )
| ~ spl19_196 ),
inference(resolution,[],[f5528,f137]) ).
fof(f7097,plain,
( ! [X0] :
( ~ in(sK3(X0,sK3(sK17,sK16)),sK16)
| subset(X0,sK3(sK17,sK16)) )
| ~ spl19_196 ),
inference(resolution,[],[f6727,f139]) ).
fof(f7169,plain,
( ! [X0] :
( subset(X0,sK3(sK17,sK16))
| in(sK18(set_difference(X0,sK16)),X0)
| subset(X0,sK3(sK17,sK16)) )
| ~ spl19_196 ),
inference(resolution,[],[f7097,f347]) ).
fof(f7173,plain,
( ! [X0] :
( in(sK18(set_difference(X0,sK16)),X0)
| subset(X0,sK3(sK17,sK16)) )
| ~ spl19_196 ),
inference(duplicate_literal_removal,[],[f7169]) ).
fof(f7206,plain,
( subset(sK17,sK3(sK17,sK16))
| sK18(set_difference(sK17,sK16)) = sK3(sK16,sK18(set_difference(sK17,sK16)))
| subset(sK16,sK18(set_difference(sK17,sK16)))
| in(sK18(set_difference(sK17,sK16)),sK16)
| ~ spl19_196 ),
inference(resolution,[],[f7173,f3079]) ).
fof(f7213,plain,
( sK18(set_difference(sK17,sK16)) = sK3(sK16,sK18(set_difference(sK17,sK16)))
| subset(sK16,sK18(set_difference(sK17,sK16)))
| in(sK18(set_difference(sK17,sK16)),sK16)
| spl19_58
| ~ spl19_196 ),
inference(forward_subsumption_resolution,[],[f7206,f2970]) ).
fof(f7214,plain,
( sK18(set_difference(sK17,sK16)) = sK3(sK16,sK18(set_difference(sK17,sK16)))
| in(sK18(set_difference(sK17,sK16)),sK16)
| spl19_58
| spl19_114
| ~ spl19_196 ),
inference(forward_subsumption_resolution,[],[f7213,f3946]) ).
fof(f7215,plain,
( spl19_113
| spl19_115
| spl19_58
| spl19_114
| ~ spl19_196 ),
inference(avatar_split_clause,[],[f7214,f5526,f3945,f2968,f3949,f3941]) ).
fof(f7222,plain,
( ! [X0] :
( subset(sK17,X0)
| in(sK18(set_difference(sK16,X0)),set_difference(sK16,X0)) )
| ~ spl19_113 ),
inference(resolution,[],[f3943,f1329]) ).
fof(f7234,plain,
( spl19_133
| ~ spl19_113 ),
inference(avatar_split_clause,[],[f7222,f3941,f4201]) ).
fof(f7546,plain,
( in(sK18(set_difference(sK17,sK16)),sK16)
| subset(sK16,sK18(set_difference(sK17,sK16)))
| ~ spl19_115 ),
inference(superposition,[],[f138,f3951]) ).
fof(f7576,plain,
( subset(sK16,sK18(set_difference(sK17,sK16)))
| spl19_113
| ~ spl19_115 ),
inference(forward_subsumption_resolution,[],[f7546,f3942]) ).
fof(f7590,plain,
( $false
| spl19_113
| spl19_114
| ~ spl19_115 ),
inference(forward_subsumption_resolution,[],[f7576,f3946]) ).
fof(f7591,plain,
( spl19_113
| spl19_114
| ~ spl19_115 ),
inference(avatar_contradiction_clause,[],[f7590]) ).
fof(f8738,plain,
( ! [X0] :
( in(sK18(set_difference(sK16,X0)),set_difference(sK16,X0))
| subset(sK17,X0) )
| ~ spl19_129 ),
inference(resolution,[],[f4183,f1311]) ).
fof(f8836,plain,
( spl19_133
| ~ spl19_129 ),
inference(avatar_split_clause,[],[f8738,f4182,f4201]) ).
fof(f12055,definition,
( spl19_419
<=> in(sK3(sK3(sK17,sK16),sK16),sK17) ),
introduced(definition,[new_symbols(definition,[spl19_419])],[avatar_definition]) ).
fof(f12056,plain,
( in(sK3(sK3(sK17,sK16),sK16),sK17)
| ~ spl19_419 ),
inference(avatar_component_clause,[],[f12055]) ).
fof(f12057,plain,
( ~ in(sK3(sK3(sK17,sK16),sK16),sK17)
| spl19_419 ),
inference(avatar_component_clause,[],[f12055]) ).
fof(f12116,plain,
( subset(sK3(sK17,sK16),sK16)
| ~ spl19_54
| spl19_419 ),
inference(resolution,[],[f12057,f2890]) ).
fof(f12120,plain,
( $false
| ~ spl19_54
| spl19_238
| spl19_419 ),
inference(forward_subsumption_resolution,[],[f12116,f6329]) ).
fof(f12121,plain,
( ~ spl19_54
| spl19_238
| spl19_419 ),
inference(avatar_contradiction_clause,[],[f12120]) ).
fof(f12124,definition,
( spl19_422
<=> sK17 = sK3(sK3(sK17,sK16),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_422])],[avatar_definition]) ).
fof(f12126,plain,
( sK17 = sK3(sK3(sK17,sK16),sK16)
| ~ spl19_422 ),
inference(avatar_component_clause,[],[f12124]) ).
fof(f12128,plain,
( sK3(sK3(sK17,sK16),sK16) = sK3(sK16,sK3(sK3(sK17,sK16),sK16))
| subset(sK16,sK3(sK3(sK17,sK16),sK16))
| in(sK3(sK3(sK17,sK16),sK16),sK16)
| ~ spl19_419 ),
inference(resolution,[],[f12056,f3079]) ).
fof(f12131,plain,
( subset(sK3(sK3(sK17,sK16),sK16),sK17)
| ~ epsilon_transitive(sK17)
| ~ spl19_419 ),
inference(resolution,[],[f12056,f128]) ).
fof(f12138,plain,
( subset(sK3(sK3(sK17,sK16),sK16),sK17)
| ~ spl19_8
| ~ spl19_419 ),
inference(forward_subsumption_resolution,[],[f12131,f277]) ).
fof(f12140,definition,
( spl19_423
<=> in(sK3(sK3(sK17,sK16),sK16),sK16) ),
introduced(definition,[new_symbols(definition,[spl19_423])],[avatar_definition]) ).
fof(f12141,plain,
( ~ in(sK3(sK3(sK17,sK16),sK16),sK16)
| spl19_423 ),
inference(avatar_component_clause,[],[f12140]) ).
fof(f12142,plain,
( in(sK3(sK3(sK17,sK16),sK16),sK16)
| ~ spl19_423 ),
inference(avatar_component_clause,[],[f12140]) ).
fof(f12144,definition,
( spl19_424
<=> subset(sK16,sK3(sK3(sK17,sK16),sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_424])],[avatar_definition]) ).
fof(f12146,plain,
( subset(sK16,sK3(sK3(sK17,sK16),sK16))
| ~ spl19_424 ),
inference(avatar_component_clause,[],[f12144]) ).
fof(f12148,definition,
( spl19_425
<=> sK3(sK3(sK17,sK16),sK16) = sK3(sK16,sK3(sK3(sK17,sK16),sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_425])],[avatar_definition]) ).
fof(f12150,plain,
( sK3(sK3(sK17,sK16),sK16) = sK3(sK16,sK3(sK3(sK17,sK16),sK16))
| ~ spl19_425 ),
inference(avatar_component_clause,[],[f12148]) ).
fof(f12151,plain,
( spl19_423
| spl19_424
| spl19_425
| ~ spl19_419 ),
inference(avatar_split_clause,[],[f12128,f12055,f12148,f12144,f12140]) ).
fof(f12309,plain,
( ~ subset(sK17,sK3(sK3(sK17,sK16),sK16))
| sK17 = sK3(sK3(sK17,sK16),sK16)
| ~ spl19_8
| ~ spl19_419 ),
inference(resolution,[],[f12138,f127]) ).
fof(f12311,definition,
( spl19_432
<=> subset(sK17,sK3(sK3(sK17,sK16),sK16)) ),
introduced(definition,[new_symbols(definition,[spl19_432])],[avatar_definition]) ).
fof(f12313,plain,
( ~ subset(sK17,sK3(sK3(sK17,sK16),sK16))
| spl19_432 ),
inference(avatar_component_clause,[],[f12311]) ).
fof(f12314,plain,
( spl19_422
| ~ spl19_432
| ~ spl19_8
| ~ spl19_419 ),
inference(avatar_split_clause,[],[f12309,f12055,f276,f12311,f12124]) ).
fof(f12459,plain,
( in(sK3(sK3(sK17,sK16),sK16),sK16)
| subset(sK16,sK3(sK3(sK17,sK16),sK16))
| ~ spl19_425 ),
inference(superposition,[],[f138,f12150]) ).
fof(f12482,plain,
( empty_set = set_difference(sK16,sK3(sK3(sK17,sK16),sK16))
| ~ spl19_424 ),
inference(resolution,[],[f12146,f184]) ).
fof(f13093,plain,
( in(sK18(empty_set),empty_set)
| subset(sK17,sK16)
| ~ spl19_133 ),
inference(superposition,[],[f4202,f328]) ).
fof(f13094,plain,
( subset(sK17,sK16)
| ~ spl19_133 ),
inference(forward_subsumption_resolution,[],[f13093,f337]) ).
fof(f13098,plain,
( $false
| spl19_2
| ~ spl19_133 ),
inference(forward_subsumption_resolution,[],[f13094,f225]) ).
fof(f13099,plain,
( spl19_2
| ~ spl19_133 ),
inference(avatar_contradiction_clause,[],[f13098]) ).
fof(f15662,plain,
( in(sK17,sK3(sK17,sK16))
| subset(sK3(sK17,sK16),sK16)
| ~ spl19_422 ),
inference(superposition,[],[f138,f12126]) ).
fof(f15682,plain,
( subset(sK3(sK17,sK16),sK16)
| ~ spl19_149
| ~ spl19_422 ),
inference(forward_subsumption_resolution,[],[f15662,f5833]) ).
fof(f15713,plain,
( $false
| ~ spl19_149
| spl19_238
| ~ spl19_422 ),
inference(forward_subsumption_resolution,[],[f15682,f6329]) ).
fof(f15714,plain,
( ~ spl19_149
| spl19_238
| ~ spl19_422 ),
inference(avatar_contradiction_clause,[],[f15713]) ).
fof(f20540,plain,
( ! [X0] :
( in(sK18(empty_set),empty_set)
| subset(X0,sK3(sK3(sK17,sK16),sK16))
| in(sK18(set_difference(X0,sK16)),X0) )
| ~ spl19_424 ),
inference(superposition,[],[f1330,f12482]) ).
fof(f20560,plain,
( ! [X0] :
( subset(X0,sK3(sK3(sK17,sK16),sK16))
| in(sK18(set_difference(X0,sK16)),X0) )
| ~ spl19_424 ),
inference(forward_subsumption_resolution,[],[f20540,f337]) ).
fof(f20632,plain,
( in(sK18(set_difference(sK17,sK16)),sK17)
| ~ spl19_424
| spl19_432 ),
inference(resolution,[],[f20560,f12313]) ).
fof(f20691,plain,
( subset(sK16,sK3(sK3(sK17,sK16),sK16))
| spl19_423
| ~ spl19_425 ),
inference(forward_subsumption_resolution,[],[f12459,f12141]) ).
fof(f20741,plain,
( subset(sK3(sK17,sK16),sK16)
| ~ spl19_423 ),
inference(resolution,[],[f12142,f139]) ).
fof(f20754,plain,
( $false
| spl19_238
| ~ spl19_423 ),
inference(forward_subsumption_resolution,[],[f20741,f6329]) ).
fof(f20755,plain,
( spl19_238
| ~ spl19_423 ),
inference(avatar_contradiction_clause,[],[f20754]) ).
fof(f20935,plain,
( spl19_424
| spl19_423
| ~ spl19_425 ),
inference(avatar_split_clause,[],[f20691,f12148,f12140,f12144]) ).
fof(f20970,plain,
( subset(sK18(set_difference(sK17,sK16)),sK17)
| ~ epsilon_transitive(sK17)
| ~ spl19_424
| spl19_432 ),
inference(resolution,[],[f20632,f128]) ).
fof(f20979,plain,
( subset(sK18(set_difference(sK17,sK16)),sK17)
| ~ spl19_8
| ~ spl19_424
| spl19_432 ),
inference(forward_subsumption_resolution,[],[f20970,f277]) ).
fof(f23537,definition,
( spl19_816
<=> ! [X0] :
( in(sK3(sK18(set_difference(sK17,sK16)),X0),sK17)
| subset(sK18(set_difference(sK17,sK16)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_816])],[avatar_definition]) ).
fof(f23538,plain,
( ! [X0] :
( in(sK3(sK18(set_difference(sK17,sK16)),X0),sK17)
| subset(sK18(set_difference(sK17,sK16)),X0) )
| ~ spl19_816 ),
inference(avatar_component_clause,[],[f23537]) ).
fof(f24724,plain,
( ! [X0] :
( ~ in(X0,sK18(set_difference(sK17,sK16)))
| in(X0,sK17) )
| ~ spl19_8
| ~ spl19_424
| spl19_432 ),
inference(resolution,[],[f20979,f137]) ).
fof(f24746,plain,
( ! [X0] :
( in(sK3(sK18(set_difference(sK17,sK16)),X0),sK17)
| subset(sK18(set_difference(sK17,sK16)),X0) )
| ~ spl19_8
| ~ spl19_424
| spl19_432 ),
inference(resolution,[],[f24724,f138]) ).
fof(f24824,plain,
( spl19_816
| ~ spl19_8
| ~ spl19_424
| spl19_432 ),
inference(avatar_split_clause,[],[f24746,f12311,f12144,f276,f23537]) ).
fof(f25201,plain,
( ! [X0,X1] :
( subset(sK18(set_difference(sK17,sK16)),X0)
| subset(sK18(set_difference(sK17,sK16)),X0)
| ~ in(X1,set_difference(sK17,sK16))
| in(sK3(sK18(set_difference(sK17,sK16)),X0),sK16) )
| ~ spl19_816 ),
inference(resolution,[],[f23538,f1002]) ).
fof(f25217,plain,
( ! [X0,X1] :
( subset(sK18(set_difference(sK17,sK16)),X0)
| ~ in(X1,set_difference(sK17,sK16))
| in(sK3(sK18(set_difference(sK17,sK16)),X0),sK16) )
| ~ spl19_816 ),
inference(duplicate_literal_removal,[],[f25201]) ).
fof(f25224,definition,
( spl19_897
<=> ! [X0] :
( subset(sK18(set_difference(sK17,sK16)),X0)
| in(sK3(sK18(set_difference(sK17,sK16)),X0),sK16) ) ),
introduced(definition,[new_symbols(definition,[spl19_897])],[avatar_definition]) ).
fof(f25225,plain,
( ! [X0] :
( in(sK3(sK18(set_difference(sK17,sK16)),X0),sK16)
| subset(sK18(set_difference(sK17,sK16)),X0) )
| ~ spl19_897 ),
inference(avatar_component_clause,[],[f25224]) ).
fof(f25226,plain,
( spl19_129
| spl19_897
| ~ spl19_816 ),
inference(avatar_split_clause,[],[f25217,f23537,f25224,f4182]) ).
fof(f25229,plain,
( subset(sK18(set_difference(sK17,sK16)),sK16)
| subset(sK18(set_difference(sK17,sK16)),sK16)
| ~ spl19_897 ),
inference(resolution,[],[f25225,f139]) ).
fof(f25242,plain,
( subset(sK18(set_difference(sK17,sK16)),sK16)
| ~ spl19_897 ),
inference(duplicate_literal_removal,[],[f25229]) ).
fof(f25248,plain,
( $false
| spl19_119
| ~ spl19_897 ),
inference(forward_subsumption_resolution,[],[f25242,f4094]) ).
fof(f25249,plain,
( spl19_119
| ~ spl19_897 ),
inference(avatar_contradiction_clause,[],[f25248]) ).
cnf(s1,plain,
( spl19_1
| ~ spl19_2 ),
inference(sat_conversion,[],[f226]) ).
cnf(s7,plain,
spl19_8,
inference(sat_conversion,[],[f396]) ).
cnf(s79,plain,
( spl19_2
| ~ spl19_8
| spl19_52 ),
inference(sat_conversion,[],[f2906]) ).
cnf(s82,plain,
( spl19_2
| ~ spl19_8
| spl19_54 ),
inference(sat_conversion,[],[f2909]) ).
cnf(s85,plain,
~ spl19_1,
inference(sat_conversion,[],[f2939]) ).
cnf(s86,plain,
( ~ spl19_52
| spl19_57
| ~ spl19_58 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s88,plain,
( spl19_2
| ~ spl19_29
| ~ spl19_57 ),
inference(sat_conversion,[],[f2997]) ).
cnf(s89,plain,
( spl19_2
| spl19_29
| ~ spl19_57 ),
inference(sat_conversion,[],[f2998]) ).
cnf(s153,plain,
( ~ spl19_114
| spl19_118
| ~ spl19_119 ),
inference(sat_conversion,[],[f4095]) ).
cnf(s182,plain,
( spl19_2
| ~ spl19_118 ),
inference(sat_conversion,[],[f4249]) ).
cnf(s381,plain,
( ~ spl19_196
| spl19_237
| ~ spl19_238 ),
inference(sat_conversion,[],[f6330]) ).
cnf(s388,plain,
( spl19_2
| ~ spl19_237 ),
inference(sat_conversion,[],[f6437]) ).
cnf(s417,plain,
( ~ spl19_149
| spl19_196
| spl19_259
| spl19_260 ),
inference(sat_conversion,[],[f6638]) ).
cnf(s420,plain,
( spl19_2
| spl19_149 ),
inference(sat_conversion,[],[f6663]) ).
cnf(s423,plain,
( spl19_2
| ~ spl19_259 ),
inference(sat_conversion,[],[f6681]) ).
cnf(s426,plain,
( spl19_196
| spl19_259
| ~ spl19_260 ),
inference(sat_conversion,[],[f6720]) ).
cnf(s467,plain,
( spl19_58
| spl19_113
| spl19_114
| spl19_115
| ~ spl19_196 ),
inference(sat_conversion,[],[f7215]) ).
cnf(s468,plain,
( ~ spl19_113
| spl19_133 ),
inference(sat_conversion,[],[f7234]) ).
cnf(s489,plain,
( spl19_113
| spl19_114
| ~ spl19_115 ),
inference(sat_conversion,[],[f7591]) ).
cnf(s562,plain,
( ~ spl19_129
| spl19_133 ),
inference(sat_conversion,[],[f8836]) ).
cnf(s794,plain,
( ~ spl19_54
| spl19_238
| spl19_419 ),
inference(sat_conversion,[],[f12121]) ).
cnf(s796,plain,
( ~ spl19_419
| spl19_423
| spl19_424
| spl19_425 ),
inference(sat_conversion,[],[f12151]) ).
cnf(s814,plain,
( ~ spl19_8
| ~ spl19_419
| spl19_422
| ~ spl19_432 ),
inference(sat_conversion,[],[f12314]) ).
cnf(s828,plain,
( spl19_2
| ~ spl19_133 ),
inference(sat_conversion,[],[f13099]) ).
cnf(s978,plain,
( ~ spl19_149
| spl19_238
| ~ spl19_422 ),
inference(sat_conversion,[],[f15714]) ).
cnf(s1261,plain,
( spl19_238
| ~ spl19_423 ),
inference(sat_conversion,[],[f20755]) ).
cnf(s1278,plain,
( spl19_423
| spl19_424
| ~ spl19_425 ),
inference(sat_conversion,[],[f20935]) ).
cnf(s1605,plain,
( ~ spl19_8
| ~ spl19_424
| spl19_432
| spl19_816 ),
inference(sat_conversion,[],[f24824]) ).
cnf(s1643,plain,
( spl19_129
| ~ spl19_816
| spl19_897 ),
inference(sat_conversion,[],[f25226]) ).
cnf(s1645,plain,
( spl19_119
| ~ spl19_897 ),
inference(sat_conversion,[],[f25249]) ).
cnf(s1695,plain,
~ spl19_2,
inference(rat,[],[s1,s85]) ).
cnf(s1696,plain,
~ spl19_133,
inference(rat,[],[s828,s1695]) ).
cnf(s1700,plain,
~ spl19_259,
inference(rat,[],[s423,s1695]) ).
cnf(s1701,plain,
spl19_149,
inference(rat,[],[s420,s1695]) ).
cnf(s1702,plain,
~ spl19_237,
inference(rat,[],[s388,s1695]) ).
cnf(s1703,plain,
~ spl19_118,
inference(rat,[],[s182,s1695]) ).
cnf(s1704,plain,
spl19_54,
inference(rat,[],[s82,s7,s1695]) ).
cnf(s1707,plain,
spl19_52,
inference(rat,[],[s79,s7,s1695]) ).
cnf(s1709,plain,
~ spl19_129,
inference(rat,[],[s562,s1696]) ).
cnf(s1710,plain,
~ spl19_113,
inference(rat,[],[s468,s1696]) ).
cnf(s1726,plain,
spl19_196,
inference(rat,[],[s417,s426,s1700,s1701]) ).
cnf(s1730,plain,
~ spl19_238,
inference(rat,[],[s381,s1702,s1726]) ).
cnf(s1732,plain,
~ spl19_423,
inference(rat,[],[s1261,s1730]) ).
cnf(s1734,plain,
~ spl19_422,
inference(rat,[],[s978,s1701,s1730]) ).
cnf(s1738,plain,
spl19_419,
inference(rat,[],[s794,s1704,s1730]) ).
cnf(s1747,plain,
~ spl19_432,
inference(rat,[],[s814,s1734,s7,s1738]) ).
cnf(s1764,plain,
spl19_424,
inference(rat,[],[s796,s1278,s1732,s1738]) ).
cnf(s1766,plain,
spl19_816,
inference(rat,[],[s1605,s1747,s7,s1764]) ).
cnf(s1775,plain,
spl19_897,
inference(rat,[],[s1643,s1709,s1766]) ).
cnf(s1778,plain,
spl19_119,
inference(rat,[],[s1645,s1775]) ).
cnf(s1780,plain,
~ spl19_114,
inference(rat,[],[s153,s1703,s1778]) ).
cnf(s1781,plain,
~ spl19_115,
inference(rat,[],[s489,s1710,s1780]) ).
cnf(s1783,plain,
spl19_58,
inference(rat,[],[s467,s1781,s1726,s1710,s1780]) ).
cnf(s1785,plain,
spl19_57,
inference(rat,[],[s86,s1707,s1783]) ).
cnf(s1786,plain,
spl19_29,
inference(rat,[],[s89,s1695,s1785]) ).
cnf(s1787,plain,
$false,
inference(rat,[],[s88,s1695,s1785,s1786]) ).
fof(f25250,plain,
$false,
inference(avatar_sat_refutation,[],[s1787]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU231+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 04:11:55 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.47/2.52 % (3571713)Detected formulas, will run a generic FOF schedule.
% 11.47/2.52 % (3571722)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1483640142:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.47/2.52 % (3571722)Instruction limit reached!
% 11.47/2.52 % (3571722)------------------------------
% 11.47/2.52 % (3571722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (3571722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (3571722)CaDiCaL version: 2.1.3
% 11.47/2.52 % (3571722)Termination reason: Instruction limit
% 11.47/2.52 % (3571722)Termination phase: Saturation
% 11.47/2.52 % (3571722)Time elapsed: 0.037 s
% 11.47/2.52 % (3571722)Peak memory usage: 88 MB
% 11.47/2.52 % (3571722)Instructions burned: 120 (million)
% 11.47/2.52 % (3571719)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2642655811:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.47/2.52 % (3571720)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2291587210:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.47/2.52 % (3571721)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=362958963:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.47/2.52 % (3571724)dis-21_1_sil=8000:lcm=predicate:random_seed=1325567882:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.47/2.52 % (3571718)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3537292199:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.47/2.52 % (3571723)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1232850542:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.47/2.52 % (3571721)Refutation not found, incomplete strategy
% 11.47/2.52 % (3571721)------------------------------
% 11.47/2.52 % (3571721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (3571721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (3571721)CaDiCaL version: 2.1.3
% 11.47/2.52 % (3571721)Termination reason: Refutation not found, incomplete strategy
% 11.47/2.52 % (3571721)Time elapsed: 0.002 s
% 11.47/2.52 % (3571721)Peak memory usage: 88 MB
% 11.47/2.52 % (3571721)Instructions burned: 1 (million)
% 11.47/2.52 % (3571724)Instruction limit reached!
% 11.47/2.52 % (3571724)------------------------------
% 11.47/2.52 % (3571724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (3571724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (3571724)CaDiCaL version: 2.1.3
% 11.47/2.52 % (3571724)Termination reason: Instruction limit
% 11.47/2.52 % (3571724)Termination phase: Saturation
% 11.47/2.52 % (3571724)Time elapsed: 0.075 s
% 11.47/2.52 % (3571724)Peak memory usage: 89 MB
% 11.47/2.52 % (3571724)Instructions burned: 129 (million)
% 11.47/2.52 % (3571723)Instruction limit reached!
% 11.47/2.52 % (3571723)------------------------------
% 11.47/2.52 % (3571723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (3571723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (3571723)CaDiCaL version: 2.1.3
% 11.47/2.52 % (3571723)Termination reason: Instruction limit
% 11.47/2.52 % (3571723)Termination phase: Saturation
% 11.47/2.52 % (3571723)Time elapsed: 0.098 s
% 11.47/2.52 % (3571723)Peak memory usage: 90 MB
% 11.47/2.52 % (3571723)Instructions burned: 140 (million)
% 11.47/2.52 % (3571726)lrs+10_1_sil=8000:sp=occurrence:random_seed=206306626:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.47/2.52 % (3571726)Instruction limit reached!
% 11.47/2.52 % (3571726)------------------------------
% 11.47/2.52 % (3571726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.47/2.52 % (3571726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.47/2.52 % (3571726)CaDiCaL version: 2.1.3
% 11.47/2.52 % (3571726)Termination reason: Instruction limit
% 11.47/2.52 % (3571726)Termination phase: Saturation
% 11.47/2.52 % (3571726)Time elapsed: 0.099 s
% 11.47/2.52 % (3571726)Peak memory usage: 91 MB
% 11.47/2.52 % (3571726)Instructions burned: 288 (million)
% 18.66/3.51 % (3571733)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1112816901:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.66/3.51 % (3571733)Refutation not found, incomplete strategy
% 18.66/3.51 % (3571733)------------------------------
% 18.66/3.51 % (3571733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.66/3.51 % (3571733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.66/3.51 % (3571733)CaDiCaL version: 2.1.3
% 18.66/3.51 % (3571733)Termination reason: Refutation not found, incomplete strategy
% 18.66/3.51 % (3571733)Time elapsed: 0.002 s
% 18.66/3.51 % (3571733)Peak memory usage: 88 MB
% 18.66/3.51 % (3571733)Instructions burned: 1 (million)
% 18.66/3.51 % (3571721)------------------------------
% 18.66/3.51 % (3571721)------------------------------
% 18.66/3.51 % (3571734)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4066955786:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.66/3.51 % (3571736)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3229260409:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 18.66/3.51 % (3571736)Instruction limit reached!
% 18.66/3.51 % (3571736)------------------------------
% 18.66/3.51 % (3571736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.66/3.51 % (3571736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.66/3.51 % (3571736)CaDiCaL version: 2.1.3
% 18.66/3.51 % (3571736)Termination reason: Instruction limit
% 18.66/3.51 % (3571736)Termination phase: Saturation
% 18.66/3.51 % (3571736)Time elapsed: 0.074 s
% 18.66/3.51 % (3571736)Peak memory usage: 91 MB
% 18.66/3.51 % (3571736)Instructions burned: 251 (million)
% 18.66/3.51 % (3571739)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1009734662:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.66/3.51 % (3571739)Refutation not found, incomplete strategy
% 18.66/3.51 % (3571739)------------------------------
% 18.66/3.51 % (3571739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.66/3.51 % (3571739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.66/3.51 % (3571739)CaDiCaL version: 2.1.3
% 18.66/3.51 % (3571739)Termination reason: Refutation not found, incomplete strategy
% 18.66/3.51 % (3571739)Time elapsed: 0.003 s
% 18.66/3.51 % (3571739)Peak memory usage: 88 MB
% 18.66/3.51 % (3571739)Instructions burned: 2 (million)
% 18.66/3.51 % (3571733)------------------------------
% 18.66/3.51 % (3571733)------------------------------
% 18.66/3.51 % (3571734)Instruction limit reached!
% 18.66/3.51 % (3571734)------------------------------
% 18.66/3.51 % (3571734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.66/3.51 % (3571734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.66/3.51 % (3571734)CaDiCaL version: 2.1.3
% 18.66/3.51 % (3571734)Termination reason: Instruction limit
% 18.66/3.51 % (3571734)Termination phase: Saturation
% 18.66/3.51 % (3571734)Time elapsed: 0.220 s
% 18.66/3.51 % (3571734)Peak memory usage: 91 MB
% 18.66/3.51 % (3571734)Instructions burned: 325 (million)
% 18.66/3.51 % (3571741)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2880630982:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.66/3.51 % (3571743)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2854159223:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 18.66/3.51 % (3571744)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3706577179:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 18.66/3.51 % (3571739)------------------------------
% 18.66/3.51 % (3571739)------------------------------
% 18.66/3.51 % (3571744)Instruction limit reached!
% 18.66/3.51 % (3571744)------------------------------
% 18.66/3.51 % (3571744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.66/3.51 % (3571744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.66/3.51 % (3571744)CaDiCaL version: 2.1.3
% 18.66/3.51 % (3571744)Termination reason: Instruction limit
% 18.66/3.51 % (3571744)Termination phase: Saturation
% 18.66/3.51 % (3571744)Time elapsed: 0.068 s
% 18.66/3.51 % (3571744)Peak memory usage: 88 MB
% 18.66/3.51 % (3571744)Instructions burned: 127 (million)
% 18.66/3.51 % (3571743)Instruction limit reached!
% 18.66/3.51 % (3571743)------------------------------
% 18.66/3.51 % (3571743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571743)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571743)Termination reason: Instruction limit
% 19.93/3.74 % (3571743)Termination phase: Saturation
% 19.93/3.74 % (3571743)Time elapsed: 0.081 s
% 19.93/3.74 % (3571743)Peak memory usage: 89 MB
% 19.93/3.74 % (3571743)Instructions burned: 113 (million)
% 19.93/3.74 % (3571748)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2519528618:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 19.93/3.74 % (3571748)Refutation not found, incomplete strategy
% 19.93/3.74 % (3571748)------------------------------
% 19.93/3.74 % (3571748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571748)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571748)Termination reason: Refutation not found, incomplete strategy
% 19.93/3.74 % (3571748)Time elapsed: 0.003 s
% 19.93/3.74 % (3571748)Peak memory usage: 88 MB
% 19.93/3.74 % (3571748)Instructions burned: 2 (million)
% 19.93/3.74 % (3571749)lrs+10_1_sil=8000:sp=occurrence:random_seed=2388865901:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 19.93/3.74 % (3571750)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3682510383:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 19.93/3.74 % (3571748)------------------------------
% 19.93/3.74 % (3571748)------------------------------
% 19.93/3.74 % (3571750)Instruction limit reached!
% 19.93/3.74 % (3571750)------------------------------
% 19.93/3.74 % (3571750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571750)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571750)Termination reason: Instruction limit
% 19.93/3.74 % (3571750)Termination phase: Saturation
% 19.93/3.74 % (3571750)Time elapsed: 0.248 s
% 19.93/3.74 % (3571750)Peak memory usage: 90 MB
% 19.93/3.74 % (3571750)Instructions burned: 437 (million)
% 19.93/3.74 % (3571754)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1982227994:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 19.93/3.74 % (3571755)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=719213126:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 19.93/3.74 % (3571755)Instruction limit reached!
% 19.93/3.74 % (3571755)------------------------------
% 19.93/3.74 % (3571755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571755)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571755)Termination reason: Instruction limit
% 19.93/3.74 % (3571755)Termination phase: Saturation
% 19.93/3.74 % (3571755)Time elapsed: 0.072 s
% 19.93/3.74 % (3571755)Peak memory usage: 93 MB
% 19.93/3.74 % (3571755)Instructions burned: 134 (million)
% 19.93/3.74 % (3571741)Instruction limit reached!
% 19.93/3.74 % (3571741)------------------------------
% 19.93/3.74 % (3571741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571741)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571741)Termination reason: Instruction limit
% 19.93/3.74 % (3571741)Termination phase: Saturation
% 19.93/3.74 % (3571741)Time elapsed: 0.854 s
% 19.93/3.74 % (3571741)Peak memory usage: 140 MB
% 19.93/3.74 % (3571741)Instructions burned: 2350 (million)
% 19.93/3.74 % (3571749)Instruction limit reached!
% 19.93/3.74 % (3571749)------------------------------
% 19.93/3.74 % (3571749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571749)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571749)Termination reason: Instruction limit
% 19.93/3.74 % (3571749)Termination phase: Saturation
% 19.93/3.74 % (3571749)Time elapsed: 0.551 s
% 19.93/3.74 % (3571749)Peak memory usage: 96 MB
% 19.93/3.74 % (3571749)Instructions burned: 908 (million)
% 19.93/3.74 % (3571759)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4147204501:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 19.93/3.74 % (3571758)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3477796367:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 19.93/3.74 % (3571758)Refutation not found, incomplete strategy
% 19.93/3.74 % (3571758)------------------------------
% 19.93/3.74 % (3571758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571758)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571758)Termination reason: Refutation not found, incomplete strategy
% 19.93/3.74 % (3571758)Time elapsed: 0.002 s
% 19.93/3.74 % (3571758)Peak memory usage: 88 MB
% 19.93/3.74 % (3571758)Instructions burned: 2 (million)
% 19.93/3.74 % (3571760)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3015028828:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 19.93/3.74 % (3571760)Instruction limit reached!
% 19.93/3.74 % (3571760)------------------------------
% 19.93/3.74 % (3571760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571760)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571760)Termination reason: Instruction limit
% 19.93/3.74 % (3571760)Termination phase: Saturation
% 19.93/3.74 % (3571760)Time elapsed: 0.093 s
% 19.93/3.74 % (3571760)Peak memory usage: 90 MB
% 19.93/3.74 % (3571760)Instructions burned: 125 (million)
% 19.93/3.74 % (3571758)------------------------------
% 19.93/3.74 % (3571758)------------------------------
% 19.93/3.74 % (3571764)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3018894853:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 19.93/3.74 % (3571765)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1351847516:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 19.93/3.74 % (3571765)Refutation not found, incomplete strategy
% 19.93/3.74 % (3571765)------------------------------
% 19.93/3.74 % (3571765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571765)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571765)Termination reason: Refutation not found, incomplete strategy
% 19.93/3.74 % (3571765)Time elapsed: 0.002 s
% 19.93/3.74 % (3571765)Peak memory usage: 88 MB
% 19.93/3.74 % (3571765)Instructions burned: 1 (million)
% 19.93/3.74 % (3571764)Instruction limit reached!
% 19.93/3.74 % (3571764)------------------------------
% 19.93/3.74 % (3571764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571764)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571764)Termination reason: Instruction limit
% 19.93/3.74 % (3571764)Termination phase: Saturation
% 19.93/3.74 % (3571764)Time elapsed: 0.087 s
% 19.93/3.74 % (3571764)Peak memory usage: 90 MB
% 19.93/3.74 % (3571764)Instructions burned: 134 (million)
% 19.93/3.74 % (3571768)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1656089865:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 19.93/3.74 % (3571765)------------------------------
% 19.93/3.74 % (3571765)------------------------------
% 19.93/3.74 % (3571770)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1974630286:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 19.93/3.74 % (3571768)Instruction limit reached!
% 19.93/3.74 % (3571768)------------------------------
% 19.93/3.74 % (3571768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571768)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571768)Termination reason: Instruction limit
% 19.93/3.74 % (3571768)Termination phase: Saturation
% 19.93/3.74 % (3571768)Time elapsed: 0.235 s
% 19.93/3.74 % (3571768)Peak memory usage: 93 MB
% 19.93/3.74 % (3571768)Instructions burned: 432 (million)
% 19.93/3.74 % (3571718)First to succeed.
% 19.93/3.74 % (3571718)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3571713"
% 19.93/3.74 % (3571772)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1704296427:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 19.93/3.74 % (3571772)Instruction limit reached!
% 19.93/3.74 % (3571772)------------------------------
% 19.93/3.74 % (3571772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.93/3.74 % (3571772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.74 % (3571772)CaDiCaL version: 2.1.3
% 19.93/3.74 % (3571772)Termination reason: Instruction limit
% 19.93/3.74 % (3571772)Termination phase: Saturation
% 19.93/3.74 % (3571772)Time elapsed: 0.097 s
% 19.93/3.74 % (3571772)Peak memory usage: 90 MB
% 19.93/3.74 % (3571772)Instructions burned: 151 (million)
% 19.93/3.74 % (3571718)Refutation found. Thanks to Tanya!
% 19.93/3.74 % SZS status Theorem for theBenchmark
% 19.93/3.74 % SZS output start Proof for theBenchmark
% See solution above
% 21.03/3.94 % (3571718)------------------------------
% 21.03/3.94 % (3571718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.03/3.94 % (3571718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.03/3.94 % (3571718)CaDiCaL version: 2.1.3
% 21.03/3.94 % (3571718)Termination reason: Refutation
% 21.03/3.94 % (3571718)Time elapsed: 2.453 s
% 21.03/3.94 % (3571718)Peak memory usage: 150 MB
% 21.03/3.94 % (3571718)Instructions burned: 3644 (million)
% 21.03/3.94 % (3571718)------------------------------
% 21.03/3.94 % (3571718)------------------------------
% 21.03/3.94 % (3571713)Success in time 2.889 s
% 21.03/3.94 % Vampire exiting
%------------------------------------------------------------------------------