%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM406+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:15:04 PM UTC 2026
% Result : Theorem 11.87s 2.35s
% Output : Refutation 12.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 19
% Syntax : Number of formulae : 187 ( 19 unt; 6 def)
% Number of atoms : 696 ( 101 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 812 ( 303 ~; 423 |; 53 &)
% ( 15 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 7 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 246 ( 0 sgn 229 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f3,axiom,
! [X0] :
( ordinal(X0)
=> ( epsilon_transitive(X0)
& epsilon_connected(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_ordinal1) ).
fof(f10,axiom,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_ordinal1) ).
fof(f11,axiom,
! [X0] :
( epsilon_transitive(X0)
<=> ! [X1] :
( in(X1,X0)
=> subset(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_ordinal1) ).
fof(f12,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f20,axiom,
! [X0] :
( ordinal(X0)
=> ( ~ empty(succ(X0))
& epsilon_transitive(succ(X0))
& epsilon_connected(succ(X0))
& ordinal(succ(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_ordinal1) ).
fof(f37,axiom,
! [X0,X1] :
( ( ordinal(X0)
& ordinal(X1) )
=> ( ordinal_subset(X0,X1)
<=> subset(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_ordinal1) ).
fof(f40,axiom,
! [X0,X1] :
( ordinal(X1)
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,succ(X1))
& ~ in(X3,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e3_44__ordinal1) ).
fof(f41,axiom,
! [X0] : in(X0,succ(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_ordinal1) ).
fof(f44,axiom,
! [X0] :
( ordinal(X0)
=> ! [X1] :
( ordinal(X1)
=> ~ ( ~ in(X0,X1)
& X0 != X1
& ~ in(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t24_ordinal1) ).
fof(f46,axiom,
! [X0,X1] :
( ordinal(X1)
=> ~ ( subset(X0,X1)
& X0 != empty_set
& ! [X2] :
( ordinal(X2)
=> ~ ( in(X2,X0)
& ! [X3] :
( ordinal(X3)
=> ( in(X3,X0)
=> ordinal_subset(X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_ordinal1) ).
fof(f47,axiom,
! [X0] :
~ ! [X1] :
( ordinal(X1)
=> in(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_ordinal1) ).
fof(f48,conjecture,
! [X0] :
? [X1] :
( ordinal(X1)
& ~ in(X1,X0)
& ! [X2] :
( ordinal(X2)
=> ( ~ in(X2,X0)
=> ordinal_subset(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_ordinal1) ).
fof(f49,negated_conjecture,
~ ! [X0] :
? [X1] :
( ordinal(X1)
& ~ in(X1,X0)
& ! [X2] :
( ordinal(X2)
=> ( ~ in(X2,X0)
=> ordinal_subset(X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f67,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f1]) ).
fof(f69,plain,
! [X0] :
( ( epsilon_transitive(X0)
& epsilon_connected(X0) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f78,plain,
! [X0] :
( epsilon_transitive(X0)
<=> ! [X1] :
( subset(X1,X0)
| ~ in(X1,X0) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f83,plain,
! [X0] :
( ( ~ empty(succ(X0))
& epsilon_transitive(succ(X0))
& epsilon_connected(succ(X0))
& ordinal(succ(X0)) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f85,plain,
! [X0,X1] :
( ( ordinal_subset(X0,X1)
<=> subset(X0,X1) )
| ~ ordinal(X0)
| ~ ordinal(X1) ),
inference(ennf_transformation,[],[f37]) ).
fof(f86,plain,
! [X0,X1] :
( ( ordinal_subset(X0,X1)
<=> subset(X0,X1) )
| ~ ordinal(X0)
| ~ ordinal(X1) ),
inference(flattening,[],[f85]) ).
fof(f89,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,succ(X1))
& ~ in(X3,X0) ) )
| ~ ordinal(X1) ),
inference(ennf_transformation,[],[f40]) ).
fof(f91,plain,
! [X0] :
( ! [X1] :
( in(X0,X1)
| X0 = X1
| in(X1,X0)
| ~ ordinal(X1) )
| ~ ordinal(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f92,plain,
! [X0] :
( ! [X1] :
( in(X0,X1)
| X0 = X1
| in(X1,X0)
| ~ ordinal(X1) )
| ~ ordinal(X0) ),
inference(flattening,[],[f91]) ).
fof(f95,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| ? [X2] :
( in(X2,X0)
& ! [X3] :
( ordinal_subset(X2,X3)
| ~ in(X3,X0)
| ~ ordinal(X3) )
& ordinal(X2) )
| ~ ordinal(X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f96,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| ? [X2] :
( in(X2,X0)
& ! [X3] :
( ordinal_subset(X2,X3)
| ~ in(X3,X0)
| ~ ordinal(X3) )
& ordinal(X2) )
| ~ ordinal(X1) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0] :
? [X1] :
( ~ in(X1,X0)
& ordinal(X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f98,plain,
? [X0] :
! [X1] :
( ~ ordinal(X1)
| in(X1,X0)
| ? [X2] :
( ~ ordinal_subset(X1,X2)
& ~ in(X2,X0)
& ordinal(X2) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f99,plain,
? [X0] :
! [X1] :
( ~ ordinal(X1)
| in(X1,X0)
| ? [X2] :
( ~ ordinal_subset(X1,X2)
& ~ in(X2,X0)
& ordinal(X2) ) ),
inference(flattening,[],[f98]) ).
fof(f106,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,[],[f78]) ).
fof(f107,plain,
! [X0] :
( ( epsilon_transitive(X0)
| ? [X1] :
( ~ subset(X1,X0)
& in(X1,X0) ) )
& ( ! [X2] :
( subset(X2,X0)
| ~ in(X2,X0) )
| ~ epsilon_transitive(X0) ) ),
inference(rectify,[],[f106]) ).
fof(f108,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))],[f107]) ).
fof(f109,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,[],[f79]) ).
fof(f110,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,[],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK1(X0,X1),X1)
& in(sK1(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f110]) ).
fof(f126,plain,
! [X0,X1] :
( ( ( ordinal_subset(X0,X1)
| ~ subset(X0,X1) )
& ( subset(X0,X1)
| ~ ordinal_subset(X0,X1) ) )
| ~ ordinal(X0)
| ~ ordinal(X1) ),
inference(nnf_transformation,[],[f86]) ).
fof(f127,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,succ(X1))
| in(X3,X0) )
& ( ( in(X3,succ(X1))
& ~ in(X3,X0) )
| ~ in(X3,X2) ) )
| ~ ordinal(X1) ),
inference(nnf_transformation,[],[f89]) ).
fof(f128,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ~ in(X3,succ(X1))
| in(X3,X0) )
& ( ( in(X3,succ(X1))
& ~ in(X3,X0) )
| ~ in(X3,X2) ) )
| ~ ordinal(X1) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( ! [X3] :
( ( in(X3,sK16(X0,X1))
| ~ in(X3,succ(X1))
| in(X3,X0) )
& ( ( in(X3,succ(X1))
& ~ in(X3,X0) )
| ~ in(X3,sK16(X0,X1)) ) )
| ~ ordinal(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X2,sK16(X0,X1))],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| ( in(sK17(X0),X0)
& ! [X3] :
( ordinal_subset(sK17(X0),X3)
| ~ in(X3,X0)
| ~ ordinal(X3) )
& ordinal(sK17(X0)) )
| ~ ordinal(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X2,sK17(X0))],[f96]) ).
fof(f131,plain,
! [X0] :
( ~ in(sK18(X0),X0)
& ordinal(sK18(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X1,sK18(X0))],[f97]) ).
fof(f132,plain,
! [X1] :
( ~ ordinal(X1)
| in(X1,sK19)
| ( ~ ordinal_subset(X1,sK20(X1))
& ~ in(sK20(X1),sK19)
& ordinal(sK20(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X0,sK19),skolemize(X2,sK20(X1))],[f99]) ).
fof(f134,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f137,plain,
! [X0] :
( ~ ordinal(X0)
| epsilon_transitive(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f147,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f148,plain,
! [X2,X0] :
( ~ in(X2,X0)
| subset(X2,X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f151,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f152,plain,
! [X0,X1] :
( in(sK1(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f153,plain,
! [X0,X1] :
( ~ in(sK1(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f167,plain,
! [X0] :
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f207,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ordinal_subset(X0,X1)
| ~ ordinal(X0)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f210,plain,
! [X3,X0,X1] :
( ~ in(X3,sK16(X0,X1))
| ~ in(X3,X0)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f211,plain,
! [X3,X0,X1] :
( in(X3,succ(X1))
| ~ in(X3,sK16(X0,X1))
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f212,plain,
! [X3,X0,X1] :
( in(X3,sK16(X0,X1))
| ~ in(X3,succ(X1))
| in(X3,X0)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f129]) ).
fof(f213,plain,
! [X0] : in(X0,succ(X0)),
inference(cnf_transformation,[],[f41]) ).
fof(f216,plain,
! [X0,X1] :
( in(X1,X0)
| in(X0,X1)
| X0 = X1
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[],[f92]) ).
fof(f218,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| ordinal(sK17(X0))
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f219,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| ordinal_subset(sK17(X0),X3)
| ~ in(X3,X0)
| ~ ordinal(X3)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f220,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = X0
| in(sK17(X0),X0)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f221,plain,
! [X0] : ordinal(sK18(X0)),
inference(cnf_transformation,[],[f131]) ).
fof(f222,plain,
! [X0] : ~ in(sK18(X0),X0),
inference(cnf_transformation,[],[f131]) ).
fof(f223,plain,
! [X1] :
( in(X1,sK19)
| ~ ordinal(X1)
| ordinal(sK20(X1)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f224,plain,
! [X1] :
( ~ in(sK20(X1),sK19)
| in(X1,sK19)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f132]) ).
fof(f225,plain,
! [X1] :
( ~ ordinal_subset(X1,sK20(X1))
| in(X1,sK19)
| ~ ordinal(X1) ),
inference(cnf_transformation,[],[f132]) ).
fof(f237,plain,
! [X0] :
( ordinal(set_union2(X0,singleton(X0)))
| ~ ordinal(X0) ),
inference(definition_unfolding,[],[f167,f147]) ).
fof(f238,plain,
! [X3,X0,X1] :
( ~ in(X3,set_union2(X1,singleton(X1)))
| in(X3,sK16(X0,X1))
| in(X3,X0)
| ~ ordinal(X1) ),
inference(definition_unfolding,[],[f212,f147]) ).
fof(f239,plain,
! [X3,X0,X1] :
( ~ in(X3,sK16(X0,X1))
| in(X3,set_union2(X1,singleton(X1)))
| ~ ordinal(X1) ),
inference(definition_unfolding,[],[f211,f147]) ).
fof(f240,plain,
! [X0] : in(X0,set_union2(X0,singleton(X0))),
inference(definition_unfolding,[],[f213,f147]) ).
fof(f254,plain,
! [X0,X1] :
( in(X0,sK16(X1,X0))
| in(X0,X1)
| ~ ordinal(X0) ),
inference(resolution,[],[f238,f240]) ).
fof(f258,plain,
( ~ ordinal(sK18(sK19))
| ordinal(sK20(sK18(sK19))) ),
inference(resolution,[],[f223,f222]) ).
fof(f261,plain,
ordinal(sK20(sK18(sK19))),
inference(forward_subsumption_resolution,[],[f258,f221]) ).
fof(f281,plain,
! [X0,X1] :
( in(X1,X0)
| X0 = X1
| ~ ordinal(X1)
| ~ ordinal(X0)
| subset(X0,X1)
| ~ epsilon_transitive(X1) ),
inference(resolution,[],[f216,f148]) ).
fof(f291,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 = X1
| ~ ordinal(X1)
| ~ ordinal(X0)
| in(X1,X0) ),
inference(forward_subsumption_resolution,[],[f281,f137]) ).
fof(f314,plain,
! [X2,X0,X1] :
( ~ in(X2,X0)
| ~ ordinal(X1)
| ~ ordinal(X0)
| in(X1,X0)
| X0 = X1
| in(X2,X1) ),
inference(resolution,[],[f291,f151]) ).
fof(f315,plain,
! [X0,X1] :
( X0 = X1
| ~ ordinal(X1)
| ~ ordinal(X0)
| in(X1,X0)
| ordinal_subset(X0,X1)
| ~ ordinal(X0)
| ~ ordinal(X1) ),
inference(resolution,[],[f291,f207]) ).
fof(f316,plain,
! [X0,X1] :
( ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0)
| in(X1,X0)
| X0 = X1 ),
inference(duplicate_literal_removal,[],[f315]) ).
fof(f318,plain,
! [X0] :
( ~ ordinal(sK20(X0))
| ~ ordinal(X0)
| in(sK20(X0),X0)
| sK20(X0) = X0
| in(X0,sK19)
| ~ ordinal(X0) ),
inference(resolution,[],[f316,f225]) ).
fof(f321,plain,
! [X0] :
( ~ ordinal(sK20(X0))
| ~ ordinal(X0)
| in(sK20(X0),X0)
| sK20(X0) = X0
| in(X0,sK19) ),
inference(duplicate_literal_removal,[],[f318]) ).
fof(f322,plain,
! [X0] :
( in(sK20(X0),X0)
| ~ ordinal(X0)
| sK20(X0) = X0
| in(X0,sK19) ),
inference(forward_subsumption_resolution,[],[f321,f223]) ).
fof(f325,plain,
! [X0,X1] :
( ~ ordinal(set_union2(X0,singleton(X0)))
| set_union2(X0,singleton(X0)) = sK20(set_union2(X0,singleton(X0)))
| in(set_union2(X0,singleton(X0)),sK19)
| in(sK20(set_union2(X0,singleton(X0))),sK16(X1,X0))
| in(sK20(set_union2(X0,singleton(X0))),X1)
| ~ ordinal(X0) ),
inference(resolution,[],[f322,f238]) ).
fof(f328,plain,
! [X0,X1] :
( in(sK20(set_union2(X0,singleton(X0))),sK16(X1,X0))
| in(set_union2(X0,singleton(X0)),sK19)
| set_union2(X0,singleton(X0)) = sK20(set_union2(X0,singleton(X0)))
| in(sK20(set_union2(X0,singleton(X0))),X1)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f325,f237]) ).
fof(f343,plain,
! [X2,X0,X1] :
( in(sK1(sK16(X0,X1),X2),set_union2(X1,singleton(X1)))
| ~ ordinal(X1)
| subset(sK16(X0,X1),X2) ),
inference(resolution,[],[f239,f152]) ).
fof(f450,plain,
! [X0,X1] :
( ~ ordinal(X0)
| subset(sK16(X1,X0),set_union2(X0,singleton(X0)))
| subset(sK16(X1,X0),set_union2(X0,singleton(X0))) ),
inference(resolution,[],[f343,f153]) ).
fof(f456,plain,
! [X0,X1] :
( subset(sK16(X1,X0),set_union2(X0,singleton(X0)))
| ~ ordinal(X0) ),
inference(duplicate_literal_removal,[],[f450]) ).
fof(f555,plain,
! [X0,X1] :
( ~ ordinal(X0)
| empty_set = sK16(X1,X0)
| ordinal(sK17(sK16(X1,X0)))
| ~ ordinal(set_union2(X0,singleton(X0))) ),
inference(resolution,[],[f456,f218]) ).
fof(f556,plain,
! [X2,X0,X1] :
( ~ ordinal(X0)
| empty_set = sK16(X1,X0)
| ordinal_subset(sK17(sK16(X1,X0)),X2)
| ~ in(X2,sK16(X1,X0))
| ~ ordinal(X2)
| ~ ordinal(set_union2(X0,singleton(X0))) ),
inference(resolution,[],[f456,f219]) ).
fof(f557,plain,
! [X0,X1] :
( ~ ordinal(X0)
| empty_set = sK16(X1,X0)
| in(sK17(sK16(X1,X0)),sK16(X1,X0))
| ~ ordinal(set_union2(X0,singleton(X0))) ),
inference(resolution,[],[f456,f220]) ).
fof(f561,plain,
! [X0,X1] :
( in(sK17(sK16(X1,X0)),sK16(X1,X0))
| empty_set = sK16(X1,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f557,f237]) ).
fof(f562,plain,
! [X2,X0,X1] :
( ordinal_subset(sK17(sK16(X1,X0)),X2)
| empty_set = sK16(X1,X0)
| ~ ordinal(X0)
| ~ in(X2,sK16(X1,X0))
| ~ ordinal(X2) ),
inference(forward_subsumption_resolution,[],[f556,f237]) ).
fof(f563,plain,
! [X0,X1] :
( ordinal(sK17(sK16(X1,X0)))
| empty_set = sK16(X1,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f555,f237]) ).
fof(f564,plain,
! [X0,X1] :
( empty_set = sK16(X0,X1)
| ~ ordinal(X1)
| in(sK17(sK16(X0,X1)),set_union2(X1,singleton(X1)))
| ~ ordinal(X1) ),
inference(resolution,[],[f561,f239]) ).
fof(f565,plain,
! [X0,X1] :
( empty_set = sK16(X0,X1)
| ~ ordinal(X1)
| ~ in(sK17(sK16(X0,X1)),X0)
| ~ ordinal(X1) ),
inference(resolution,[],[f561,f210]) ).
fof(f569,plain,
! [X0,X1] :
( ~ in(sK17(sK16(X0,X1)),X0)
| ~ ordinal(X1)
| empty_set = sK16(X0,X1) ),
inference(duplicate_literal_removal,[],[f565]) ).
fof(f570,plain,
! [X0,X1] :
( in(sK17(sK16(X0,X1)),set_union2(X1,singleton(X1)))
| ~ ordinal(X1)
| empty_set = sK16(X0,X1) ),
inference(duplicate_literal_removal,[],[f564]) ).
fof(f572,plain,
! [X0,X1] :
( ~ ordinal(X0)
| empty_set = sK16(X1,X0)
| ~ in(set_union2(X0,singleton(X0)),sK17(sK16(X1,X0))) ),
inference(resolution,[],[f570,f134]) ).
fof(f587,plain,
! [X0] :
( ~ ordinal(X0)
| empty_set = sK16(set_union2(X0,singleton(X0)),X0)
| ~ ordinal(X0)
| empty_set = sK16(set_union2(X0,singleton(X0)),X0) ),
inference(resolution,[],[f569,f570]) ).
fof(f593,plain,
! [X0] :
( ~ ordinal(X0)
| empty_set = sK16(sK19,X0)
| ~ ordinal(sK17(sK16(sK19,X0)))
| ordinal(sK20(sK17(sK16(sK19,X0)))) ),
inference(resolution,[],[f569,f223]) ).
fof(f594,plain,
! [X0] :
( ~ ordinal(X0)
| empty_set = sK16(set_union2(X0,singleton(X0)),X0) ),
inference(duplicate_literal_removal,[],[f587]) ).
fof(f596,plain,
! [X0] :
( ordinal(sK20(sK17(sK16(sK19,X0))))
| empty_set = sK16(sK19,X0)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[],[f593,f563]) ).
fof(f730,plain,
empty_set = sK16(set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))),sK20(sK18(sK19))),
inference(resolution,[],[f594,f261]) ).
fof(f732,plain,
! [X0] :
( ~ in(X0,empty_set)
| ~ in(X0,set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))))
| ~ ordinal(sK20(sK18(sK19))) ),
inference(superposition,[],[f210,f730]) ).
fof(f733,plain,
! [X0] :
( ~ in(X0,empty_set)
| in(X0,set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))))
| ~ ordinal(sK20(sK18(sK19))) ),
inference(superposition,[],[f239,f730]) ).
fof(f758,plain,
! [X0] :
( in(X0,set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))))
| ~ in(X0,empty_set) ),
inference(forward_subsumption_resolution,[],[f733,f261]) ).
fof(f759,plain,
! [X0] :
( ~ in(X0,empty_set)
| ~ in(X0,set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19))))) ),
inference(forward_subsumption_resolution,[],[f732,f261]) ).
fof(f779,plain,
! [X0] : ~ in(X0,empty_set),
inference(forward_subsumption_resolution,[],[f759,f758]) ).
fof(f980,plain,
! [X0,X1] :
( empty_set = sK16(X0,X1)
| ~ ordinal(X1)
| ~ in(sK20(sK17(sK16(X0,X1))),sK16(X0,X1))
| ~ ordinal(sK20(sK17(sK16(X0,X1))))
| in(sK17(sK16(X0,X1)),sK19)
| ~ ordinal(sK17(sK16(X0,X1))) ),
inference(resolution,[],[f562,f225]) ).
fof(f984,plain,
! [X0,X1] :
( ~ in(sK20(sK17(sK16(X0,X1))),sK16(X0,X1))
| ~ ordinal(X1)
| empty_set = sK16(X0,X1)
| ~ ordinal(sK20(sK17(sK16(X0,X1))))
| in(sK17(sK16(X0,X1)),sK19) ),
inference(forward_subsumption_resolution,[],[f980,f563]) ).
fof(f1581,plain,
! [X0,X1] :
( ~ ordinal(X0)
| ~ ordinal(X1)
| in(X0,X1)
| X0 = X1
| in(sK20(X1),X0)
| ~ ordinal(X1)
| sK20(X1) = X1
| in(X1,sK19) ),
inference(resolution,[],[f314,f322]) ).
fof(f1591,plain,
! [X0,X1] :
( in(sK20(X1),X0)
| ~ ordinal(X1)
| in(X0,X1)
| X0 = X1
| ~ ordinal(X0)
| sK20(X1) = X1
| in(X1,sK19) ),
inference(duplicate_literal_removal,[],[f1581]) ).
fof(f1623,plain,
! [X2,X0,X1] :
( ~ ordinal(X0)
| in(set_union2(X1,singleton(X1)),X0)
| set_union2(X1,singleton(X1)) = X0
| ~ ordinal(set_union2(X1,singleton(X1)))
| sK20(X0) = X0
| in(X0,sK19)
| in(sK20(X0),sK16(X2,X1))
| in(sK20(X0),X2)
| ~ ordinal(X1) ),
inference(resolution,[],[f1591,f238]) ).
fof(f1633,plain,
! [X2,X0,X1] :
( in(sK20(X0),sK16(X2,X1))
| in(set_union2(X1,singleton(X1)),X0)
| set_union2(X1,singleton(X1)) = X0
| sK20(X0) = X0
| in(X0,sK19)
| ~ ordinal(X0)
| in(sK20(X0),X2)
| ~ ordinal(X1) ),
inference(forward_subsumption_resolution,[],[f1623,f237]) ).
fof(f1640,plain,
! [X0,X1] :
( in(set_union2(X1,singleton(X1)),sK17(sK16(X0,X1)))
| set_union2(X1,singleton(X1)) = sK17(sK16(X0,X1))
| sK17(sK16(X0,X1)) = sK20(sK17(sK16(X0,X1)))
| in(sK17(sK16(X0,X1)),sK19)
| ~ ordinal(sK17(sK16(X0,X1)))
| in(sK20(sK17(sK16(X0,X1))),X0)
| ~ ordinal(X1)
| ~ ordinal(X1)
| empty_set = sK16(X0,X1)
| ~ ordinal(sK20(sK17(sK16(X0,X1))))
| in(sK17(sK16(X0,X1)),sK19) ),
inference(resolution,[],[f1633,f984]) ).
fof(f1668,plain,
! [X0,X1] :
( in(set_union2(X1,singleton(X1)),sK17(sK16(X0,X1)))
| set_union2(X1,singleton(X1)) = sK17(sK16(X0,X1))
| sK17(sK16(X0,X1)) = sK20(sK17(sK16(X0,X1)))
| in(sK17(sK16(X0,X1)),sK19)
| ~ ordinal(sK17(sK16(X0,X1)))
| in(sK20(sK17(sK16(X0,X1))),X0)
| ~ ordinal(X1)
| empty_set = sK16(X0,X1)
| ~ ordinal(sK20(sK17(sK16(X0,X1)))) ),
inference(duplicate_literal_removal,[],[f1640]) ).
fof(f1674,plain,
! [X0,X1] :
( in(set_union2(X1,singleton(X1)),sK17(sK16(X0,X1)))
| set_union2(X1,singleton(X1)) = sK17(sK16(X0,X1))
| sK17(sK16(X0,X1)) = sK20(sK17(sK16(X0,X1)))
| in(sK17(sK16(X0,X1)),sK19)
| ~ ordinal(sK17(sK16(X0,X1)))
| in(sK20(sK17(sK16(X0,X1))),X0)
| ~ ordinal(X1)
| empty_set = sK16(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1668,f223]) ).
fof(f1679,plain,
! [X0,X1] :
( set_union2(X1,singleton(X1)) = sK17(sK16(X0,X1))
| sK17(sK16(X0,X1)) = sK20(sK17(sK16(X0,X1)))
| in(sK17(sK16(X0,X1)),sK19)
| ~ ordinal(sK17(sK16(X0,X1)))
| in(sK20(sK17(sK16(X0,X1))),X0)
| ~ ordinal(X1)
| empty_set = sK16(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1674,f572]) ).
fof(f1682,plain,
! [X0,X1] :
( in(sK20(sK17(sK16(X0,X1))),X0)
| sK17(sK16(X0,X1)) = sK20(sK17(sK16(X0,X1)))
| in(sK17(sK16(X0,X1)),sK19)
| set_union2(X1,singleton(X1)) = sK17(sK16(X0,X1))
| ~ ordinal(X1)
| empty_set = sK16(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1679,f563]) ).
fof(f2380,plain,
! [X0] :
( sK17(sK16(sK19,X0)) = sK20(sK17(sK16(sK19,X0)))
| in(sK17(sK16(sK19,X0)),sK19)
| set_union2(X0,singleton(X0)) = sK17(sK16(sK19,X0))
| ~ ordinal(X0)
| empty_set = sK16(sK19,X0)
| in(sK17(sK16(sK19,X0)),sK19)
| ~ ordinal(sK17(sK16(sK19,X0))) ),
inference(resolution,[],[f1682,f224]) ).
fof(f2392,plain,
! [X0] :
( sK17(sK16(sK19,X0)) = sK20(sK17(sK16(sK19,X0)))
| in(sK17(sK16(sK19,X0)),sK19)
| set_union2(X0,singleton(X0)) = sK17(sK16(sK19,X0))
| ~ ordinal(X0)
| empty_set = sK16(sK19,X0)
| ~ ordinal(sK17(sK16(sK19,X0))) ),
inference(duplicate_literal_removal,[],[f2380]) ).
fof(f2393,plain,
! [X0] :
( sK17(sK16(sK19,X0)) = sK20(sK17(sK16(sK19,X0)))
| set_union2(X0,singleton(X0)) = sK17(sK16(sK19,X0))
| ~ ordinal(X0)
| empty_set = sK16(sK19,X0)
| ~ ordinal(sK17(sK16(sK19,X0))) ),
inference(forward_subsumption_resolution,[],[f2392,f569]) ).
fof(f2394,plain,
! [X0] :
( ~ ordinal(X0)
| set_union2(X0,singleton(X0)) = sK17(sK16(sK19,X0))
| sK17(sK16(sK19,X0)) = sK20(sK17(sK16(sK19,X0)))
| empty_set = sK16(sK19,X0) ),
inference(forward_subsumption_resolution,[],[f2393,f563]) ).
fof(f2403,plain,
( set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))) = sK17(sK16(sK19,sK20(sK18(sK19))))
| sK17(sK16(sK19,sK20(sK18(sK19)))) = sK20(sK17(sK16(sK19,sK20(sK18(sK19)))))
| empty_set = sK16(sK19,sK20(sK18(sK19))) ),
inference(resolution,[],[f2394,f261]) ).
fof(f2407,definition,
( spl21_47
<=> empty_set = sK16(sK19,sK20(sK18(sK19))) ),
introduced(definition,[new_symbols(definition,[spl21_47])],[avatar_definition]) ).
fof(f2408,plain,
( empty_set != sK16(sK19,sK20(sK18(sK19)))
| spl21_47 ),
inference(avatar_component_clause,[],[f2407]) ).
fof(f2409,plain,
( empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_47 ),
inference(avatar_component_clause,[],[f2407]) ).
fof(f2411,definition,
( spl21_48
<=> sK17(sK16(sK19,sK20(sK18(sK19)))) = sK20(sK17(sK16(sK19,sK20(sK18(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl21_48])],[avatar_definition]) ).
fof(f2412,plain,
( sK17(sK16(sK19,sK20(sK18(sK19)))) != sK20(sK17(sK16(sK19,sK20(sK18(sK19)))))
| spl21_48 ),
inference(avatar_component_clause,[],[f2411]) ).
fof(f2413,plain,
( sK17(sK16(sK19,sK20(sK18(sK19)))) = sK20(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ spl21_48 ),
inference(avatar_component_clause,[],[f2411]) ).
fof(f2429,plain,
( in(sK20(sK18(sK19)),empty_set)
| in(sK20(sK18(sK19)),sK19)
| ~ ordinal(sK20(sK18(sK19)))
| ~ spl21_47 ),
inference(superposition,[],[f254,f2409]) ).
fof(f2461,plain,
( in(sK20(sK18(sK19)),sK19)
| ~ ordinal(sK20(sK18(sK19)))
| ~ spl21_47 ),
inference(forward_subsumption_resolution,[],[f2429,f779]) ).
fof(f2472,plain,
( in(sK20(sK18(sK19)),sK19)
| ~ spl21_47 ),
inference(forward_subsumption_resolution,[],[f2461,f261]) ).
fof(f2493,plain,
( in(sK18(sK19),sK19)
| ~ ordinal(sK18(sK19))
| ~ spl21_47 ),
inference(resolution,[],[f2472,f224]) ).
fof(f2500,plain,
( ~ ordinal(sK18(sK19))
| ~ spl21_47 ),
inference(forward_subsumption_resolution,[],[f2493,f222]) ).
fof(f2501,plain,
( $false
| ~ spl21_47 ),
inference(forward_subsumption_resolution,[],[f2500,f221]) ).
fof(f2502,plain,
~ spl21_47,
inference(avatar_contradiction_clause,[],[f2501]) ).
fof(f2505,plain,
( ~ in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK16(sK19,sK20(sK18(sK19))))
| ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| ~ spl21_48 ),
inference(superposition,[],[f984,f2413]) ).
fof(f2514,plain,
( ~ in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK16(sK19,sK20(sK18(sK19))))
| ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ spl21_48 ),
inference(forward_subsumption_resolution,[],[f2505,f210]) ).
fof(f2517,definition,
( spl21_52
<=> ordinal(sK17(sK16(sK19,sK20(sK18(sK19))))) ),
introduced(definition,[new_symbols(definition,[spl21_52])],[avatar_definition]) ).
fof(f2518,plain,
( ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ spl21_52 ),
inference(avatar_component_clause,[],[f2517]) ).
fof(f2521,definition,
( spl21_53
<=> in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19) ),
introduced(definition,[new_symbols(definition,[spl21_53])],[avatar_definition]) ).
fof(f2522,plain,
( ~ in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| spl21_53 ),
inference(avatar_component_clause,[],[f2521]) ).
fof(f2523,plain,
( in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| ~ spl21_53 ),
inference(avatar_component_clause,[],[f2521]) ).
fof(f2526,plain,
( ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ spl21_48 ),
inference(forward_subsumption_resolution,[],[f2514,f561]) ).
fof(f2533,plain,
( ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_48 ),
inference(forward_subsumption_resolution,[],[f2526,f563]) ).
fof(f2535,plain,
( empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_48 ),
inference(forward_subsumption_resolution,[],[f2533,f261]) ).
fof(f2537,plain,
( $false
| spl21_47
| ~ spl21_48 ),
inference(forward_subsumption_resolution,[],[f2535,f2408]) ).
fof(f2538,plain,
( spl21_47
| ~ spl21_48 ),
inference(avatar_contradiction_clause,[],[f2537]) ).
fof(f2618,plain,
( set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))) = sK17(sK16(sK19,sK20(sK18(sK19))))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| spl21_48 ),
inference(forward_subsumption_resolution,[],[f2403,f2412]) ).
fof(f2619,plain,
( set_union2(sK20(sK18(sK19)),singleton(sK20(sK18(sK19)))) = sK17(sK16(sK19,sK20(sK18(sK19))))
| spl21_47
| spl21_48 ),
inference(forward_subsumption_resolution,[],[f2618,f2408]) ).
fof(f2627,plain,
( ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ ordinal(sK20(sK18(sK19)))
| spl21_47
| spl21_48 ),
inference(superposition,[],[f237,f2619]) ).
fof(f2632,plain,
( ! [X0] :
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK16(X0,sK20(sK18(sK19))))
| in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| sK17(sK16(sK19,sK20(sK18(sK19)))) = sK20(sK17(sK16(sK19,sK20(sK18(sK19)))))
| in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),X0)
| ~ ordinal(sK20(sK18(sK19))) )
| spl21_47
| spl21_48 ),
inference(superposition,[],[f328,f2619]) ).
fof(f2702,plain,
( ! [X0] :
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK16(X0,sK20(sK18(sK19))))
| in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),X0)
| ~ ordinal(sK20(sK18(sK19))) )
| spl21_47
| spl21_48 ),
inference(forward_subsumption_resolution,[],[f2632,f2412]) ).
fof(f2706,plain,
( ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| spl21_47
| spl21_48 ),
inference(forward_subsumption_resolution,[],[f2627,f261]) ).
fof(f2735,plain,
( ! [X0] :
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK16(X0,sK20(sK18(sK19))))
| in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),X0) )
| spl21_47
| spl21_48 ),
inference(forward_subsumption_resolution,[],[f2702,f261]) ).
fof(f2736,plain,
( spl21_52
| spl21_47
| spl21_48 ),
inference(avatar_split_clause,[],[f2706,f2411,f2407,f2517]) ).
fof(f2747,definition,
( spl21_66
<=> ! [X0] :
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK16(X0,sK20(sK18(sK19))))
| in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_66])],[avatar_definition]) ).
fof(f2748,plain,
( ! [X0] :
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK16(X0,sK20(sK18(sK19))))
| in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),X0) )
| ~ spl21_66 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2749,plain,
( spl21_53
| spl21_66
| spl21_47
| spl21_48 ),
inference(avatar_split_clause,[],[f2735,f2411,f2407,f2747,f2521]) ).
fof(f2751,plain,
( ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_53 ),
inference(resolution,[],[f2523,f569]) ).
fof(f2760,plain,
( empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_53 ),
inference(forward_subsumption_resolution,[],[f2751,f261]) ).
fof(f2761,plain,
( $false
| spl21_47
| ~ spl21_53 ),
inference(forward_subsumption_resolution,[],[f2760,f2408]) ).
fof(f2762,plain,
( spl21_47
| ~ spl21_53 ),
inference(avatar_contradiction_clause,[],[f2761]) ).
fof(f2801,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ ordinal(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))))
| in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| ~ spl21_66 ),
inference(resolution,[],[f2748,f984]) ).
fof(f2815,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ ordinal(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))))
| ~ spl21_66 ),
inference(forward_subsumption_resolution,[],[f2801,f569]) ).
fof(f2819,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| ~ ordinal(sK20(sK18(sK19)))
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_66 ),
inference(forward_subsumption_resolution,[],[f2815,f596]) ).
fof(f2821,definition,
( spl21_67
<=> in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19) ),
introduced(definition,[new_symbols(definition,[spl21_67])],[avatar_definition]) ).
fof(f2823,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| ~ spl21_67 ),
inference(avatar_component_clause,[],[f2821]) ).
fof(f2825,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| empty_set = sK16(sK19,sK20(sK18(sK19)))
| ~ spl21_66 ),
inference(forward_subsumption_resolution,[],[f2819,f261]) ).
fof(f2826,plain,
( in(sK20(sK17(sK16(sK19,sK20(sK18(sK19))))),sK19)
| spl21_47
| ~ spl21_66 ),
inference(forward_subsumption_resolution,[],[f2825,f2408]) ).
fof(f2827,plain,
( spl21_67
| spl21_47
| ~ spl21_66 ),
inference(avatar_split_clause,[],[f2826,f2747,f2407,f2821]) ).
fof(f2837,plain,
( in(sK17(sK16(sK19,sK20(sK18(sK19)))),sK19)
| ~ ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| ~ spl21_67 ),
inference(resolution,[],[f2823,f224]) ).
fof(f2844,plain,
( ~ ordinal(sK17(sK16(sK19,sK20(sK18(sK19)))))
| spl21_53
| ~ spl21_67 ),
inference(forward_subsumption_resolution,[],[f2837,f2522]) ).
fof(f2845,plain,
( $false
| ~ spl21_52
| spl21_53
| ~ spl21_67 ),
inference(forward_subsumption_resolution,[],[f2844,f2518]) ).
fof(f2846,plain,
( ~ spl21_52
| spl21_53
| ~ spl21_67 ),
inference(avatar_contradiction_clause,[],[f2845]) ).
cnf(s56,plain,
~ spl21_47,
inference(sat_conversion,[],[f2502]) ).
cnf(s60,plain,
( spl21_47
| ~ spl21_48 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s74,plain,
( spl21_47
| spl21_48
| spl21_52 ),
inference(sat_conversion,[],[f2736]) ).
cnf(s77,plain,
( spl21_47
| spl21_48
| spl21_53
| spl21_66 ),
inference(sat_conversion,[],[f2749]) ).
cnf(s78,plain,
( spl21_47
| ~ spl21_53 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s88,plain,
( spl21_47
| ~ spl21_66
| spl21_67 ),
inference(sat_conversion,[],[f2827]) ).
cnf(s89,plain,
( ~ spl21_52
| spl21_53
| ~ spl21_67 ),
inference(sat_conversion,[],[f2846]) ).
cnf(s93,plain,
~ spl21_53,
inference(rat,[],[s78,s56]) ).
cnf(s94,plain,
~ spl21_48,
inference(rat,[],[s60,s56]) ).
cnf(s96,plain,
spl21_66,
inference(rat,[],[s77,s56,s93,s94]) ).
cnf(s98,plain,
spl21_52,
inference(rat,[],[s74,s56,s94]) ).
cnf(s99,plain,
spl21_67,
inference(rat,[],[s88,s56,s96]) ).
cnf(s100,plain,
$false,
inference(rat,[],[s89,s93,s99,s98]) ).
fof(f2847,plain,
$false,
inference(avatar_sat_refutation,[],[s100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM406+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n014.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 19:48:19 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.85/2.14 % (1123577)Detected formulas, will run a generic FOF schedule.
% 10.85/2.14 % (1123587)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2971920174:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.85/2.14 % (1123582)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=2524865039:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.85/2.14 % (1123588)dis-21_1_sil=8000:lcm=predicate:random_seed=2527330143: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)
% 10.85/2.14 % (1123586)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2290638376:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.85/2.14 % (1123584)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=1943889876:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.85/2.14 % (1123583)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=1348700153:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.85/2.14 % (1123585)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2436101395:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.85/2.14 % (1123585)Refutation not found, incomplete strategy
% 10.85/2.14 % (1123585)------------------------------
% 10.85/2.14 % (1123585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.14 % (1123585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.14 % (1123585)CaDiCaL version: 2.1.3
% 10.85/2.14 % (1123585)Termination reason: Refutation not found, incomplete strategy
% 10.85/2.14 % (1123585)Time elapsed: 0.002 s
% 10.85/2.14 % (1123585)Peak memory usage: 88 MB
% 10.85/2.14 % (1123585)Instructions burned: 2 (million)
% 10.85/2.14 % (1123586)Instruction limit reached!
% 10.85/2.14 % (1123586)------------------------------
% 10.85/2.14 % (1123586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.14 % (1123586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.14 % (1123586)CaDiCaL version: 2.1.3
% 10.85/2.14 % (1123586)Termination reason: Instruction limit
% 10.85/2.14 % (1123586)Termination phase: Saturation
% 10.85/2.14 % (1123586)Time elapsed: 0.068 s
% 10.85/2.14 % (1123586)Peak memory usage: 88 MB
% 10.85/2.14 % (1123586)Instructions burned: 121 (million)
% 10.85/2.14 % (1123587)Instruction limit reached!
% 10.85/2.14 % (1123587)------------------------------
% 10.85/2.14 % (1123587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.14 % (1123587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.14 % (1123587)CaDiCaL version: 2.1.3
% 10.85/2.14 % (1123587)Termination reason: Instruction limit
% 10.85/2.14 % (1123587)Termination phase: Saturation
% 10.85/2.14 % (1123587)Time elapsed: 0.072 s
% 10.85/2.14 % (1123587)Peak memory usage: 89 MB
% 10.85/2.14 % (1123587)Instructions burned: 141 (million)
% 10.85/2.14 % (1123588)Instruction limit reached!
% 10.85/2.14 % (1123588)------------------------------
% 10.85/2.14 % (1123588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.85/2.14 % (1123588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.14 % (1123588)CaDiCaL version: 2.1.3
% 10.85/2.14 % (1123588)Termination reason: Instruction limit
% 10.85/2.14 % (1123588)Termination phase: Saturation
% 10.85/2.14 % (1123588)Time elapsed: 0.076 s
% 10.85/2.14 % (1123588)Peak memory usage: 90 MB
% 10.85/2.14 % (1123588)Instructions burned: 130 (million)
% 10.85/2.14 % (1123596)lrs+10_1_sil=8000:sp=occurrence:random_seed=3111677119:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.85/2.14 % (1123598)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2520790648:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.85/2.14 % (1123597)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1780007264:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.85/2.14 % (1123585)------------------------------
% 10.85/2.14 % (1123585)------------------------------
% 10.85/2.14 % (1123596)Instruction limit reached!
% 10.85/2.14 % (1123596)------------------------------
% 10.85/2.14 % (1123596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123596)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123596)Termination reason: Instruction limit
% 11.87/2.35 % (1123596)Termination phase: Saturation
% 11.87/2.35 % (1123596)Time elapsed: 0.093 s
% 11.87/2.35 % (1123596)Peak memory usage: 91 MB
% 11.87/2.35 % (1123596)Instructions burned: 288 (million)
% 11.87/2.35 % (1123597)Instruction limit reached!
% 11.87/2.35 % (1123597)------------------------------
% 11.87/2.35 % (1123597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123597)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123597)Termination reason: Instruction limit
% 11.87/2.35 % (1123597)Termination phase: Saturation
% 11.87/2.35 % (1123597)Time elapsed: 0.080 s
% 11.87/2.35 % (1123597)Peak memory usage: 89 MB
% 11.87/2.35 % (1123597)Instructions burned: 158 (million)
% 11.87/2.35 % (1123603)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=701706255:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 11.87/2.35 % (1123602)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=3889186374:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 11.87/2.35 % (1123604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2099307677:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 11.87/2.35 % (1123598)Instruction limit reached!
% 11.87/2.35 % (1123598)------------------------------
% 11.87/2.35 % (1123598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123598)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123598)Termination reason: Instruction limit
% 11.87/2.35 % (1123598)Termination phase: Saturation
% 11.87/2.35 % (1123598)Time elapsed: 0.217 s
% 11.87/2.35 % (1123598)Peak memory usage: 91 MB
% 11.87/2.35 % (1123598)Instructions burned: 326 (million)
% 11.87/2.35 % (1123603)Instruction limit reached!
% 11.87/2.35 % (1123603)------------------------------
% 11.87/2.35 % (1123603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123603)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123603)Termination reason: Instruction limit
% 11.87/2.35 % (1123603)Termination phase: Saturation
% 11.87/2.35 % (1123603)Time elapsed: 0.088 s
% 11.87/2.35 % (1123603)Peak memory usage: 89 MB
% 11.87/2.35 % (1123603)Instructions burned: 296 (million)
% 11.87/2.35 % (1123602)Instruction limit reached!
% 11.87/2.35 % (1123602)------------------------------
% 11.87/2.35 % (1123602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123602)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123602)Termination reason: Instruction limit
% 11.87/2.35 % (1123602)Termination phase: Saturation
% 11.87/2.35 % (1123602)Time elapsed: 0.141 s
% 11.87/2.35 % (1123602)Peak memory usage: 95 MB
% 11.87/2.35 % (1123602)Instructions burned: 248 (million)
% 11.87/2.35 % (1123609)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3081842624:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 11.87/2.35 % (1123609)Instruction limit reached!
% 11.87/2.35 % (1123609)------------------------------
% 11.87/2.35 % (1123609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123609)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123609)Termination reason: Instruction limit
% 11.87/2.35 % (1123609)Termination phase: Saturation
% 11.87/2.35 % (1123609)Time elapsed: 0.036 s
% 11.87/2.35 % (1123609)Peak memory usage: 89 MB
% 11.87/2.35 % (1123609)Instructions burned: 129 (million)
% 11.87/2.35 % (1123608)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4190326162:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 11.87/2.35 % (1123608)Instruction limit reached!
% 11.87/2.35 % (1123608)------------------------------
% 11.87/2.35 % (1123608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123608)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123608)Termination reason: Instruction limit
% 11.87/2.35 % (1123608)Termination phase: Saturation
% 11.87/2.35 % (1123608)Time elapsed: 0.080 s
% 11.87/2.35 % (1123608)Peak memory usage: 90 MB
% 11.87/2.35 % (1123608)Instructions burned: 114 (million)
% 11.87/2.35 % (1123611)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1496625267:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 11.87/2.35 % (1123612)lrs+10_1_sil=8000:sp=occurrence:random_seed=231318822:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 11.87/2.35 % (1123611)Instruction limit reached!
% 11.87/2.35 % (1123611)------------------------------
% 11.87/2.35 % (1123611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123611)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123611)Termination reason: Instruction limit
% 11.87/2.35 % (1123611)Termination phase: Saturation
% 11.87/2.35 % (1123611)Time elapsed: 0.063 s
% 11.87/2.35 % (1123611)Peak memory usage: 89 MB
% 11.87/2.35 % (1123611)Instructions burned: 114 (million)
% 11.87/2.35 % (1123614)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2492609406:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 11.87/2.35 % (1123617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=546754197:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 11.87/2.35 % (1123612)Instruction limit reached!
% 11.87/2.35 % (1123612)------------------------------
% 11.87/2.35 % (1123612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123612)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123612)Termination reason: Instruction limit
% 11.87/2.35 % (1123612)Termination phase: Saturation
% 11.87/2.35 % (1123612)Time elapsed: 0.295 s
% 11.87/2.35 % (1123612)Peak memory usage: 96 MB
% 11.87/2.35 % (1123612)Instructions burned: 910 (million)
% 11.87/2.35 % (1123614)Instruction limit reached!
% 11.87/2.35 % (1123614)------------------------------
% 11.87/2.35 % (1123614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123614)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123614)Termination reason: Instruction limit
% 11.87/2.35 % (1123614)Termination phase: Saturation
% 11.87/2.35 % (1123614)Time elapsed: 0.240 s
% 11.87/2.35 % (1123614)Peak memory usage: 90 MB
% 11.87/2.35 % (1123614)Instructions burned: 438 (million)
% 11.87/2.35 % (1123620)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3636875716:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 11.87/2.35 % (1123620)Instruction limit reached!
% 11.87/2.35 % (1123620)------------------------------
% 11.87/2.35 % (1123620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123620)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123620)Termination reason: Instruction limit
% 11.87/2.35 % (1123620)Termination phase: Saturation
% 11.87/2.35 % (1123620)Time elapsed: 0.039 s
% 11.87/2.35 % (1123620)Peak memory usage: 93 MB
% 11.87/2.35 % (1123620)Instructions burned: 137 (million)
% 11.87/2.35 % (1123621)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2660678214:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 11.87/2.35 % (1123621)Refutation not found, incomplete strategy
% 11.87/2.35 % (1123621)------------------------------
% 11.87/2.35 % (1123621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/2.35 % (1123621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/2.35 % (1123621)CaDiCaL version: 2.1.3
% 11.87/2.35 % (1123621)Termination reason: Refutation not found, incomplete strategy
% 11.87/2.35 % (1123621)Time elapsed: 0.003 s
% 11.87/2.35 % (1123621)Peak memory usage: 88 MB
% 11.87/2.35 % (1123621)Instructions burned: 3 (million)
% 11.87/2.35 % (1123623)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1842289494:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 11.87/2.35 % (1123604)First to succeed.
% 11.87/2.35 % (1123604)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1123577"
% 11.87/2.35 % (1123621)------------------------------
% 11.87/2.35 % (1123621)------------------------------
% 11.87/2.35 % (1123626)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=2139651840:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 11.87/2.35 % (1123604)Refutation found. Thanks to Tanya!
% 11.87/2.35 % SZS status Theorem for theBenchmark
% 11.87/2.35 % SZS output start Proof for theBenchmark
% See solution above
% 12.43/2.44 % (1123604)------------------------------
% 12.43/2.44 % (1123604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/2.44 % (1123604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/2.44 % (1123604)CaDiCaL version: 2.1.3
% 12.43/2.44 % (1123604)Termination reason: Refutation
% 12.43/2.44 % (1123604)Time elapsed: 0.924 s
% 12.43/2.44 % (1123604)Peak memory usage: 133 MB
% 12.43/2.44 % (1123604)Instructions burned: 1394 (million)
% 12.43/2.44 % (1123604)------------------------------
% 12.43/2.44 % (1123604)------------------------------
% 12.43/2.44 % (1123577)Success in time 1.719 s
% 12.43/2.44 % Vampire exiting
%------------------------------------------------------------------------------