%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU364+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:33 PM UTC 2026
% Result : Theorem 5.48s 1.91s
% Output : Refutation 5.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 17
% Syntax : Number of formulae : 181 ( 20 unt; 13 def)
% Number of atoms : 1000 ( 120 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 1309 ( 490 ~; 575 |; 214 &)
% ( 19 <=>; 9 =>; 0 <=; 2 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 13 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-4 aty)
% Number of variables : 370 ( 0 sgn 263 !; 107 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f413,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f447,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,powerset(X2))
& X5 = X4
& ? [X10] :
( X10 = X4
& ? [X11] :
( element(X11,the_carrier(X0))
& in(X11,X1)
& relstr_set_smaller(X0,X10,X11) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_tarski__e11_2_1__waybel_0__1) ).
fof(f463,conjecture,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e11_2_1__waybel_0__1) ).
fof(f464,negated_conjecture,
~ ! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f463]) ).
fof(f635,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f717,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
=> X4 = X5 )
=> ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,powerset(X2))
& X11 = X12
& ? [X13] :
( X11 = X13
& ? [X14] :
( element(X14,the_carrier(X0))
& in(X14,X1)
& relstr_set_smaller(X0,X13,X14) ) ) ) ) ) ),
inference(rectify,[],[f447]) ).
fof(f1226,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,powerset(X2))
& X11 = X12
& ? [X13] :
( X11 = X13
& ? [X14] :
( element(X14,the_carrier(X0))
& in(X14,X1)
& relstr_set_smaller(X0,X13,X14) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(ennf_transformation,[],[f717]) ).
fof(f1227,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,powerset(X2))
& X11 = X12
& ? [X13] :
( X11 = X13
& ? [X14] :
( element(X14,the_carrier(X0))
& in(X14,X1)
& relstr_set_smaller(X0,X13,X14) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(flattening,[],[f1226]) ).
fof(f1258,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) ) )
& ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) ),
inference(ennf_transformation,[],[f464]) ).
fof(f1259,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) ) )
& ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) ),
inference(flattening,[],[f1258]) ).
fof(f1489,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f635]) ).
fof(f1490,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f1489]) ).
fof(f1598,definition,
! [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
| ~ sP14(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f1599,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,powerset(X2))
& X11 = X12
& ? [X13] :
( X11 = X13
& ? [X14] :
( element(X14,the_carrier(X0))
& in(X14,X1)
& relstr_set_smaller(X0,X13,X14) ) ) ) )
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(definition_folding,[],[f1227,f1598]) ).
fof(f2025,plain,
! [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6] :
( X6 = X4
& ? [X7] :
( element(X7,the_carrier(X0))
& in(X7,X1)
& relstr_set_smaller(X0,X6,X7) ) )
& X3 = X5
& ? [X8] :
( X8 = X5
& ? [X9] :
( element(X9,the_carrier(X0))
& in(X9,X1)
& relstr_set_smaller(X0,X8,X9) ) ) )
| ~ sP14(X0,X1) ),
inference(nnf_transformation,[],[f1598]) ).
fof(f2026,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( X3 = X5
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) )
& X2 = X4
& ? [X7] :
( X4 = X7
& ? [X8] :
( element(X8,the_carrier(X0))
& in(X8,X1)
& relstr_set_smaller(X0,X7,X8) ) ) )
| ~ sP14(X0,X1) ),
inference(rectify,[],[f2025]) ).
fof(f2027,plain,
! [X0,X1] :
( ( sK283(X0,X1) != sK284(X0,X1)
& sK282(X0,X1) = sK283(X0,X1)
& sK283(X0,X1) = sK285(X0,X1)
& element(sK286(X0,X1),the_carrier(X0))
& in(sK286(X0,X1),X1)
& relstr_set_smaller(X0,sK285(X0,X1),sK286(X0,X1))
& sK282(X0,X1) = sK284(X0,X1)
& sK284(X0,X1) = sK287(X0,X1)
& element(sK288(X0,X1),the_carrier(X0))
& in(sK288(X0,X1),X1)
& relstr_set_smaller(X0,sK287(X0,X1),sK288(X0,X1)) )
| ~ sP14(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK282,sK283,sK284,sK285,sK286,sK287,sK288]),skolemize(X2,sK282(X0,X1)),skolemize(X3,sK283(X0,X1)),skolemize(X4,sK284(X0,X1)),skolemize(X5,sK285(X0,X1)),skolemize(X6,sK286(X0,X1)),skolemize(X7,sK287(X0,X1)),skolemize(X8,sK288(X0,X1))],[f2026]) ).
fof(f2028,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( ( in(X11,X10)
| ! [X12] :
( ~ in(X12,powerset(X2))
| X11 != X12
| ! [X13] :
( X11 != X13
| ! [X14] :
( ~ element(X14,the_carrier(X0))
| ~ in(X14,X1)
| ~ relstr_set_smaller(X0,X13,X14) ) ) ) )
& ( ? [X12] :
( in(X12,powerset(X2))
& X11 = X12
& ? [X13] :
( X11 = X13
& ? [X14] :
( element(X14,the_carrier(X0))
& in(X14,X1)
& relstr_set_smaller(X0,X13,X14) ) ) )
| ~ in(X11,X10) ) )
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(nnf_transformation,[],[f1599]) ).
fof(f2029,plain,
! [X0,X1,X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ! [X5] :
( ~ in(X5,powerset(X2))
| X4 != X5
| ! [X6] :
( X4 != X6
| ! [X7] :
( ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7) ) ) ) )
& ( ? [X8] :
( in(X8,powerset(X2))
& X4 = X8
& ? [X9] :
( X4 = X9
& ? [X10] :
( element(X10,the_carrier(X0))
& in(X10,X1)
& relstr_set_smaller(X0,X9,X10) ) ) )
| ~ in(X4,X3) ) )
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(rectify,[],[f2028]) ).
fof(f2030,plain,
! [X0,X1,X2] :
( ! [X4] :
( ( in(X4,sK289(X0,X1,X2))
| ! [X5] :
( ~ in(X5,powerset(X2))
| X4 != X5
| ! [X6] :
( X4 != X6
| ! [X7] :
( ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7) ) ) ) )
& ( ( in(sK290(X0,X1,X2,X4),powerset(X2))
& sK290(X0,X1,X2,X4) = X4
& sK291(X0,X1,X4) = X4
& element(sK292(X0,X1,X4),the_carrier(X0))
& in(sK292(X0,X1,X4),X1)
& relstr_set_smaller(X0,sK291(X0,X1,X4),sK292(X0,X1,X4)) )
| ~ in(X4,sK289(X0,X1,X2)) ) )
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK289,sK290,sK291,sK292]),skolemize(X3,sK289(X0,X1,X2)),skolemize(X8,sK290(X0,X1,X2,X4)),skolemize(X9,sK291(X0,X1,X4)),skolemize(X10,sK292(X0,X1,X4))],[f2029]) ).
fof(f2111,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,powerset(X2))
| ! [X5] :
( X4 != X5
| ! [X6] :
( ~ element(X6,the_carrier(X0))
| ~ in(X6,X1)
| ~ relstr_set_smaller(X0,X5,X6) ) )
| ~ in(X4,X3) )
& ( ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) )
| in(X4,X3) ) )
& ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) ),
inference(nnf_transformation,[],[f1259]) ).
fof(f2112,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,powerset(X2))
| ! [X5] :
( X4 != X5
| ! [X6] :
( ~ element(X6,the_carrier(X0))
| ~ in(X6,X1)
| ~ relstr_set_smaller(X0,X5,X6) ) )
| ~ in(X4,X3) )
& ( ( in(X4,powerset(X2))
& ? [X5] :
( X5 = X4
& ? [X6] :
( element(X6,the_carrier(X0))
& in(X6,X1)
& relstr_set_smaller(X0,X5,X6) ) ) )
| in(X4,X3) ) )
& ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) ),
inference(flattening,[],[f2111]) ).
fof(f2113,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,powerset(X2))
| ! [X5] :
( X4 != X5
| ! [X6] :
( ~ element(X6,the_carrier(X0))
| ~ in(X6,X1)
| ~ relstr_set_smaller(X0,X5,X6) ) )
| ~ in(X4,X3) )
& ( ( in(X4,powerset(X2))
& ? [X7] :
( X4 = X7
& ? [X8] :
( element(X8,the_carrier(X0))
& in(X8,X1)
& relstr_set_smaller(X0,X7,X8) ) ) )
| in(X4,X3) ) )
& ~ empty_carrier(X0)
& transitive_relstr(X0)
& rel_str(X0)
& element(X1,powerset(the_carrier(X0)))
& finite(X2)
& element(X2,powerset(X1)) ),
inference(rectify,[],[f2112]) ).
fof(f2114,plain,
( ! [X3] :
( ( ~ in(sK416(X3),powerset(sK415))
| ! [X5] :
( sK416(X3) != X5
| ! [X6] :
( ~ element(X6,the_carrier(sK413))
| ~ in(X6,sK414)
| ~ relstr_set_smaller(sK413,X5,X6) ) )
| ~ in(sK416(X3),X3) )
& ( ( in(sK416(X3),powerset(sK415))
& sK416(X3) = sK417(X3)
& element(sK418(X3),the_carrier(sK413))
& in(sK418(X3),sK414)
& relstr_set_smaller(sK413,sK417(X3),sK418(X3)) )
| in(sK416(X3),X3) ) )
& ~ empty_carrier(sK413)
& transitive_relstr(sK413)
& rel_str(sK413)
& element(sK414,powerset(the_carrier(sK413)))
& finite(sK415)
& element(sK415,powerset(sK414)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK413,sK414,sK415,sK416,sK417,sK418]),skolemize(X0,sK413),skolemize(X1,sK414),skolemize(X2,sK415),skolemize(X4,sK416(X3)),skolemize(X7,sK417(X3)),skolemize(X8,sK418(X3))],[f2113]) ).
fof(f3391,plain,
! [X0] : powerset(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f413]) ).
fof(f3558,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| sK282(X0,X1) = sK284(X0,X1) ),
inference(cnf_transformation,[],[f2027]) ).
fof(f3563,plain,
! [X0,X1] :
( ~ sP14(X0,X1)
| sK282(X0,X1) = sK283(X0,X1) ),
inference(cnf_transformation,[],[f2027]) ).
fof(f3564,plain,
! [X0,X1] :
( sK283(X0,X1) != sK284(X0,X1)
| ~ sP14(X0,X1) ),
inference(cnf_transformation,[],[f2027]) ).
fof(f3565,plain,
! [X2,X0,X1,X4] :
( relstr_set_smaller(X0,sK291(X0,X1,X4),sK292(X0,X1,X4))
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3566,plain,
! [X2,X0,X1,X4] :
( in(sK292(X0,X1,X4),X1)
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3568,plain,
! [X2,X0,X1,X4] :
( sK291(X0,X1,X4) = X4
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3569,plain,
! [X2,X0,X1,X4] :
( sK290(X0,X1,X2,X4) = X4
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3570,plain,
! [X2,X0,X1,X4] :
( in(sK290(X0,X1,X2,X4),powerset(X2))
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3571,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK289(X0,X1,X2))
| ~ in(X5,powerset(X2))
| X4 != X5
| X4 != X6
| ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,powerset(X1)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3767,plain,
element(sK415,powerset(sK414)),
inference(cnf_transformation,[],[f2114]) ).
fof(f3768,plain,
finite(sK415),
inference(cnf_transformation,[],[f2114]) ).
fof(f3769,plain,
element(sK414,powerset(the_carrier(sK413))),
inference(cnf_transformation,[],[f2114]) ).
fof(f3770,plain,
rel_str(sK413),
inference(cnf_transformation,[],[f2114]) ).
fof(f3771,plain,
transitive_relstr(sK413),
inference(cnf_transformation,[],[f2114]) ).
fof(f3772,plain,
~ empty_carrier(sK413),
inference(cnf_transformation,[],[f2114]) ).
fof(f3773,plain,
! [X3] :
( relstr_set_smaller(sK413,sK417(X3),sK418(X3))
| in(sK416(X3),X3) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f3774,plain,
! [X3] :
( in(sK418(X3),sK414)
| in(sK416(X3),X3) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f3776,plain,
! [X3] :
( in(sK416(X3),X3)
| sK416(X3) = sK417(X3) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f3777,plain,
! [X3] :
( in(sK416(X3),powerset(sK415))
| in(sK416(X3),X3) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f3778,plain,
! [X3,X6,X5] :
( ~ in(sK416(X3),powerset(sK415))
| sK416(X3) != X5
| ~ element(X6,the_carrier(sK413))
| ~ in(X6,sK414)
| ~ relstr_set_smaller(sK413,X5,X6)
| ~ in(sK416(X3),X3) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f4197,plain,
! [X2,X0,X1] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(cnf_transformation,[],[f1490]) ).
fof(f4722,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK289(X0,X1,X2))
| ~ in(X5,k1_pcomps_1(X2))
| X4 != X5
| X4 != X6
| ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3571,f3391,f3391,f3391]) ).
fof(f4723,plain,
! [X2,X0,X1,X4] :
( in(sK290(X0,X1,X2,X4),k1_pcomps_1(X2))
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3570,f3391,f3391,f3391]) ).
fof(f4724,plain,
! [X2,X0,X1,X4] :
( ~ transitive_relstr(X0)
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| sK290(X0,X1,X2,X4) = X4
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3569,f3391,f3391]) ).
fof(f4725,plain,
! [X2,X0,X1,X4] :
( ~ transitive_relstr(X0)
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| sK291(X0,X1,X4) = X4
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3568,f3391,f3391]) ).
fof(f4727,plain,
! [X2,X0,X1,X4] :
( ~ transitive_relstr(X0)
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| in(sK292(X0,X1,X4),X1)
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3566,f3391,f3391]) ).
fof(f4728,plain,
! [X2,X0,X1,X4] :
( ~ transitive_relstr(X0)
| ~ in(X4,sK289(X0,X1,X2))
| sP14(X0,X1)
| empty_carrier(X0)
| relstr_set_smaller(X0,sK291(X0,X1,X4),sK292(X0,X1,X4))
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(definition_unfolding,[],[f3565,f3391,f3391]) ).
fof(f4828,plain,
! [X3,X6,X5] :
( ~ in(sK416(X3),k1_pcomps_1(sK415))
| sK416(X3) != X5
| ~ element(X6,the_carrier(sK413))
| ~ in(X6,sK414)
| ~ relstr_set_smaller(sK413,X5,X6)
| ~ in(sK416(X3),X3) ),
inference(definition_unfolding,[],[f3778,f3391]) ).
fof(f4829,plain,
! [X3] :
( in(sK416(X3),k1_pcomps_1(sK415))
| in(sK416(X3),X3) ),
inference(definition_unfolding,[],[f3777,f3391]) ).
fof(f4830,plain,
element(sK414,k1_pcomps_1(the_carrier(sK413))),
inference(definition_unfolding,[],[f3769,f3391]) ).
fof(f4831,plain,
element(sK415,k1_pcomps_1(sK414)),
inference(definition_unfolding,[],[f3767,f3391]) ).
fof(f5028,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(definition_unfolding,[],[f4197,f3391]) ).
fof(f5225,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK289(X0,X1,X2))
| ~ in(X5,k1_pcomps_1(X2))
| X5 != X6
| ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(equality_resolution,[],[f4722]) ).
fof(f5226,plain,
! [X2,X0,X1,X6,X7] :
( in(X6,sK289(X0,X1,X2))
| ~ in(X6,k1_pcomps_1(X2))
| ~ element(X7,the_carrier(X0))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| sP14(X0,X1)
| empty_carrier(X0)
| ~ transitive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(equality_resolution,[],[f5225]) ).
fof(f5282,plain,
! [X3,X6] :
( ~ in(sK416(X3),k1_pcomps_1(sK415))
| ~ element(X6,the_carrier(sK413))
| ~ in(X6,sK414)
| ~ relstr_set_smaller(sK413,sK416(X3),X6)
| ~ in(sK416(X3),X3) ),
inference(equality_resolution,[],[f4828]) ).
fof(f5568,plain,
! [X2,X0,X1,X6,X7] :
( ~ transitive_relstr(X0)
| ~ in(X6,k1_pcomps_1(X2))
| ~ in(X7,X1)
| ~ relstr_set_smaller(X0,X6,X7)
| sP14(X0,X1)
| empty_carrier(X0)
| in(X6,sK289(X0,X1,X2))
| ~ rel_str(X0)
| ~ element(X1,k1_pcomps_1(the_carrier(X0)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5226,f5028]) ).
fof(f5792,plain,
! [X2,X3,X0,X1] :
( ~ in(X0,k1_pcomps_1(X1))
| ~ in(X2,X3)
| ~ relstr_set_smaller(sK413,X0,X2)
| sP14(sK413,X3)
| empty_carrier(sK413)
| in(X0,sK289(sK413,X3,X1))
| ~ rel_str(sK413)
| ~ element(X3,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X1)
| ~ element(X1,k1_pcomps_1(X3)) ),
inference(resolution,[],[f5568,f3771]) ).
fof(f5793,plain,
! [X2,X3,X0,X1] :
( ~ in(X0,k1_pcomps_1(X1))
| ~ in(X2,X3)
| ~ relstr_set_smaller(sK413,X0,X2)
| sP14(sK413,X3)
| in(X0,sK289(sK413,X3,X1))
| ~ rel_str(sK413)
| ~ element(X3,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X1)
| ~ element(X1,k1_pcomps_1(X3)) ),
inference(forward_subsumption_resolution,[],[f5792,f3772]) ).
fof(f5794,plain,
! [X2,X3,X0,X1] :
( ~ finite(X1)
| ~ in(X2,X3)
| ~ relstr_set_smaller(sK413,X0,X2)
| sP14(sK413,X3)
| in(X0,sK289(sK413,X3,X1))
| ~ element(X3,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,k1_pcomps_1(X1))
| ~ element(X1,k1_pcomps_1(X3)) ),
inference(forward_subsumption_resolution,[],[f5793,f3770]) ).
fof(f5795,plain,
! [X2,X0,X1] :
( ~ element(sK415,k1_pcomps_1(X1))
| ~ relstr_set_smaller(sK413,X2,X0)
| sP14(sK413,X1)
| in(X2,sK289(sK413,X1,sK415))
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X2,k1_pcomps_1(sK415))
| ~ in(X0,X1) ),
inference(resolution,[],[f5794,f3768]) ).
fof(f5796,plain,
! [X0,X1] :
( ~ relstr_set_smaller(sK413,X0,X1)
| sP14(sK413,sK414)
| in(X0,sK289(sK413,sK414,sK415))
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,k1_pcomps_1(sK415))
| ~ in(X1,sK414) ),
inference(resolution,[],[f5795,f4831]) ).
fof(f5797,plain,
! [X0,X1] :
( ~ relstr_set_smaller(sK413,X0,X1)
| sP14(sK413,sK414)
| in(X0,sK289(sK413,sK414,sK415))
| ~ in(X0,k1_pcomps_1(sK415))
| ~ in(X1,sK414) ),
inference(forward_subsumption_resolution,[],[f5796,f4830]) ).
fof(f5799,definition,
( spl519_76
<=> sP14(sK413,sK414) ),
introduced(definition,[new_symbols(definition,[spl519_76])],[avatar_definition]) ).
fof(f5800,plain,
( sP14(sK413,sK414)
| ~ spl519_76 ),
inference(avatar_component_clause,[],[f5799]) ).
fof(f5802,definition,
( spl519_77
<=> ! [X0,X1] :
( ~ relstr_set_smaller(sK413,X0,X1)
| ~ in(X1,sK414)
| ~ in(X0,k1_pcomps_1(sK415))
| in(X0,sK289(sK413,sK414,sK415)) ) ),
introduced(definition,[new_symbols(definition,[spl519_77])],[avatar_definition]) ).
fof(f5803,plain,
( ! [X0,X1] :
( ~ relstr_set_smaller(sK413,X0,X1)
| ~ in(X1,sK414)
| ~ in(X0,k1_pcomps_1(sK415))
| in(X0,sK289(sK413,sK414,sK415)) )
| ~ spl519_77 ),
inference(avatar_component_clause,[],[f5802]) ).
fof(f5804,plain,
( spl519_76
| spl519_77 ),
inference(avatar_split_clause,[],[f5797,f5802,f5799]) ).
fof(f5806,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| empty_carrier(sK413)
| relstr_set_smaller(sK413,sK291(sK413,X1,X0),sK292(sK413,X1,X0))
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(resolution,[],[f4728,f3771]) ).
fof(f5807,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| relstr_set_smaller(sK413,sK291(sK413,X1,X0),sK292(sK413,X1,X0))
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5806,f3772]) ).
fof(f5808,plain,
! [X2,X0,X1] :
( ~ finite(X2)
| sP14(sK413,X1)
| relstr_set_smaller(sK413,sK291(sK413,X1,X0),sK292(sK413,X1,X0))
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,X1,X2))
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5807,f3770]) ).
fof(f5810,plain,
! [X0] :
( element(X0,the_carrier(sK413))
| ~ in(X0,sK414) ),
inference(resolution,[],[f5028,f4830]) ).
fof(f5812,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| empty_carrier(sK413)
| sK291(sK413,X1,X0) = X0
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(resolution,[],[f4725,f3771]) ).
fof(f5813,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| sK291(sK413,X1,X0) = X0
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5812,f3772]) ).
fof(f5814,plain,
! [X2,X0,X1] :
( ~ finite(X2)
| sP14(sK413,X1)
| sK291(sK413,X1,X0) = X0
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,X1,X2))
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5813,f3770]) ).
fof(f5815,plain,
! [X0,X1] :
( ~ element(sK415,k1_pcomps_1(X0))
| sK291(sK413,X0,X1) = X1
| ~ element(X0,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X1,sK289(sK413,X0,sK415))
| sP14(sK413,X0) ),
inference(resolution,[],[f5814,f3768]) ).
fof(f5816,plain,
! [X0] :
( sK291(sK413,sK414,X0) = X0
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,sK414,sK415))
| sP14(sK413,sK414) ),
inference(resolution,[],[f5815,f4831]) ).
fof(f5817,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| empty_carrier(sK413)
| in(sK292(sK413,X1,X0),X1)
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(resolution,[],[f4727,f3771]) ).
fof(f5818,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| in(sK292(sK413,X1,X0),X1)
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5817,f3772]) ).
fof(f5819,plain,
! [X2,X0,X1] :
( ~ finite(X2)
| sP14(sK413,X1)
| in(sK292(sK413,X1,X0),X1)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,X1,X2))
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5818,f3770]) ).
fof(f5822,plain,
! [X0,X1] :
( relstr_set_smaller(sK413,sK291(sK413,X0,X1),sK292(sK413,X0,X1))
| sP14(sK413,X0)
| ~ element(X0,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X1,sK289(sK413,X0,sK415))
| ~ element(sK415,k1_pcomps_1(X0)) ),
inference(resolution,[],[f5808,f3768]) ).
fof(f5824,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| empty_carrier(sK413)
| sK290(sK413,X1,X2,X0) = X0
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(resolution,[],[f4724,f3771]) ).
fof(f5825,plain,
! [X2,X0,X1] :
( ~ in(X0,sK289(sK413,X1,X2))
| sP14(sK413,X1)
| sK290(sK413,X1,X2,X0) = X0
| ~ rel_str(sK413)
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(X2)
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5824,f3772]) ).
fof(f5826,plain,
! [X2,X0,X1] :
( ~ finite(X2)
| sP14(sK413,X1)
| sK290(sK413,X1,X2,X0) = X0
| ~ element(X1,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,X1,X2))
| ~ element(X2,k1_pcomps_1(X1)) ),
inference(forward_subsumption_resolution,[],[f5825,f3770]) ).
fof(f5827,plain,
! [X0,X1] :
( ~ element(sK415,k1_pcomps_1(X0))
| sK290(sK413,X0,sK415,X1) = X1
| ~ element(X0,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X1,sK289(sK413,X0,sK415))
| sP14(sK413,X0) ),
inference(resolution,[],[f5826,f3768]) ).
fof(f5828,plain,
! [X0] :
( sK290(sK413,sK414,sK415,X0) = X0
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X0,sK289(sK413,sK414,sK415))
| sP14(sK413,sK414) ),
inference(resolution,[],[f5827,f4831]) ).
fof(f5832,plain,
! [X0,X1] :
( in(sK292(sK413,X0,X1),X0)
| sP14(sK413,X0)
| ~ element(X0,k1_pcomps_1(the_carrier(sK413)))
| ~ in(X1,sK289(sK413,X0,sK415))
| ~ element(sK415,k1_pcomps_1(X0)) ),
inference(resolution,[],[f5819,f3768]) ).
fof(f6853,plain,
( sK284(sK413,sK414) = sK282(sK413,sK414)
| ~ spl519_76 ),
inference(resolution,[],[f3558,f5800]) ).
fof(f6854,plain,
( sK283(sK413,sK414) = sK282(sK413,sK414)
| ~ spl519_76 ),
inference(resolution,[],[f3563,f5800]) ).
fof(f6856,plain,
( sK283(sK413,sK414) = sK284(sK413,sK414)
| ~ spl519_76 ),
inference(superposition,[],[f6853,f6854]) ).
fof(f6859,plain,
( sK283(sK413,sK414) != sK283(sK413,sK414)
| ~ sP14(sK413,sK414)
| ~ spl519_76 ),
inference(superposition,[],[f3564,f6856]) ).
fof(f6860,plain,
( ~ sP14(sK413,sK414)
| ~ spl519_76 ),
inference(trivial_inequality_removal,[],[f6859]) ).
fof(f6862,plain,
( $false
| ~ spl519_76 ),
inference(forward_subsumption_resolution,[],[f6860,f5800]) ).
fof(f6863,plain,
~ spl519_76,
inference(avatar_contradiction_clause,[],[f6862]) ).
fof(f6864,plain,
! [X0] :
( sK291(sK413,sK414,X0) = X0
| ~ in(X0,sK289(sK413,sK414,sK415))
| sP14(sK413,sK414) ),
inference(forward_subsumption_resolution,[],[f5816,f4830]) ).
fof(f6865,plain,
! [X0] :
( sK290(sK413,sK414,sK415,X0) = X0
| ~ in(X0,sK289(sK413,sK414,sK415))
| sP14(sK413,sK414) ),
inference(forward_subsumption_resolution,[],[f5828,f4830]) ).
fof(f6868,definition,
( spl519_122
<=> ! [X0] :
( sK291(sK413,sK414,X0) = X0
| ~ in(X0,sK289(sK413,sK414,sK415)) ) ),
introduced(definition,[new_symbols(definition,[spl519_122])],[avatar_definition]) ).
fof(f6869,plain,
( ! [X0] :
( ~ in(X0,sK289(sK413,sK414,sK415))
| sK291(sK413,sK414,X0) = X0 )
| ~ spl519_122 ),
inference(avatar_component_clause,[],[f6868]) ).
fof(f6870,plain,
( spl519_76
| spl519_122 ),
inference(avatar_split_clause,[],[f6864,f6868,f5799]) ).
fof(f6872,definition,
( spl519_123
<=> ! [X0] :
( sK290(sK413,sK414,sK415,X0) = X0
| ~ in(X0,sK289(sK413,sK414,sK415)) ) ),
introduced(definition,[new_symbols(definition,[spl519_123])],[avatar_definition]) ).
fof(f6873,plain,
( ! [X0] :
( ~ in(X0,sK289(sK413,sK414,sK415))
| sK290(sK413,sK414,sK415,X0) = X0 )
| ~ spl519_123 ),
inference(avatar_component_clause,[],[f6872]) ).
fof(f6874,plain,
( spl519_76
| spl519_123 ),
inference(avatar_split_clause,[],[f6865,f6872,f5799]) ).
fof(f6941,definition,
( spl519_132
<=> sK416(sK289(sK413,sK414,sK415)) = sK291(sK413,sK414,sK416(sK289(sK413,sK414,sK415))) ),
introduced(definition,[new_symbols(definition,[spl519_132])],[avatar_definition]) ).
fof(f6942,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK291(sK413,sK414,sK416(sK289(sK413,sK414,sK415)))
| ~ spl519_132 ),
inference(avatar_component_clause,[],[f6941]) ).
fof(f6953,definition,
( spl519_135
<=> in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415)) ),
introduced(definition,[new_symbols(definition,[spl519_135])],[avatar_definition]) ).
fof(f6954,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| ~ spl519_135 ),
inference(avatar_component_clause,[],[f6953]) ).
fof(f6957,definition,
( spl519_136
<=> sK416(sK289(sK413,sK414,sK415)) = sK417(sK289(sK413,sK414,sK415)) ),
introduced(definition,[new_symbols(definition,[spl519_136])],[avatar_definition]) ).
fof(f6958,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK417(sK289(sK413,sK414,sK415))
| ~ spl519_136 ),
inference(avatar_component_clause,[],[f6957]) ).
fof(f6994,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK290(sK413,sK414,sK415,sK416(sK289(sK413,sK414,sK415)))
| in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| ~ spl519_123 ),
inference(resolution,[],[f6873,f4829]) ).
fof(f7007,definition,
( spl519_144
<=> sK416(sK289(sK413,sK414,sK415)) = sK290(sK413,sK414,sK415,sK416(sK289(sK413,sK414,sK415))) ),
introduced(definition,[new_symbols(definition,[spl519_144])],[avatar_definition]) ).
fof(f7008,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK290(sK413,sK414,sK415,sK416(sK289(sK413,sK414,sK415)))
| ~ spl519_144 ),
inference(avatar_component_clause,[],[f7007]) ).
fof(f7012,plain,
( spl519_135
| spl519_144
| ~ spl519_123 ),
inference(avatar_split_clause,[],[f6994,f6872,f7007,f6953]) ).
fof(f7041,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))))
| sP14(sK413,sK414)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_132 ),
inference(superposition,[],[f5822,f6942]) ).
fof(f7042,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))))
| sP14(sK413,sK414)
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_132 ),
inference(forward_subsumption_resolution,[],[f7041,f4830]) ).
fof(f7043,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))))
| sP14(sK413,sK414)
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_132 ),
inference(forward_subsumption_resolution,[],[f7042,f4831]) ).
fof(f7045,definition,
( spl519_148
<=> in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415)) ),
introduced(definition,[new_symbols(definition,[spl519_148])],[avatar_definition]) ).
fof(f7046,plain,
( ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| spl519_148 ),
inference(avatar_component_clause,[],[f7045]) ).
fof(f7048,definition,
( spl519_149
<=> relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415)))) ),
introduced(definition,[new_symbols(definition,[spl519_149])],[avatar_definition]) ).
fof(f7049,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))))
| ~ spl519_149 ),
inference(avatar_component_clause,[],[f7048]) ).
fof(f7050,plain,
( ~ spl519_148
| spl519_76
| spl519_149
| ~ spl519_132 ),
inference(avatar_split_clause,[],[f7043,f6941,f7048,f5799,f7045]) ).
fof(f7053,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK417(sK289(sK413,sK414,sK415))
| spl519_148 ),
inference(resolution,[],[f7046,f3776]) ).
fof(f7062,plain,
( spl519_136
| spl519_148 ),
inference(avatar_split_clause,[],[f7053,f7045,f6957]) ).
fof(f7067,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK413))
| ~ in(X0,sK414)
| ~ relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),X0)
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415)) )
| ~ spl519_135 ),
inference(resolution,[],[f6954,f5282]) ).
fof(f7069,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK418(sK289(sK413,sK414,sK415)))
| in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_136 ),
inference(superposition,[],[f3773,f6958]) ).
fof(f7070,plain,
( relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),sK418(sK289(sK413,sK414,sK415)))
| ~ spl519_136
| spl519_148 ),
inference(forward_subsumption_resolution,[],[f7069,f7046]) ).
fof(f7073,plain,
( ~ in(sK418(sK289(sK413,sK414,sK415)),sK414)
| ~ in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(resolution,[],[f7070,f5803]) ).
fof(f7077,plain,
( ~ in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(forward_subsumption_resolution,[],[f7073,f3774]) ).
fof(f7079,plain,
( in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(forward_subsumption_resolution,[],[f7077,f4829]) ).
fof(f7081,plain,
( $false
| ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(forward_subsumption_resolution,[],[f7079,f7046]) ).
fof(f7082,plain,
( ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(avatar_contradiction_clause,[],[f7081]) ).
fof(f7083,plain,
( ! [X0] :
( ~ in(X0,sK414)
| ~ relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),X0)
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415)) )
| ~ spl519_135 ),
inference(forward_subsumption_resolution,[],[f7067,f5810]) ).
fof(f7084,plain,
( in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ spl519_148 ),
inference(avatar_component_clause,[],[f7045]) ).
fof(f7090,definition,
( spl519_151
<=> ! [X0] :
( ~ in(X0,sK414)
| ~ relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl519_151])],[avatar_definition]) ).
fof(f7091,plain,
( ! [X0] :
( ~ relstr_set_smaller(sK413,sK416(sK289(sK413,sK414,sK415)),X0)
| ~ in(X0,sK414) )
| ~ spl519_151 ),
inference(avatar_component_clause,[],[f7090]) ).
fof(f7092,plain,
( ~ spl519_148
| spl519_151
| ~ spl519_135 ),
inference(avatar_split_clause,[],[f7083,f6953,f7090,f7045]) ).
fof(f7094,plain,
( sK416(sK289(sK413,sK414,sK415)) = sK291(sK413,sK414,sK416(sK289(sK413,sK414,sK415)))
| ~ spl519_122
| ~ spl519_148 ),
inference(resolution,[],[f7084,f6869]) ).
fof(f7096,plain,
( ~ in(sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))),sK414)
| ~ spl519_149
| ~ spl519_151 ),
inference(resolution,[],[f7049,f7091]) ).
fof(f7103,definition,
( spl519_153
<=> in(sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))),sK414) ),
introduced(definition,[new_symbols(definition,[spl519_153])],[avatar_definition]) ).
fof(f7104,plain,
( ~ in(sK292(sK413,sK414,sK416(sK289(sK413,sK414,sK415))),sK414)
| spl519_153 ),
inference(avatar_component_clause,[],[f7103]) ).
fof(f7106,plain,
( ~ spl519_153
| ~ spl519_149
| ~ spl519_151 ),
inference(avatar_split_clause,[],[f7096,f7090,f7048,f7103]) ).
fof(f7113,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| sP14(sK413,sK414)
| empty_carrier(sK413)
| ~ transitive_relstr(sK413)
| ~ rel_str(sK413)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(superposition,[],[f4723,f7008]) ).
fof(f7114,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| empty_carrier(sK413)
| ~ transitive_relstr(sK413)
| ~ rel_str(sK413)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7113,f4829]) ).
fof(f7119,plain,
( sP14(sK413,sK414)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ element(sK415,k1_pcomps_1(sK414))
| spl519_153 ),
inference(resolution,[],[f7104,f5832]) ).
fof(f7120,plain,
( sP14(sK413,sK414)
| ~ in(sK416(sK289(sK413,sK414,sK415)),sK289(sK413,sK414,sK415))
| ~ element(sK415,k1_pcomps_1(sK414))
| spl519_153 ),
inference(forward_subsumption_resolution,[],[f7119,f4830]) ).
fof(f7121,plain,
( sP14(sK413,sK414)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_148
| spl519_153 ),
inference(forward_subsumption_resolution,[],[f7120,f7084]) ).
fof(f7122,plain,
( sP14(sK413,sK414)
| ~ spl519_148
| spl519_153 ),
inference(forward_subsumption_resolution,[],[f7121,f4831]) ).
fof(f7123,plain,
( spl519_76
| ~ spl519_148
| spl519_153 ),
inference(avatar_split_clause,[],[f7122,f7103,f7045,f5799]) ).
fof(f7124,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ transitive_relstr(sK413)
| ~ rel_str(sK413)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7114,f3772]) ).
fof(f7125,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ rel_str(sK413)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7124,f3771]) ).
fof(f7126,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ element(sK414,k1_pcomps_1(the_carrier(sK413)))
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7125,f3770]) ).
fof(f7127,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ finite(sK415)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7126,f4830]) ).
fof(f7128,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ element(sK415,k1_pcomps_1(sK414))
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7127,f3768]) ).
fof(f7129,plain,
( in(sK416(sK289(sK413,sK414,sK415)),k1_pcomps_1(sK415))
| sP14(sK413,sK414)
| ~ spl519_144 ),
inference(forward_subsumption_resolution,[],[f7128,f4831]) ).
fof(f7130,plain,
( spl519_76
| spl519_135
| ~ spl519_144 ),
inference(avatar_split_clause,[],[f7129,f7007,f6953,f5799]) ).
fof(f7131,plain,
( spl519_132
| ~ spl519_122
| ~ spl519_148 ),
inference(avatar_split_clause,[],[f7094,f7045,f6868,f6941]) ).
cnf(s69,plain,
( spl519_76
| spl519_77 ),
inference(sat_conversion,[],[f5804]) ).
cnf(s104,plain,
~ spl519_76,
inference(sat_conversion,[],[f6863]) ).
cnf(s105,plain,
( spl519_76
| spl519_122 ),
inference(sat_conversion,[],[f6870]) ).
cnf(s106,plain,
( spl519_76
| spl519_123 ),
inference(sat_conversion,[],[f6874]) ).
cnf(s125,plain,
( ~ spl519_123
| spl519_135
| spl519_144 ),
inference(sat_conversion,[],[f7012]) ).
cnf(s131,plain,
( spl519_76
| ~ spl519_132
| ~ spl519_148
| spl519_149 ),
inference(sat_conversion,[],[f7050]) ).
cnf(s136,plain,
( spl519_136
| spl519_148 ),
inference(sat_conversion,[],[f7062]) ).
cnf(s140,plain,
( ~ spl519_77
| ~ spl519_136
| spl519_148 ),
inference(sat_conversion,[],[f7082]) ).
cnf(s142,plain,
( ~ spl519_135
| ~ spl519_148
| spl519_151 ),
inference(sat_conversion,[],[f7092]) ).
cnf(s144,plain,
( ~ spl519_149
| ~ spl519_151
| ~ spl519_153 ),
inference(sat_conversion,[],[f7106]) ).
cnf(s145,plain,
( spl519_76
| ~ spl519_148
| spl519_153 ),
inference(sat_conversion,[],[f7123]) ).
cnf(s146,plain,
( spl519_76
| spl519_135
| ~ spl519_144 ),
inference(sat_conversion,[],[f7130]) ).
cnf(s147,plain,
( ~ spl519_122
| spl519_132
| ~ spl519_148 ),
inference(sat_conversion,[],[f7131]) ).
cnf(s149,plain,
spl519_123,
inference(rat,[],[s106,s104]) ).
cnf(s150,plain,
spl519_122,
inference(rat,[],[s105,s104]) ).
cnf(s151,plain,
spl519_77,
inference(rat,[],[s69,s104]) ).
cnf(s154,plain,
( ~ spl519_148
| ~ spl519_135
| ~ spl519_132 ),
inference(rat,[],[s144,s142,s131,s145,s104]) ).
cnf(s155,plain,
spl519_148,
inference(rat,[],[s140,s136,s151]) ).
cnf(s157,plain,
spl519_135,
inference(rat,[],[s125,s146,s149,s104]) ).
cnf(s158,plain,
spl519_132,
inference(rat,[],[s147,s150,s155]) ).
cnf(s159,plain,
$false,
inference(rat,[],[s154,s158,s157,s155]) ).
fof(f7132,plain,
$false,
inference(avatar_sat_refutation,[],[s159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU364+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n013.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:57:48 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 5.48/1.91 % (811504)Detected formulas, will run a generic FOF schedule.
% 5.48/1.91 % (811510)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=3490773937:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.48/1.91 % (811509)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=1044264302:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.48/1.91 % (811513)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1134192028:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.48/1.91 % (811515)dis-21_1_sil=8000:lcm=predicate:random_seed=362539078: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)
% 5.48/1.91 % (811512)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3365866785:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.48/1.91 % (811511)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=1416198246:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.48/1.91 % (811514)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=299317505:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.48/1.91 % (811512)Instruction limit reached!
% 5.48/1.91 % (811512)------------------------------
% 5.48/1.91 % (811512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811512)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811512)Termination reason: Instruction limit
% 5.48/1.91 % (811512)Termination phase: Saturation
% 5.48/1.91 % (811512)Time elapsed: 0.058 s
% 5.48/1.91 % (811512)Peak memory usage: 91 MB
% 5.48/1.91 % (811512)Instructions burned: 109 (million)
% 5.48/1.91 % (811515)Instruction limit reached!
% 5.48/1.91 % (811515)------------------------------
% 5.48/1.91 % (811515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811515)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811515)Termination reason: Instruction limit
% 5.48/1.91 % (811515)Termination phase: Saturation
% 5.48/1.91 % (811515)Time elapsed: 0.066 s
% 5.48/1.91 % (811515)Peak memory usage: 91 MB
% 5.48/1.91 % (811515)Instructions burned: 129 (million)
% 5.48/1.91 % (811513)Instruction limit reached!
% 5.48/1.91 % (811513)------------------------------
% 5.48/1.91 % (811513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811513)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811513)Termination reason: Instruction limit
% 5.48/1.91 % (811513)Termination phase: Saturation
% 5.48/1.91 % (811513)Time elapsed: 0.072 s
% 5.48/1.91 % (811513)Peak memory usage: 91 MB
% 5.48/1.91 % (811513)Instructions burned: 119 (million)
% 5.48/1.91 % (811514)Instruction limit reached!
% 5.48/1.91 % (811514)------------------------------
% 5.48/1.91 % (811514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811514)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811514)Termination reason: Instruction limit
% 5.48/1.91 % (811514)Termination phase: Saturation
% 5.48/1.91 % (811514)Time elapsed: 0.085 s
% 5.48/1.91 % (811514)Peak memory usage: 92 MB
% 5.48/1.91 % (811514)Instructions burned: 139 (million)
% 5.48/1.91 % (811523)lrs+10_1_sil=8000:sp=occurrence:random_seed=2822227941:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.48/1.91 % (811524)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2956390437:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.48/1.91 % (811525)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3088249053:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.48/1.91 % (811526)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=417883782:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.48/1.91 % (811524)Instruction limit reached!
% 5.48/1.91 % (811524)------------------------------
% 5.48/1.91 % (811524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811524)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811524)Termination reason: Instruction limit
% 5.48/1.91 % (811524)Termination phase: Saturation
% 5.48/1.91 % (811524)Time elapsed: 0.084 s
% 5.48/1.91 % (811524)Peak memory usage: 92 MB
% 5.48/1.91 % (811524)Instructions burned: 157 (million)
% 5.48/1.91 % (811526)Instruction limit reached!
% 5.48/1.91 % (811526)------------------------------
% 5.48/1.91 % (811526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811526)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811526)Termination reason: Instruction limit
% 5.48/1.91 % (811526)Termination phase: Saturation
% 5.48/1.91 % (811526)Time elapsed: 0.143 s
% 5.48/1.91 % (811526)Peak memory usage: 95 MB
% 5.48/1.91 % (811526)Instructions burned: 249 (million)
% 5.48/1.91 % (811523)Instruction limit reached!
% 5.48/1.91 % (811523)------------------------------
% 5.48/1.91 % (811523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811523)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811523)Termination reason: Instruction limit
% 5.48/1.91 % (811523)Termination phase: Saturation
% 5.48/1.91 % (811523)Time elapsed: 0.177 s
% 5.48/1.91 % (811523)Peak memory usage: 95 MB
% 5.48/1.91 % (811523)Instructions burned: 285 (million)
% 5.48/1.91 % (811531)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3812829928:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.48/1.91 % (811525)Instruction limit reached!
% 5.48/1.91 % (811525)------------------------------
% 5.48/1.91 % (811525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811525)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811525)Termination reason: Instruction limit
% 5.48/1.91 % (811525)Termination phase: Saturation
% 5.48/1.91 % (811525)Time elapsed: 0.217 s
% 5.48/1.91 % (811525)Peak memory usage: 95 MB
% 5.48/1.91 % (811525)Instructions burned: 325 (million)
% 5.48/1.91 % (811532)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1295767331:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.48/1.91 % (811533)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2263012147:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.48/1.91 % (811535)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4244700756:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.48/1.91 % (811533)Instruction limit reached!
% 5.48/1.91 % (811533)------------------------------
% 5.48/1.91 % (811533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811533)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811533)Termination reason: Instruction limit
% 5.48/1.91 % (811533)Termination phase: Saturation
% 5.48/1.91 % (811533)Time elapsed: 0.063 s
% 5.48/1.91 % (811533)Peak memory usage: 92 MB
% 5.48/1.91 % (811533)Instructions burned: 113 (million)
% 5.48/1.91 % (811531)Instruction limit reached!
% 5.48/1.91 % (811531)------------------------------
% 5.48/1.91 % (811531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811531)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811531)Termination reason: Instruction limit
% 5.48/1.91 % (811531)Termination phase: Saturation
% 5.48/1.91 % (811531)Time elapsed: 0.182 s
% 5.48/1.91 % (811531)Peak memory usage: 93 MB
% 5.48/1.91 % (811531)Instructions burned: 294 (million)
% 5.48/1.91 % (811535)Instruction limit reached!
% 5.48/1.91 % (811535)------------------------------
% 5.48/1.91 % (811535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811535)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811535)Termination reason: Instruction limit
% 5.48/1.91 % (811535)Termination phase: Saturation
% 5.48/1.91 % (811535)Time elapsed: 0.069 s
% 5.48/1.91 % (811535)Peak memory usage: 91 MB
% 5.48/1.91 % (811535)Instructions burned: 127 (million)
% 5.48/1.91 % (811539)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2885184605:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 5.48/1.91 % (811510)First to succeed.
% 5.48/1.91 % (811510)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-811504"
% 5.48/1.91 % (811540)lrs+10_1_sil=8000:sp=occurrence:random_seed=4135760204:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 5.48/1.91 % (811539)Instruction limit reached!
% 5.48/1.91 % (811539)------------------------------
% 5.48/1.91 % (811539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/1.91 % (811539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.91 % (811539)CaDiCaL version: 2.1.3
% 5.48/1.91 % (811539)Termination reason: Instruction limit
% 5.48/1.91 % (811539)Termination phase: Saturation
% 5.48/1.91 % (811539)Time elapsed: 0.055 s
% 5.48/1.91 % (811539)Peak memory usage: 89 MB
% 5.48/1.91 % (811539)Instructions burned: 115 (million)
% 5.48/1.91 % (811541)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2894401498:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 5.48/1.91 % (811510)Refutation found. Thanks to Tanya!
% 5.48/1.91 % SZS status Theorem for theBenchmark
% 5.48/1.91 % SZS output start Proof for theBenchmark
% See solution above
% 5.48/2.02 % (811510)------------------------------
% 5.48/2.02 % (811510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.48/2.02 % (811510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/2.02 % (811510)CaDiCaL version: 2.1.3
% 5.48/2.02 % (811510)Termination reason: Refutation
% 5.48/2.02 % (811510)Time elapsed: 0.742 s
% 5.48/2.02 % (811510)Peak memory usage: 155 MB
% 5.48/2.02 % (811510)Instructions burned: 2050 (million)
% 5.48/2.02 % (811510)------------------------------
% 5.48/2.02 % (811510)------------------------------
% 5.48/2.02 % (811504)Success in time 1.049 s
% 5.48/2.02 % Vampire exiting
%------------------------------------------------------------------------------