%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU334+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:24 PM UTC 2026
% Result : Theorem 133.06s 40.44s
% Output : Refutation 280.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 35
% Syntax : Number of formulae : 341 ( 16 unt; 23 def)
% Number of atoms : 1668 ( 347 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 2223 ( 896 ~;1000 |; 209 &)
% ( 28 <=>; 90 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 30 ( 28 usr; 20 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 2 con; 0-3 aty)
% Number of variables : 534 ( 0 sgn 445 !; 89 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f116,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ! [X2] :
( element(X2,powerset(powerset(X0)))
=> ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( element(X3,powerset(X0))
=> ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_setfam_1) ).
fof(f140,axiom,
! [X0] :
( one_sorted_str(X0)
=> element(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f149,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> element(subset_complement(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f167,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(complements_of_subsets(X0,X1),powerset(powerset(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_setfam_1) ).
fof(f256,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,subset_complement(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f258,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k7_setfam_1) ).
fof(f316,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_subset_1) ).
fof(f340,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ! [X2,X3,X4] :
( ( in(X2,X1)
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& in(X2,X1)
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,X1)
& in(X4,X1)
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X4
=> X3 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_7_2__tops_2__1) ).
fof(f360,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X3] :
~ ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X2
=> X3 = subset_complement(the_carrier(X0),X7) ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = complements_of_subsets(the_carrier(X0),X1)
& ! [X3] :
( in(X3,complements_of_subsets(the_carrier(X0),X1))
=> ! [X8] :
( element(X8,powerset(the_carrier(X0)))
=> ( X8 = X3
=> apply(X2,X3) = subset_complement(the_carrier(X0),X8) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_funct_1__e4_7_1__tops_2) ).
fof(f361,conjecture,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X1)
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,X1)
& ! [X3] :
~ ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X2
=> X3 = subset_complement(the_carrier(X0),X7) ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X1
& ! [X3] :
( in(X3,X1)
=> ! [X8] :
( element(X8,powerset(the_carrier(X0)))
=> ( X8 = X3
=> apply(X2,X3) = subset_complement(the_carrier(X0),X8) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_funct_1__e4_7_2__tops_2) ).
fof(f362,negated_conjecture,
~ ! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X1)
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,X1)
& ! [X3] :
~ ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X2
=> X3 = subset_complement(the_carrier(X0),X7) ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X1
& ! [X3] :
( in(X3,X1)
=> ! [X8] :
( element(X8,powerset(the_carrier(X0)))
=> ( X8 = X3
=> apply(X2,X3) = subset_complement(the_carrier(X0),X8) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f361]) ).
fof(f406,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_pre_topc) ).
fof(f497,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f577,plain,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ! [X2,X3,X4] :
( ( in(X2,X1)
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& in(X2,X1)
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
=> ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,X1)
& in(X9,X1)
& ! [X10] :
( element(X10,powerset(the_carrier(X0)))
=> ( X9 = X10
=> subset_complement(the_carrier(X0),X10) = X8 ) ) ) ) ) ),
inference(rectify,[],[f340]) ).
fof(f585,plain,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
& ! [X7] :
~ ( in(X7,complements_of_subsets(the_carrier(X0),X1))
& ! [X8] :
~ ! [X9] :
( element(X9,powerset(the_carrier(X0)))
=> ( X7 = X9
=> subset_complement(the_carrier(X0),X9) = X8 ) ) ) )
=> ? [X10] :
( relation(X10)
& function(X10)
& complements_of_subsets(the_carrier(X0),X1) = relation_dom(X10)
& ! [X11] :
( in(X11,complements_of_subsets(the_carrier(X0),X1))
=> ! [X12] :
( element(X12,powerset(the_carrier(X0)))
=> ( X11 = X12
=> apply(X10,X11) = subset_complement(the_carrier(X0),X12) ) ) ) ) ) ),
inference(rectify,[],[f360]) ).
fof(f586,plain,
~ ! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X1)
& ! [X5] :
( element(X5,powerset(the_carrier(X0)))
=> ( X5 = X2
=> X3 = subset_complement(the_carrier(X0),X5) ) )
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
& ! [X7] :
~ ( in(X7,X1)
& ! [X8] :
~ ! [X9] :
( element(X9,powerset(the_carrier(X0)))
=> ( X7 = X9
=> subset_complement(the_carrier(X0),X9) = X8 ) ) ) )
=> ? [X10] :
( relation(X10)
& function(X10)
& relation_dom(X10) = X1
& ! [X11] :
( in(X11,X1)
=> ! [X12] :
( element(X12,powerset(the_carrier(X0)))
=> ( X11 = X12
=> apply(X10,X11) = subset_complement(the_carrier(X0),X12) ) ) ) ) ) ),
inference(rectify,[],[f362]) ).
fof(f728,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = complements_of_subsets(X0,X1)
<=> ! [X3] :
( ( in(X3,X2)
<=> in(subset_complement(X0,X3),X1) )
| ~ element(X3,powerset(X0)) ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f116]) ).
fof(f745,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f747,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f149]) ).
fof(f762,plain,
! [X0,X1] :
( element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f167]) ).
fof(f846,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f256]) ).
fof(f848,plain,
! [X0,X1] :
( complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f258]) ).
fof(f888,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f316]) ).
fof(f889,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f888]) ).
fof(f928,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,X1)
& in(X9,X1)
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X8
| X9 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X1)
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& in(X2,X1)
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f577]) ).
fof(f929,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,X1)
& in(X9,X1)
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X8
| X9 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X1)
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& in(X2,X1)
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f928]) ).
fof(f963,plain,
! [X0,X1] :
( ? [X10] :
( relation(X10)
& function(X10)
& complements_of_subsets(the_carrier(X0),X1) = relation_dom(X10)
& ! [X11] :
( ! [X12] :
( apply(X10,X11) = subset_complement(the_carrier(X0),X12)
| X11 != X12
| ~ element(X12,powerset(the_carrier(X0))) )
| ~ in(X11,complements_of_subsets(the_carrier(X0),X1)) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ? [X7] :
( in(X7,complements_of_subsets(the_carrier(X0),X1))
& ! [X8] :
? [X9] :
( subset_complement(the_carrier(X0),X9) != X8
& X7 = X9
& element(X9,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f585]) ).
fof(f964,plain,
! [X0,X1] :
( ? [X10] :
( relation(X10)
& function(X10)
& complements_of_subsets(the_carrier(X0),X1) = relation_dom(X10)
& ! [X11] :
( ! [X12] :
( apply(X10,X11) = subset_complement(the_carrier(X0),X12)
| X11 != X12
| ~ element(X12,powerset(the_carrier(X0))) )
| ~ in(X11,complements_of_subsets(the_carrier(X0),X1)) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ? [X7] :
( in(X7,complements_of_subsets(the_carrier(X0),X1))
& ! [X8] :
? [X9] :
( subset_complement(the_carrier(X0),X9) != X8
& X7 = X9
& element(X9,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f963]) ).
fof(f965,plain,
? [X0,X1] :
( ! [X10] :
( ~ relation(X10)
| ~ function(X10)
| relation_dom(X10) != X1
| ? [X11] :
( ? [X12] :
( apply(X10,X11) != subset_complement(the_carrier(X0),X12)
& X11 = X12
& element(X12,powerset(the_carrier(X0))) )
& in(X11,X1) ) )
& ! [X2,X3,X4] :
( X3 = X4
| ~ in(X2,X1)
| ? [X5] :
( subset_complement(the_carrier(X0),X5) != X3
& X5 = X2
& element(X5,powerset(the_carrier(X0))) )
| ? [X6] :
( subset_complement(the_carrier(X0),X6) != X4
& X6 = X2
& element(X6,powerset(the_carrier(X0))) ) )
& ! [X7] :
( ~ in(X7,X1)
| ? [X8] :
! [X9] :
( subset_complement(the_carrier(X0),X9) = X8
| X7 != X9
| ~ element(X9,powerset(the_carrier(X0))) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f586]) ).
fof(f966,plain,
? [X0,X1] :
( ! [X10] :
( ~ relation(X10)
| ~ function(X10)
| relation_dom(X10) != X1
| ? [X11] :
( ? [X12] :
( apply(X10,X11) != subset_complement(the_carrier(X0),X12)
& X11 = X12
& element(X12,powerset(the_carrier(X0))) )
& in(X11,X1) ) )
& ! [X2,X3,X4] :
( X3 = X4
| ~ in(X2,X1)
| ? [X5] :
( subset_complement(the_carrier(X0),X5) != X3
& X5 = X2
& element(X5,powerset(the_carrier(X0))) )
| ? [X6] :
( subset_complement(the_carrier(X0),X6) != X4
& X6 = X2
& element(X6,powerset(the_carrier(X0))) ) )
& ! [X7] :
( ~ in(X7,X1)
| ? [X8] :
! [X9] :
( subset_complement(the_carrier(X0),X9) = X8
| X7 != X9
| ~ element(X9,powerset(the_carrier(X0))) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f965]) ).
fof(f1024,plain,
! [X0] :
( ! [X1] :
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f406]) ).
fof(f1132,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f497]) ).
fof(f1133,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f1132]) ).
fof(f1256,definition,
! [X1,X0] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,X1)
& in(X9,X1)
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X8
| X9 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) ) )
| ~ sP35(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f1257,plain,
! [X0,X1] :
( sP35(X1,X0)
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X1)
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& in(X2,X1)
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(definition_folding,[],[f929,f1256]) ).
fof(f1278,definition,
! [X1,X0] :
( ? [X7] :
( in(X7,complements_of_subsets(the_carrier(X0),X1))
& ! [X8] :
? [X9] :
( subset_complement(the_carrier(X0),X9) != X8
& X7 = X9
& element(X9,powerset(the_carrier(X0))) ) )
| ~ sP48(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f1279,definition,
! [X1,X0] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ sP49(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f1280,plain,
! [X0,X1] :
( ? [X10] :
( relation(X10)
& function(X10)
& complements_of_subsets(the_carrier(X0),X1) = relation_dom(X10)
& ! [X11] :
( ! [X12] :
( apply(X10,X11) = subset_complement(the_carrier(X0),X12)
| X11 != X12
| ~ element(X12,powerset(the_carrier(X0))) )
| ~ in(X11,complements_of_subsets(the_carrier(X0),X1)) ) )
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(definition_folding,[],[f964,f1279,f1278]) ).
fof(f1281,definition,
! [X4,X0,X2] :
( ? [X6] :
( subset_complement(the_carrier(X0),X6) != X4
& X6 = X2
& element(X6,powerset(the_carrier(X0))) )
| ~ sP50(X4,X0,X2) ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f1282,plain,
? [X0,X1] :
( ! [X10] :
( ~ relation(X10)
| ~ function(X10)
| relation_dom(X10) != X1
| ? [X11] :
( ? [X12] :
( apply(X10,X11) != subset_complement(the_carrier(X0),X12)
& X11 = X12
& element(X12,powerset(the_carrier(X0))) )
& in(X11,X1) ) )
& ! [X2,X3,X4] :
( X3 = X4
| ~ in(X2,X1)
| ? [X5] :
( subset_complement(the_carrier(X0),X5) != X3
& X5 = X2
& element(X5,powerset(the_carrier(X0))) )
| sP50(X4,X0,X2) )
& ! [X7] :
( ~ in(X7,X1)
| ? [X8] :
! [X9] :
( subset_complement(the_carrier(X0),X9) = X8
| X7 != X9
| ~ element(X9,powerset(the_carrier(X0))) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(definition_folding,[],[f966,f1281]) ).
fof(f1476,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = complements_of_subsets(X0,X1)
| ? [X3] :
( ( ~ in(subset_complement(X0,X3),X1)
| ~ in(X3,X2) )
& ( in(subset_complement(X0,X3),X1)
| in(X3,X2) )
& element(X3,powerset(X0)) ) )
& ( ! [X3] :
( ( ( in(X3,X2)
| ~ in(subset_complement(X0,X3),X1) )
& ( in(subset_complement(X0,X3),X1)
| ~ in(X3,X2) ) )
| ~ element(X3,powerset(X0)) )
| complements_of_subsets(X0,X1) != X2 ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(nnf_transformation,[],[f728]) ).
fof(f1477,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = complements_of_subsets(X0,X1)
| ? [X3] :
( ( ~ in(subset_complement(X0,X3),X1)
| ~ in(X3,X2) )
& ( in(subset_complement(X0,X3),X1)
| in(X3,X2) )
& element(X3,powerset(X0)) ) )
& ( ! [X3] :
( ( ( in(X3,X2)
| ~ in(subset_complement(X0,X3),X1) )
& ( in(subset_complement(X0,X3),X1)
| ~ in(X3,X2) ) )
| ~ element(X3,powerset(X0)) )
| complements_of_subsets(X0,X1) != X2 ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f1476]) ).
fof(f1478,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = complements_of_subsets(X0,X1)
| ? [X3] :
( ( ~ in(subset_complement(X0,X3),X1)
| ~ in(X3,X2) )
& ( in(subset_complement(X0,X3),X1)
| in(X3,X2) )
& element(X3,powerset(X0)) ) )
& ( ! [X4] :
( ( ( in(X4,X2)
| ~ in(subset_complement(X0,X4),X1) )
& ( in(subset_complement(X0,X4),X1)
| ~ in(X4,X2) ) )
| ~ element(X4,powerset(X0)) )
| complements_of_subsets(X0,X1) != X2 ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(rectify,[],[f1477]) ).
fof(f1479,plain,
! [X0,X1] :
( ! [X2] :
( ( ( X2 = complements_of_subsets(X0,X1)
| ( ( ~ in(subset_complement(X0,sK152(X0,X1,X2)),X1)
| ~ in(sK152(X0,X1,X2),X2) )
& ( in(subset_complement(X0,sK152(X0,X1,X2)),X1)
| in(sK152(X0,X1,X2),X2) )
& element(sK152(X0,X1,X2),powerset(X0)) ) )
& ( ! [X4] :
( ( ( in(X4,X2)
| ~ in(subset_complement(X0,X4),X1) )
& ( in(subset_complement(X0,X4),X1)
| ~ in(X4,X2) ) )
| ~ element(X4,powerset(X0)) )
| complements_of_subsets(X0,X1) != X2 ) )
| ~ element(X2,powerset(powerset(X0))) )
| ~ element(X1,powerset(powerset(X0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK152]),skolemize(X3,sK152(X0,X1,X2))],[f1478]) ).
fof(f1666,plain,
! [X1,X0] :
( ? [X7] :
! [X8] :
( ( in(X8,X7)
| ! [X9] :
( ~ in(X9,X1)
| ~ in(X9,X1)
| ? [X10] :
( subset_complement(the_carrier(X0),X10) != X8
& X9 = X10
& element(X10,powerset(the_carrier(X0))) ) ) )
& ( ? [X9] :
( in(X9,X1)
& in(X9,X1)
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X8
| X9 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) )
| ~ in(X8,X7) ) )
| ~ sP35(X1,X0) ),
inference(nnf_transformation,[],[f1256]) ).
fof(f1667,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ! [X4] :
( ~ in(X4,X0)
| ~ in(X4,X0)
| ? [X5] :
( subset_complement(the_carrier(X1),X5) != X3
& X4 = X5
& element(X5,powerset(the_carrier(X1))) ) ) )
& ( ? [X6] :
( in(X6,X0)
& in(X6,X0)
& ! [X7] :
( subset_complement(the_carrier(X1),X7) = X3
| X6 != X7
| ~ element(X7,powerset(the_carrier(X1))) ) )
| ~ in(X3,X2) ) )
| ~ sP35(X0,X1) ),
inference(rectify,[],[f1666]) ).
fof(f1668,plain,
! [X0,X1] :
( ! [X3] :
( ( in(X3,sK326(X0,X1))
| ! [X4] :
( ~ in(X4,X0)
| ~ in(X4,X0)
| ( subset_complement(the_carrier(X1),sK327(X1,X3,X4)) != X3
& sK327(X1,X3,X4) = X4
& element(sK327(X1,X3,X4),powerset(the_carrier(X1))) ) ) )
& ( ( in(sK328(X0,X1,X3),X0)
& in(sK328(X0,X1,X3),X0)
& ! [X7] :
( subset_complement(the_carrier(X1),X7) = X3
| sK328(X0,X1,X3) != X7
| ~ element(X7,powerset(the_carrier(X1))) ) )
| ~ in(X3,sK326(X0,X1)) ) )
| ~ sP35(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK326,sK327,sK328]),skolemize(X2,sK326(X0,X1)),skolemize(X5,sK327(X1,X3,X4)),skolemize(X6,sK328(X0,X1,X3))],[f1667]) ).
fof(f1669,plain,
! [X0,X1] :
( sP35(X1,X0)
| ( sK330(X0,X1) != sK331(X0,X1)
& in(sK329(X0,X1),X1)
& ! [X5] :
( subset_complement(the_carrier(X0),X5) = sK330(X0,X1)
| sK329(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& in(sK329(X0,X1),X1)
& ! [X6] :
( subset_complement(the_carrier(X0),X6) = sK331(X0,X1)
| sK329(X0,X1) != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK329,sK330,sK331]),skolemize(X2,sK329(X0,X1)),skolemize(X3,sK330(X0,X1)),skolemize(X4,sK331(X0,X1))],[f1257]) ).
fof(f1762,plain,
! [X1,X0] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( X3 = subset_complement(the_carrier(X0),X5)
| X2 != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& ! [X6] :
( X4 = subset_complement(the_carrier(X0),X6)
| X2 != X6
| ~ element(X6,powerset(the_carrier(X0))) ) )
| ~ sP49(X1,X0) ),
inference(nnf_transformation,[],[f1279]) ).
fof(f1763,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,complements_of_subsets(the_carrier(X1),X0))
& ! [X5] :
( subset_complement(the_carrier(X1),X5) = X3
| X2 != X5
| ~ element(X5,powerset(the_carrier(X1))) )
& ! [X6] :
( subset_complement(the_carrier(X1),X6) = X4
| X2 != X6
| ~ element(X6,powerset(the_carrier(X1))) ) )
| ~ sP49(X0,X1) ),
inference(rectify,[],[f1762]) ).
fof(f1764,plain,
! [X0,X1] :
( ( sK421(X0,X1) != sK422(X0,X1)
& in(sK420(X0,X1),complements_of_subsets(the_carrier(X1),X0))
& ! [X5] :
( subset_complement(the_carrier(X1),X5) = sK421(X0,X1)
| sK420(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X1))) )
& ! [X6] :
( subset_complement(the_carrier(X1),X6) = sK422(X0,X1)
| sK420(X0,X1) != X6
| ~ element(X6,powerset(the_carrier(X1))) ) )
| ~ sP49(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK420,sK421,sK422]),skolemize(X2,sK420(X0,X1)),skolemize(X3,sK421(X0,X1)),skolemize(X4,sK422(X0,X1))],[f1763]) ).
fof(f1765,plain,
! [X1,X0] :
( ? [X7] :
( in(X7,complements_of_subsets(the_carrier(X0),X1))
& ! [X8] :
? [X9] :
( subset_complement(the_carrier(X0),X9) != X8
& X7 = X9
& element(X9,powerset(the_carrier(X0))) ) )
| ~ sP48(X1,X0) ),
inference(nnf_transformation,[],[f1278]) ).
fof(f1766,plain,
! [X0,X1] :
( ? [X2] :
( in(X2,complements_of_subsets(the_carrier(X1),X0))
& ! [X3] :
? [X4] :
( subset_complement(the_carrier(X1),X4) != X3
& X2 = X4
& element(X4,powerset(the_carrier(X1))) ) )
| ~ sP48(X0,X1) ),
inference(rectify,[],[f1765]) ).
fof(f1767,plain,
! [X0,X1] :
( ( in(sK423(X0,X1),complements_of_subsets(the_carrier(X1),X0))
& ! [X3] :
( subset_complement(the_carrier(X1),sK424(X0,X1,X3)) != X3
& sK423(X0,X1) = sK424(X0,X1,X3)
& element(sK424(X0,X1,X3),powerset(the_carrier(X1))) ) )
| ~ sP48(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK423,sK424]),skolemize(X2,sK423(X0,X1)),skolemize(X4,sK424(X0,X1,X3))],[f1766]) ).
fof(f1768,plain,
! [X0,X1] :
( ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = complements_of_subsets(the_carrier(X0),X1)
& ! [X3] :
( ! [X4] :
( apply(X2,X3) = subset_complement(the_carrier(X0),X4)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X3,complements_of_subsets(the_carrier(X0),X1)) ) )
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(rectify,[],[f1280]) ).
fof(f1769,plain,
! [X0,X1] :
( ( relation(sK425(X0,X1))
& function(sK425(X0,X1))
& complements_of_subsets(the_carrier(X0),X1) = relation_dom(sK425(X0,X1))
& ! [X3] :
( ! [X4] :
( subset_complement(the_carrier(X0),X4) = apply(sK425(X0,X1),X3)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X3,complements_of_subsets(the_carrier(X0),X1)) ) )
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK425]),skolemize(X2,sK425(X0,X1))],[f1768]) ).
fof(f1773,plain,
? [X0,X1] :
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != X1
| ? [X3] :
( ? [X4] :
( apply(X2,X3) != subset_complement(the_carrier(X0),X4)
& X3 = X4
& element(X4,powerset(the_carrier(X0))) )
& in(X3,X1) ) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ in(X5,X1)
| ? [X8] :
( subset_complement(the_carrier(X0),X8) != X6
& X5 = X8
& element(X8,powerset(the_carrier(X0))) )
| sP50(X7,X0,X5) )
& ! [X9] :
( ~ in(X9,X1)
| ? [X10] :
! [X11] :
( subset_complement(the_carrier(X0),X11) = X10
| X9 != X11
| ~ element(X11,powerset(the_carrier(X0))) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(rectify,[],[f1282]) ).
fof(f1774,plain,
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK428
| ( apply(X2,sK429(X2)) != subset_complement(the_carrier(sK427),sK430(X2))
& sK429(X2) = sK430(X2)
& element(sK430(X2),powerset(the_carrier(sK427)))
& in(sK429(X2),sK428) ) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ in(X5,sK428)
| ( subset_complement(the_carrier(sK427),sK431(X5,X6)) != X6
& sK431(X5,X6) = X5
& element(sK431(X5,X6),powerset(the_carrier(sK427))) )
| sP50(X7,sK427,X5) )
& ! [X9] :
( ~ in(X9,sK428)
| ! [X11] :
( sK432(X9) = subset_complement(the_carrier(sK427),X11)
| X9 != X11
| ~ element(X11,powerset(the_carrier(sK427))) ) )
& one_sorted_str(sK427)
& element(sK428,powerset(powerset(the_carrier(sK427)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK427,sK428,sK429,sK430,sK431,sK432]),skolemize(X0,sK427),skolemize(X1,sK428),skolemize(X3,sK429(X2)),skolemize(X4,sK430(X2)),skolemize(X8,sK431(X5,X6)),skolemize(X10,sK432(X9))],[f1773]) ).
fof(f2273,plain,
! [X2,X0,X1,X4] :
( in(subset_complement(X0,X4),X1)
| ~ in(X4,X2)
| ~ element(X4,powerset(X0))
| complements_of_subsets(X0,X1) != X2
| ~ element(X2,powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f2290,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f745]) ).
fof(f2293,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f747]) ).
fof(f2305,plain,
! [X0,X1] :
( element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f762]) ).
fof(f2471,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f846]) ).
fof(f2473,plain,
! [X0,X1] :
( complements_of_subsets(X0,complements_of_subsets(X0,X1)) = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f848]) ).
fof(f2614,plain,
! [X2,X0,X1] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[],[f889]) ).
fof(f2882,plain,
! [X3,X0,X1,X7] :
( subset_complement(the_carrier(X1),X7) = X3
| sK328(X0,X1,X3) != X7
| ~ element(X7,powerset(the_carrier(X1)))
| ~ in(X3,sK326(X0,X1))
| ~ sP35(X0,X1) ),
inference(cnf_transformation,[],[f1668]) ).
fof(f2884,plain,
! [X3,X0,X1] :
( in(sK328(X0,X1,X3),X0)
| ~ in(X3,sK326(X0,X1))
| ~ sP35(X0,X1) ),
inference(cnf_transformation,[],[f1668]) ).
fof(f2886,plain,
! [X3,X0,X1,X4] :
( in(X3,sK326(X0,X1))
| ~ in(X4,X0)
| ~ in(X4,X0)
| sK327(X1,X3,X4) = X4
| ~ sP35(X0,X1) ),
inference(cnf_transformation,[],[f1668]) ).
fof(f2887,plain,
! [X3,X0,X1,X4] :
( in(X3,sK326(X0,X1))
| ~ in(X4,X0)
| ~ in(X4,X0)
| subset_complement(the_carrier(X1),sK327(X1,X3,X4)) != X3
| ~ sP35(X0,X1) ),
inference(cnf_transformation,[],[f1668]) ).
fof(f2888,plain,
! [X0,X1,X6] :
( sP35(X1,X0)
| subset_complement(the_carrier(X0),X6) = sK331(X0,X1)
| sK329(X0,X1) != X6
| ~ element(X6,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1669]) ).
fof(f2889,plain,
! [X0,X1] :
( sP35(X1,X0)
| in(sK329(X0,X1),X1)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1669]) ).
fof(f2890,plain,
! [X0,X1,X5] :
( sP35(X1,X0)
| subset_complement(the_carrier(X0),X5) = sK330(X0,X1)
| sK329(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1669]) ).
fof(f2892,plain,
! [X0,X1] :
( sP35(X1,X0)
| sK330(X0,X1) != sK331(X0,X1)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1669]) ).
fof(f3055,plain,
! [X0,X1,X6] :
( subset_complement(the_carrier(X1),X6) = sK422(X0,X1)
| sK420(X0,X1) != X6
| ~ element(X6,powerset(the_carrier(X1)))
| ~ sP49(X0,X1) ),
inference(cnf_transformation,[],[f1764]) ).
fof(f3056,plain,
! [X0,X1,X5] :
( subset_complement(the_carrier(X1),X5) = sK421(X0,X1)
| sK420(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X1)))
| ~ sP49(X0,X1) ),
inference(cnf_transformation,[],[f1764]) ).
fof(f3057,plain,
! [X0,X1] :
( in(sK420(X0,X1),complements_of_subsets(the_carrier(X1),X0))
| ~ sP49(X0,X1) ),
inference(cnf_transformation,[],[f1764]) ).
fof(f3058,plain,
! [X0,X1] :
( sK421(X0,X1) != sK422(X0,X1)
| ~ sP49(X0,X1) ),
inference(cnf_transformation,[],[f1764]) ).
fof(f3059,plain,
! [X3,X0,X1] :
( element(sK424(X0,X1,X3),powerset(the_carrier(X1)))
| ~ sP48(X0,X1) ),
inference(cnf_transformation,[],[f1767]) ).
fof(f3060,plain,
! [X3,X0,X1] :
( sK423(X0,X1) = sK424(X0,X1,X3)
| ~ sP48(X0,X1) ),
inference(cnf_transformation,[],[f1767]) ).
fof(f3061,plain,
! [X3,X0,X1] :
( subset_complement(the_carrier(X1),sK424(X0,X1,X3)) != X3
| ~ sP48(X0,X1) ),
inference(cnf_transformation,[],[f1767]) ).
fof(f3063,plain,
! [X3,X0,X1,X4] :
( subset_complement(the_carrier(X0),X4) = apply(sK425(X0,X1),X3)
| X3 != X4
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X3,complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3064,plain,
! [X0,X1] :
( complements_of_subsets(the_carrier(X0),X1) = relation_dom(sK425(X0,X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3065,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| function(sK425(X0,X1)) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3066,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| relation(sK425(X0,X1)) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3070,plain,
element(sK428,powerset(powerset(the_carrier(sK427)))),
inference(cnf_transformation,[],[f1774]) ).
fof(f3071,plain,
one_sorted_str(sK427),
inference(cnf_transformation,[],[f1774]) ).
fof(f3072,plain,
! [X11,X9] :
( ~ in(X9,sK428)
| sK432(X9) = subset_complement(the_carrier(sK427),X11)
| X9 != X11
| ~ element(X11,powerset(the_carrier(sK427))) ),
inference(cnf_transformation,[],[f1774]) ).
fof(f3076,plain,
! [X2] :
( relation_dom(X2) != sK428
| ~ function(X2)
| ~ relation(X2)
| in(sK429(X2),sK428) ),
inference(cnf_transformation,[],[f1774]) ).
fof(f3077,plain,
! [X2] :
( relation_dom(X2) != sK428
| ~ function(X2)
| ~ relation(X2)
| element(sK430(X2),powerset(the_carrier(sK427))) ),
inference(cnf_transformation,[],[f1774]) ).
fof(f3078,plain,
! [X2] :
( relation_dom(X2) != sK428
| ~ function(X2)
| ~ relation(X2)
| sK429(X2) = sK430(X2) ),
inference(cnf_transformation,[],[f1774]) ).
fof(f3079,plain,
! [X2] :
( apply(X2,sK429(X2)) != subset_complement(the_carrier(sK427),sK430(X2))
| ~ function(X2)
| relation_dom(X2) != sK428
| ~ relation(X2) ),
inference(cnf_transformation,[],[f1774]) ).
fof(f3162,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1024]) ).
fof(f3311,plain,
! [X2,X0,X1] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(cnf_transformation,[],[f1133]) ).
fof(f3913,plain,
! [X0,X1,X4] :
( in(subset_complement(X0,X4),X1)
| ~ in(X4,complements_of_subsets(X0,X1))
| ~ element(X4,powerset(X0))
| ~ element(complements_of_subsets(X0,X1),powerset(powerset(X0)))
| ~ element(X1,powerset(powerset(X0))) ),
inference(equality_resolution,[],[f2273]) ).
fof(f3966,plain,
! [X3,X0,X1] :
( subset_complement(the_carrier(X1),sK328(X0,X1,X3)) = X3
| ~ element(sK328(X0,X1,X3),powerset(the_carrier(X1)))
| ~ in(X3,sK326(X0,X1))
| ~ sP35(X0,X1) ),
inference(equality_resolution,[],[f2882]) ).
fof(f3967,plain,
! [X0,X1] :
( sP35(X1,X0)
| sK330(X0,X1) = subset_complement(the_carrier(X0),sK329(X0,X1))
| ~ element(sK329(X0,X1),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f2890]) ).
fof(f3968,plain,
! [X0,X1] :
( sP35(X1,X0)
| sK331(X0,X1) = subset_complement(the_carrier(X0),sK329(X0,X1))
| ~ element(sK329(X0,X1),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f2888]) ).
fof(f4014,plain,
! [X0,X1] :
( sK421(X0,X1) = subset_complement(the_carrier(X1),sK420(X0,X1))
| ~ element(sK420(X0,X1),powerset(the_carrier(X1)))
| ~ sP49(X0,X1) ),
inference(equality_resolution,[],[f3056]) ).
fof(f4015,plain,
! [X0,X1] :
( sK422(X0,X1) = subset_complement(the_carrier(X1),sK420(X0,X1))
| ~ element(sK420(X0,X1),powerset(the_carrier(X1)))
| ~ sP49(X0,X1) ),
inference(equality_resolution,[],[f3055]) ).
fof(f4016,plain,
! [X0,X1,X4] :
( subset_complement(the_carrier(X0),X4) = apply(sK425(X0,X1),X4)
| ~ element(X4,powerset(the_carrier(X0)))
| ~ in(X4,complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f3063]) ).
fof(f4017,plain,
! [X11] :
( subset_complement(the_carrier(sK427),X11) = sK432(X11)
| ~ in(X11,sK428)
| ~ element(X11,powerset(the_carrier(sK427))) ),
inference(equality_resolution,[],[f3072]) ).
fof(f4047,plain,
! [X3,X0,X1,X4] :
( in(X3,sK326(X0,X1))
| ~ in(X4,X0)
| subset_complement(the_carrier(X1),sK327(X1,X3,X4)) != X3
| ~ sP35(X0,X1) ),
inference(duplicate_literal_removal,[],[f2887]) ).
fof(f4048,plain,
! [X3,X0,X1,X4] :
( in(X3,sK326(X0,X1))
| ~ in(X4,X0)
| sK327(X1,X3,X4) = X4
| ~ sP35(X0,X1) ),
inference(duplicate_literal_removal,[],[f2886]) ).
fof(f4290,plain,
( sP35(sK428,sK427)
| in(sK329(sK427,sK428),sK428)
| ~ one_sorted_str(sK427) ),
inference(resolution,[],[f3070,f2889]) ).
fof(f4292,plain,
( sP35(sK428,sK427)
| sK330(sK427,sK428) != sK331(sK427,sK428)
| ~ one_sorted_str(sK427) ),
inference(resolution,[],[f3070,f2892]) ).
fof(f4302,plain,
( sP35(sK428,sK427)
| sK330(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ element(sK329(sK427,sK428),powerset(the_carrier(sK427)))
| ~ one_sorted_str(sK427) ),
inference(resolution,[],[f3070,f3967]) ).
fof(f4303,plain,
( sP35(sK428,sK427)
| sK331(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ element(sK329(sK427,sK428),powerset(the_carrier(sK427)))
| ~ one_sorted_str(sK427) ),
inference(resolution,[],[f3070,f3968]) ).
fof(f4313,plain,
element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427)))),
inference(resolution,[],[f3070,f2305]) ).
fof(f4314,plain,
sK428 = complements_of_subsets(the_carrier(sK427),complements_of_subsets(the_carrier(sK427),sK428)),
inference(resolution,[],[f3070,f2473]) ).
fof(f4357,plain,
! [X0] :
( element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,sK428) ),
inference(resolution,[],[f3070,f3311]) ).
fof(f4486,definition,
( spl472_34
<=> element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427)))) ),
introduced(definition,[new_symbols(definition,[spl472_34])],[avatar_definition]) ).
fof(f4487,plain,
( element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| ~ spl472_34 ),
inference(avatar_component_clause,[],[f4486]) ).
fof(f4497,plain,
spl472_34,
inference(avatar_split_clause,[],[f4313,f4486]) ).
fof(f4501,plain,
( sP35(sK428,sK427)
| sK331(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ element(sK329(sK427,sK428),powerset(the_carrier(sK427))) ),
inference(forward_subsumption_resolution,[],[f4303,f3071]) ).
fof(f4502,plain,
( sP35(sK428,sK427)
| sK330(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ element(sK329(sK427,sK428),powerset(the_carrier(sK427))) ),
inference(forward_subsumption_resolution,[],[f4302,f3071]) ).
fof(f4527,plain,
( sP35(sK428,sK427)
| sK330(sK427,sK428) != sK331(sK427,sK428) ),
inference(forward_subsumption_resolution,[],[f4292,f3071]) ).
fof(f4529,plain,
( sP35(sK428,sK427)
| in(sK329(sK427,sK428),sK428) ),
inference(forward_subsumption_resolution,[],[f4290,f3071]) ).
fof(f4610,definition,
( spl472_56
<=> element(sK329(sK427,sK428),powerset(the_carrier(sK427))) ),
introduced(definition,[new_symbols(definition,[spl472_56])],[avatar_definition]) ).
fof(f4612,plain,
( ~ element(sK329(sK427,sK428),powerset(the_carrier(sK427)))
| spl472_56 ),
inference(avatar_component_clause,[],[f4610]) ).
fof(f4614,definition,
( spl472_57
<=> sK331(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428)) ),
introduced(definition,[new_symbols(definition,[spl472_57])],[avatar_definition]) ).
fof(f4616,plain,
( sK331(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ spl472_57 ),
inference(avatar_component_clause,[],[f4614]) ).
fof(f4618,definition,
( spl472_58
<=> sP35(sK428,sK427) ),
introduced(definition,[new_symbols(definition,[spl472_58])],[avatar_definition]) ).
fof(f4620,plain,
( sP35(sK428,sK427)
| ~ spl472_58 ),
inference(avatar_component_clause,[],[f4618]) ).
fof(f4621,plain,
( ~ spl472_56
| spl472_57
| spl472_58 ),
inference(avatar_split_clause,[],[f4501,f4618,f4614,f4610]) ).
fof(f4623,definition,
( spl472_59
<=> sK330(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428)) ),
introduced(definition,[new_symbols(definition,[spl472_59])],[avatar_definition]) ).
fof(f4625,plain,
( sK330(sK427,sK428) = subset_complement(the_carrier(sK427),sK329(sK427,sK428))
| ~ spl472_59 ),
inference(avatar_component_clause,[],[f4623]) ).
fof(f4626,plain,
( ~ spl472_56
| spl472_59
| spl472_58 ),
inference(avatar_split_clause,[],[f4502,f4618,f4623,f4610]) ).
fof(f4683,definition,
( spl472_72
<=> sK330(sK427,sK428) = sK331(sK427,sK428) ),
introduced(definition,[new_symbols(definition,[spl472_72])],[avatar_definition]) ).
fof(f4685,plain,
( sK330(sK427,sK428) != sK331(sK427,sK428)
| spl472_72 ),
inference(avatar_component_clause,[],[f4683]) ).
fof(f4686,plain,
( ~ spl472_72
| spl472_58 ),
inference(avatar_split_clause,[],[f4527,f4618,f4683]) ).
fof(f4688,definition,
( spl472_73
<=> in(sK329(sK427,sK428),sK428) ),
introduced(definition,[new_symbols(definition,[spl472_73])],[avatar_definition]) ).
fof(f4690,plain,
( in(sK329(sK427,sK428),sK428)
| ~ spl472_73 ),
inference(avatar_component_clause,[],[f4688]) ).
fof(f4692,plain,
( spl472_73
| spl472_58 ),
inference(avatar_split_clause,[],[f4529,f4618,f4688]) ).
fof(f4833,plain,
( in(sK420(complements_of_subsets(the_carrier(sK427),sK428),sK427),sK428)
| ~ sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427) ),
inference(superposition,[],[f3057,f4314]) ).
fof(f4879,definition,
( spl472_96
<=> sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427) ),
introduced(definition,[new_symbols(definition,[spl472_96])],[avatar_definition]) ).
fof(f4880,plain,
( sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ spl472_96 ),
inference(avatar_component_clause,[],[f4879]) ).
fof(f4881,plain,
( ~ sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| spl472_96 ),
inference(avatar_component_clause,[],[f4879]) ).
fof(f4883,definition,
( spl472_97
<=> in(sK420(complements_of_subsets(the_carrier(sK427),sK428),sK427),sK428) ),
introduced(definition,[new_symbols(definition,[spl472_97])],[avatar_definition]) ).
fof(f4885,plain,
( in(sK420(complements_of_subsets(the_carrier(sK427),sK428),sK427),sK428)
| ~ spl472_97 ),
inference(avatar_component_clause,[],[f4883]) ).
fof(f4886,plain,
( ~ spl472_96
| spl472_97 ),
inference(avatar_split_clause,[],[f4833,f4883,f4879]) ).
fof(f4959,plain,
! [X0] :
( sK422(X0,sK427) = sK432(sK420(X0,sK427))
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427)))
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428)
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427))) ),
inference(superposition,[],[f4015,f4017]) ).
fof(f4960,plain,
! [X0] :
( sK432(sK420(X0,sK427)) = sK421(X0,sK427)
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427)))
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428)
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427))) ),
inference(superposition,[],[f4014,f4017]) ).
fof(f4964,plain,
! [X0] :
( element(sK432(X0),powerset(the_carrier(sK427)))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,sK428)
| ~ element(X0,powerset(the_carrier(sK427))) ),
inference(superposition,[],[f2293,f4017]) ).
fof(f4974,plain,
! [X0] :
( element(sK432(X0),powerset(the_carrier(sK427)))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,sK428) ),
inference(duplicate_literal_removal,[],[f4964]) ).
fof(f4976,plain,
! [X0] :
( sK432(sK420(X0,sK427)) = sK421(X0,sK427)
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427)))
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(duplicate_literal_removal,[],[f4960]) ).
fof(f4977,plain,
! [X0] :
( sK422(X0,sK427) = sK432(sK420(X0,sK427))
| ~ element(sK420(X0,sK427),powerset(the_carrier(sK427)))
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(duplicate_literal_removal,[],[f4959]) ).
fof(f5014,plain,
! [X0] :
( element(sK432(X0),powerset(the_carrier(sK427)))
| ~ in(X0,sK428) ),
inference(forward_subsumption_resolution,[],[f4974,f4357]) ).
fof(f5018,plain,
! [X0] :
( sK432(sK420(X0,sK427)) = sK421(X0,sK427)
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(forward_subsumption_resolution,[],[f4976,f4357]) ).
fof(f5019,plain,
! [X0] :
( sK422(X0,sK427) = sK432(sK420(X0,sK427))
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(forward_subsumption_resolution,[],[f4977,f4357]) ).
fof(f6350,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),X1) = set_difference(cast_as_carrier_subset(X0),X1)
| ~ element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f2614,f3162]) ).
fof(f6353,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),X1) = set_difference(cast_as_carrier_subset(X0),X1)
| ~ element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(duplicate_literal_removal,[],[f6350]) ).
fof(f6358,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),X1) = set_difference(cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f6353,f2290]) ).
fof(f6401,plain,
! [X2,X0,X1] :
( set_difference(cast_as_carrier_subset(X0),sK424(X1,X0,X2)) != X2
| ~ sP48(X1,X0)
| ~ element(sK424(X1,X0,X2),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f3061,f6358]) ).
fof(f6466,plain,
! [X2,X0,X1] :
( set_difference(cast_as_carrier_subset(X0),sK424(X1,X0,X2)) != X2
| ~ sP48(X1,X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f6401,f3059]) ).
fof(f10615,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427)))) ),
inference(superposition,[],[f4314,f3064]) ).
fof(f10619,plain,
! [X0,X1] :
( element(relation_dom(sK425(X0,X1)),powerset(powerset(the_carrier(X0))))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(superposition,[],[f2305,f3064]) ).
fof(f10631,plain,
! [X0,X1] :
( element(relation_dom(sK425(X0,X1)),powerset(powerset(the_carrier(X0))))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0) ),
inference(duplicate_literal_removal,[],[f10619]) ).
fof(f10644,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f10615,f4881]) ).
fof(f11021,plain,
! [X2,X0,X1] :
( set_difference(cast_as_carrier_subset(X1),sK423(X0,X1)) != X2
| ~ sP48(X0,X1)
| ~ one_sorted_str(X1)
| ~ sP48(X0,X1) ),
inference(superposition,[],[f6466,f3060]) ).
fof(f11025,plain,
! [X2,X0,X1] :
( set_difference(cast_as_carrier_subset(X1),sK423(X0,X1)) != X2
| ~ sP48(X0,X1)
| ~ one_sorted_str(X1) ),
inference(duplicate_literal_removal,[],[f11021]) ).
fof(f11033,plain,
! [X0,X1] :
( ~ sP48(X0,X1)
| ~ one_sorted_str(X1) ),
inference(equality_resolution,[],[f11025]) ).
fof(f12785,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),sK429(sK425(X0,X1))) != subset_complement(the_carrier(sK427),sK430(sK425(X0,X1)))
| ~ function(sK425(X0,X1))
| relation_dom(sK425(X0,X1)) != sK428
| ~ relation(sK425(X0,X1))
| ~ element(sK429(sK425(X0,X1)),powerset(the_carrier(X0)))
| ~ in(sK429(sK425(X0,X1)),complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(superposition,[],[f3079,f4016]) ).
fof(f12786,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),sK429(sK425(X0,X1))) != subset_complement(the_carrier(sK427),sK430(sK425(X0,X1)))
| relation_dom(sK425(X0,X1)) != sK428
| ~ relation(sK425(X0,X1))
| ~ element(sK429(sK425(X0,X1)),powerset(the_carrier(X0)))
| ~ in(sK429(sK425(X0,X1)),complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f12785,f3065]) ).
fof(f12820,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),sK429(sK425(X0,X1))) != subset_complement(the_carrier(sK427),sK430(sK425(X0,X1)))
| relation_dom(sK425(X0,X1)) != sK428
| ~ element(sK429(sK425(X0,X1)),powerset(the_carrier(X0)))
| ~ in(sK429(sK425(X0,X1)),complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| sP48(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f12786,f3066]) ).
fof(f12845,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),sK429(sK425(X0,X1))) != subset_complement(the_carrier(sK427),sK430(sK425(X0,X1)))
| relation_dom(sK425(X0,X1)) != sK428
| ~ element(sK429(sK425(X0,X1)),powerset(the_carrier(X0)))
| ~ in(sK429(sK425(X0,X1)),complements_of_subsets(the_carrier(X0),X1))
| sP49(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f12820,f11033]) ).
fof(f12955,plain,
( ! [X0] :
( element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428)) )
| ~ spl472_34 ),
inference(resolution,[],[f4487,f3311]) ).
fof(f14067,plain,
( sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34 ),
inference(resolution,[],[f3066,f4487]) ).
fof(f14125,plain,
( sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f14067,f4881]) ).
fof(f14419,plain,
( sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34 ),
inference(resolution,[],[f3065,f4487]) ).
fof(f14478,plain,
( sP48(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ one_sorted_str(sK427)
| function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f14419,f4881]) ).
fof(f16298,plain,
! [X0] :
( sK422(X0,sK427) = sK421(X0,sK427)
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428)
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(superposition,[],[f5018,f5019]) ).
fof(f16301,plain,
! [X0] :
( sK422(X0,sK427) = sK421(X0,sK427)
| ~ sP49(X0,sK427)
| ~ in(sK420(X0,sK427),sK428) ),
inference(duplicate_literal_removal,[],[f16298]) ).
fof(f16304,plain,
! [X0] :
( ~ in(sK420(X0,sK427),sK428)
| ~ sP49(X0,sK427) ),
inference(forward_subsumption_resolution,[],[f16301,f3058]) ).
fof(f25807,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ one_sorted_str(sK427)
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f10644,f11033]) ).
fof(f25809,plain,
( ~ one_sorted_str(sK427)
| relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f14125,f11033]) ).
fof(f25810,plain,
( ~ one_sorted_str(sK427)
| function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f14478,f11033]) ).
fof(f25819,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f25807,f3071]) ).
fof(f25821,plain,
( relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f25809,f3071]) ).
fof(f25822,plain,
( function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f25810,f3071]) ).
fof(f25829,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_34
| spl472_96 ),
inference(forward_subsumption_resolution,[],[f25819,f4487]) ).
fof(f28892,definition,
( spl472_565
<=> sP49(sK428,sK427) ),
introduced(definition,[new_symbols(definition,[spl472_565])],[avatar_definition]) ).
fof(f28893,plain,
( sP49(sK428,sK427)
| ~ spl472_565 ),
inference(avatar_component_clause,[],[f28892]) ).
fof(f28894,plain,
( ~ sP49(sK428,sK427)
| spl472_565 ),
inference(avatar_component_clause,[],[f28892]) ).
fof(f31263,plain,
( ~ in(sK329(sK427,sK428),sK428)
| spl472_56 ),
inference(resolution,[],[f4612,f4357]) ).
fof(f32243,definition,
( spl472_879
<=> relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) ),
introduced(definition,[new_symbols(definition,[spl472_879])],[avatar_definition]) ).
fof(f32245,plain,
( relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_879 ),
inference(avatar_component_clause,[],[f32243]) ).
fof(f32248,definition,
( spl472_880
<=> function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) ),
introduced(definition,[new_symbols(definition,[spl472_880])],[avatar_definition]) ).
fof(f32250,plain,
( function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_880 ),
inference(avatar_component_clause,[],[f32248]) ).
fof(f32253,definition,
( spl472_881
<=> sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) ),
introduced(definition,[new_symbols(definition,[spl472_881])],[avatar_definition]) ).
fof(f32255,plain,
( sK428 = relation_dom(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_881 ),
inference(avatar_component_clause,[],[f32253]) ).
fof(f32258,plain,
( spl472_881
| ~ spl472_34
| spl472_96 ),
inference(avatar_split_clause,[],[f25829,f4879,f4486,f32253]) ).
fof(f32260,plain,
( spl472_879
| ~ spl472_34
| spl472_96 ),
inference(avatar_split_clause,[],[f25821,f4879,f4486,f32243]) ).
fof(f32263,plain,
( spl472_880
| ~ spl472_34
| spl472_96 ),
inference(avatar_split_clause,[],[f25822,f4879,f4486,f32248]) ).
fof(f32742,plain,
( sK330(sK427,sK428) = sK331(sK427,sK428)
| ~ spl472_57
| ~ spl472_59 ),
inference(superposition,[],[f4616,f4625]) ).
fof(f32794,plain,
( $false
| ~ spl472_57
| ~ spl472_59
| spl472_72 ),
inference(forward_subsumption_resolution,[],[f32742,f4685]) ).
fof(f32795,plain,
( ~ spl472_57
| ~ spl472_59
| spl472_72 ),
inference(avatar_contradiction_clause,[],[f32794]) ).
fof(f32936,plain,
( ! [X0] :
( subset_complement(the_carrier(sK427),sK328(sK428,sK427,X0)) = X0
| ~ element(sK328(sK428,sK427,X0),powerset(the_carrier(sK427)))
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(resolution,[],[f4620,f3966]) ).
fof(f32938,plain,
( ! [X0] :
( in(sK328(sK428,sK427,X0),sK428)
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(resolution,[],[f4620,f2884]) ).
fof(f32940,plain,
( ! [X0,X1] :
( sK327(sK427,X0,X1) = X1
| ~ in(X1,sK428)
| in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(resolution,[],[f4620,f4048]) ).
fof(f32941,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK427),sK327(sK427,X0,X1)) != X0
| ~ in(X1,sK428)
| in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(resolution,[],[f4620,f4047]) ).
fof(f33507,plain,
( sK428 = relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| ~ spl472_881 ),
inference(superposition,[],[f32255,f3064]) ).
fof(f33531,plain,
( sK428 != sK428
| ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| in(sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),sK428)
| ~ spl472_881 ),
inference(superposition,[],[f3076,f32255]) ).
fof(f33532,plain,
( sK428 != sK428
| ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| element(sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),powerset(the_carrier(sK427)))
| ~ spl472_881 ),
inference(superposition,[],[f3077,f32255]) ).
fof(f33533,plain,
( sK428 != sK428
| ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) = sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_881 ),
inference(superposition,[],[f3078,f32255]) ).
fof(f33548,plain,
( ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) = sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_881 ),
inference(trivial_inequality_removal,[],[f33533]) ).
fof(f33549,plain,
( ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| element(sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),powerset(the_carrier(sK427)))
| ~ spl472_881 ),
inference(trivial_inequality_removal,[],[f33532]) ).
fof(f33550,plain,
( ~ function(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| in(sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),sK428)
| ~ spl472_881 ),
inference(trivial_inequality_removal,[],[f33531]) ).
fof(f33562,plain,
( ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) = sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33548,f32250]) ).
fof(f33563,plain,
( ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| element(sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),powerset(the_carrier(sK427)))
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33549,f32250]) ).
fof(f33564,plain,
( ~ relation(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| in(sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),sK428)
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33550,f32250]) ).
fof(f33598,plain,
( sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))) = sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428)))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33562,f32245]) ).
fof(f33599,plain,
( element(sK430(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),powerset(the_carrier(sK427)))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33563,f32245]) ).
fof(f33600,plain,
( in(sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),sK428)
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33564,f32245]) ).
fof(f33631,plain,
( element(sK429(sK425(sK427,complements_of_subsets(the_carrier(sK427),sK428))),powerset(the_carrier(sK427)))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_demodulation,[],[f33599,f33598]) ).
fof(f33689,plain,
( in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(superposition,[],[f33600,f3064]) ).
fof(f33884,plain,
( sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))) = sK430(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(superposition,[],[f33598,f3064]) ).
fof(f34512,plain,
( sK428 = relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33507,f28894]) ).
fof(f34516,plain,
( in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33689,f28894]) ).
fof(f34534,plain,
( sK428 = relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34512,f11033]) ).
fof(f34535,plain,
( in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34516,f11033]) ).
fof(f34544,plain,
( sK428 = relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34534,f3071]) ).
fof(f34545,plain,
( in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34535,f3071]) ).
fof(f34552,plain,
( sK428 = relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| spl472_565
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34544,f3070]) ).
fof(f34553,plain,
( in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f34545,f3070]) ).
fof(f34709,definition,
( spl472_1010
<=> element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427))) ),
introduced(definition,[new_symbols(definition,[spl472_1010])],[avatar_definition]) ).
fof(f34711,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ spl472_1010 ),
inference(avatar_component_clause,[],[f34709]) ).
fof(f34719,definition,
( spl472_1011
<=> sP49(relation_dom(sK425(sK427,sK428)),sK427) ),
introduced(definition,[new_symbols(definition,[spl472_1011])],[avatar_definition]) ).
fof(f34720,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| spl472_1011 ),
inference(avatar_component_clause,[],[f34719]) ).
fof(f34723,definition,
( spl472_1012
<=> element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427)))) ),
introduced(definition,[new_symbols(definition,[spl472_1012])],[avatar_definition]) ).
fof(f34724,plain,
( element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| ~ spl472_1012 ),
inference(avatar_component_clause,[],[f34723]) ).
fof(f34725,plain,
( ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_1012 ),
inference(avatar_component_clause,[],[f34723]) ).
fof(f35190,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_96 ),
inference(superposition,[],[f4881,f3064]) ).
fof(f35197,plain,
( subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK422(sK428,sK427)
| ~ element(sK420(sK428,sK427),powerset(the_carrier(sK427)))
| ~ spl472_565 ),
inference(resolution,[],[f28893,f4015]) ).
fof(f35198,plain,
( subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK421(sK428,sK427)
| ~ element(sK420(sK428,sK427),powerset(the_carrier(sK427)))
| ~ spl472_565 ),
inference(resolution,[],[f28893,f4014]) ).
fof(f35203,definition,
( spl472_1039
<=> element(sK420(sK428,sK427),powerset(the_carrier(sK427))) ),
introduced(definition,[new_symbols(definition,[spl472_1039])],[avatar_definition]) ).
fof(f35205,plain,
( ~ element(sK420(sK428,sK427),powerset(the_carrier(sK427)))
| spl472_1039 ),
inference(avatar_component_clause,[],[f35203]) ).
fof(f35207,definition,
( spl472_1040
<=> subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK421(sK428,sK427) ),
introduced(definition,[new_symbols(definition,[spl472_1040])],[avatar_definition]) ).
fof(f35209,plain,
( subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK421(sK428,sK427)
| ~ spl472_1040 ),
inference(avatar_component_clause,[],[f35207]) ).
fof(f35210,plain,
( ~ spl472_1039
| spl472_1040
| ~ spl472_565 ),
inference(avatar_split_clause,[],[f35198,f28892,f35207,f35203]) ).
fof(f35212,definition,
( spl472_1041
<=> subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK422(sK428,sK427) ),
introduced(definition,[new_symbols(definition,[spl472_1041])],[avatar_definition]) ).
fof(f35214,plain,
( subset_complement(the_carrier(sK427),sK420(sK428,sK427)) = sK422(sK428,sK427)
| ~ spl472_1041 ),
inference(avatar_component_clause,[],[f35212]) ).
fof(f35215,plain,
( ~ spl472_1039
| spl472_1041
| ~ spl472_565 ),
inference(avatar_split_clause,[],[f35197,f28892,f35212,f35203]) ).
fof(f35287,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(superposition,[],[f33631,f3064]) ).
fof(f36181,plain,
( ! [X0] :
( sK432(sK328(sK428,sK427,X0)) = X0
| ~ in(sK328(sK428,sK427,X0),sK428)
| ~ element(sK328(sK428,sK427,X0),powerset(the_carrier(sK427)))
| ~ element(sK328(sK428,sK427,X0),powerset(the_carrier(sK427)))
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(superposition,[],[f4017,f32936]) ).
fof(f36221,plain,
( ! [X0] :
( sK432(sK328(sK428,sK427,X0)) = X0
| ~ in(sK328(sK428,sK427,X0),sK428)
| ~ element(sK328(sK428,sK427,X0),powerset(the_carrier(sK427)))
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(duplicate_literal_removal,[],[f36181]) ).
fof(f36235,plain,
( ! [X0] :
( ~ element(sK328(sK428,sK427,X0),powerset(the_carrier(sK427)))
| sK432(sK328(sK428,sK427,X0)) = X0
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f36221,f32938]) ).
fof(f36243,plain,
( ! [X0] :
( sK432(sK328(sK428,sK427,X0)) = X0
| ~ in(X0,sK326(sK428,sK427))
| ~ in(sK328(sK428,sK427,X0),sK428) )
| ~ spl472_58 ),
inference(resolution,[],[f36235,f4357]) ).
fof(f36252,plain,
( ! [X0] :
( sK432(sK328(sK428,sK427,X0)) = X0
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f36243,f32938]) ).
fof(f36253,plain,
( ! [X0] :
( element(X0,powerset(the_carrier(sK427)))
| ~ in(sK328(sK428,sK427,X0),sK428)
| ~ in(X0,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(superposition,[],[f5014,f36252]) ).
fof(f36256,plain,
( ! [X0] :
( ~ in(X0,sK326(sK428,sK427))
| element(X0,powerset(the_carrier(sK427))) )
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f36253,f32938]) ).
fof(f38023,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK427),X0) != X1
| ~ in(X0,sK428)
| in(X1,sK326(sK428,sK427))
| ~ in(X0,sK428)
| in(X1,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(superposition,[],[f32941,f32940]) ).
fof(f38026,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK427),X0) != X1
| ~ in(X0,sK428)
| in(X1,sK326(sK428,sK427)) )
| ~ spl472_58 ),
inference(duplicate_literal_removal,[],[f38023]) ).
fof(f38221,plain,
( ! [X0] :
( in(subset_complement(the_carrier(sK427),X0),sK326(sK428,sK427))
| ~ in(X0,sK428) )
| ~ spl472_58 ),
inference(equality_resolution,[],[f38026]) ).
fof(f38361,plain,
( ! [X0] :
( ~ in(subset_complement(the_carrier(sK427),X0),sK428)
| in(X0,sK326(sK428,sK427))
| ~ element(X0,powerset(the_carrier(sK427))) )
| ~ spl472_58 ),
inference(superposition,[],[f38221,f2471]) ).
fof(f42731,plain,
( ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| spl472_1012 ),
inference(resolution,[],[f34725,f10631]) ).
fof(f94061,plain,
( ! [X0] :
( in(X0,sK326(sK428,sK427))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| ~ element(sK428,powerset(powerset(the_carrier(sK427)))) )
| ~ spl472_58 ),
inference(resolution,[],[f38361,f3913]) ).
fof(f94206,plain,
( ! [X0] :
( in(X0,sK326(sK428,sK427))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428))
| ~ element(complements_of_subsets(the_carrier(sK427),sK428),powerset(powerset(the_carrier(sK427))))
| ~ element(sK428,powerset(powerset(the_carrier(sK427)))) )
| ~ spl472_58 ),
inference(duplicate_literal_removal,[],[f94061]) ).
fof(f94236,plain,
( ! [X0] :
( in(X0,sK326(sK428,sK427))
| ~ element(X0,powerset(the_carrier(sK427)))
| ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428))
| ~ element(sK428,powerset(powerset(the_carrier(sK427)))) )
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f94206,f2305]) ).
fof(f94251,plain,
( ! [X0] :
( in(X0,sK326(sK428,sK427))
| ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428))
| ~ element(sK428,powerset(powerset(the_carrier(sK427)))) )
| ~ spl472_34
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f94236,f12955]) ).
fof(f94259,plain,
( ! [X0] :
( ~ in(X0,complements_of_subsets(the_carrier(sK427),sK428))
| in(X0,sK326(sK428,sK427)) )
| ~ spl472_34
| ~ spl472_58 ),
inference(forward_subsumption_resolution,[],[f94251,f3070]) ).
fof(f94804,plain,
( in(sK420(sK428,sK427),sK326(sK428,sK427))
| ~ sP49(sK428,sK427)
| ~ spl472_34
| ~ spl472_58 ),
inference(resolution,[],[f94259,f3057]) ).
fof(f94823,plain,
( in(sK420(sK428,sK427),sK326(sK428,sK427))
| ~ spl472_34
| ~ spl472_58
| ~ spl472_565 ),
inference(forward_subsumption_resolution,[],[f94804,f28893]) ).
fof(f94938,plain,
( sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))) = sK430(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f33884,f28894]) ).
fof(f94939,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_96
| spl472_565 ),
inference(forward_subsumption_resolution,[],[f35190,f28894]) ).
fof(f94940,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f35287,f28894]) ).
fof(f94948,plain,
( sP49(sK428,sK427)
| sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| spl472_1012 ),
inference(forward_subsumption_resolution,[],[f42731,f3070]) ).
fof(f95227,plain,
( sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))) = sK430(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f94938,f11033]) ).
fof(f95228,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_96
| spl472_565 ),
inference(forward_subsumption_resolution,[],[f94939,f11033]) ).
fof(f95229,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ one_sorted_str(sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f94940,f11033]) ).
fof(f95237,plain,
( sP48(sK428,sK427)
| ~ one_sorted_str(sK427)
| spl472_565
| spl472_1012 ),
inference(forward_subsumption_resolution,[],[f94948,f28894]) ).
fof(f95346,plain,
( sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))) = sK430(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f95227,f3071]) ).
fof(f95347,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_96
| spl472_565 ),
inference(forward_subsumption_resolution,[],[f95228,f3071]) ).
fof(f95348,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ element(sK428,powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f95229,f3071]) ).
fof(f95356,plain,
( ~ one_sorted_str(sK427)
| spl472_565
| spl472_1012 ),
inference(forward_subsumption_resolution,[],[f95237,f11033]) ).
fof(f95427,plain,
( sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))) = sK430(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f95346,f3070]) ).
fof(f95428,plain,
( ~ sP49(relation_dom(sK425(sK427,sK428)),sK427)
| spl472_96
| spl472_565 ),
inference(forward_subsumption_resolution,[],[f95347,f3070]) ).
fof(f95429,plain,
( element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f95348,f3070]) ).
fof(f95437,plain,
( $false
| spl472_565
| spl472_1012 ),
inference(forward_subsumption_resolution,[],[f95356,f3071]) ).
fof(f95438,plain,
( spl472_565
| spl472_1012 ),
inference(avatar_contradiction_clause,[],[f95437]) ).
fof(f95508,plain,
( ~ spl472_1011
| spl472_96
| spl472_565 ),
inference(avatar_split_clause,[],[f95428,f28892,f4879,f34719]) ).
fof(f95509,plain,
( spl472_1010
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(avatar_split_clause,[],[f95429,f32253,f32248,f32243,f28892,f34709]) ).
fof(f98006,plain,
( subset_complement(the_carrier(sK427),sK429(sK425(sK427,relation_dom(sK425(sK427,sK428))))) != subset_complement(the_carrier(sK427),sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| sK428 != relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(superposition,[],[f12845,f95427]) ).
fof(f98007,plain,
( sK428 != relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428))))
| ~ element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(trivial_inequality_removal,[],[f98006]) ).
fof(f98008,plain,
( ~ element(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),powerset(the_carrier(sK427)))
| ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881 ),
inference(forward_subsumption_resolution,[],[f98007,f34552]) ).
fof(f98009,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| sP49(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010 ),
inference(forward_subsumption_resolution,[],[f98008,f34711]) ).
fof(f98010,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011 ),
inference(forward_subsumption_resolution,[],[f98009,f34720]) ).
fof(f98011,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011 ),
inference(forward_subsumption_resolution,[],[f98010,f3071]) ).
fof(f98012,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),complements_of_subsets(the_carrier(sK427),relation_dom(sK425(sK427,sK428))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98011,f34724]) ).
fof(f98119,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| sP49(relation_dom(sK425(sK427,sK428)),sK427)
| sP48(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(superposition,[],[f98012,f3064]) ).
fof(f98126,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| sP48(relation_dom(sK425(sK427,sK428)),sK427)
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98119,f34720]) ).
fof(f98155,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| ~ one_sorted_str(sK427)
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98126,f11033]) ).
fof(f98159,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| ~ element(relation_dom(sK425(sK427,sK428)),powerset(powerset(the_carrier(sK427))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98155,f3071]) ).
fof(f98162,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),relation_dom(sK425(sK427,relation_dom(sK425(sK427,sK428)))))
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98159,f34724]) ).
fof(f98165,plain,
( ~ in(sK429(sK425(sK427,relation_dom(sK425(sK427,sK428)))),sK428)
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_demodulation,[],[f98162,f34552]) ).
fof(f98168,plain,
( $false
| spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(forward_subsumption_resolution,[],[f98165,f34553]) ).
fof(f98169,plain,
( spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(avatar_contradiction_clause,[],[f98168]) ).
fof(f98475,plain,
( ~ sP49(complements_of_subsets(the_carrier(sK427),sK428),sK427)
| ~ spl472_97 ),
inference(resolution,[],[f4885,f16304]) ).
fof(f98540,plain,
( $false
| ~ spl472_96
| ~ spl472_97 ),
inference(forward_subsumption_resolution,[],[f98475,f4880]) ).
fof(f98541,plain,
( ~ spl472_96
| ~ spl472_97 ),
inference(avatar_contradiction_clause,[],[f98540]) ).
fof(f98714,plain,
( sK422(sK428,sK427) = sK421(sK428,sK427)
| ~ spl472_1040
| ~ spl472_1041 ),
inference(forward_demodulation,[],[f35214,f35209]) ).
fof(f100713,plain,
( sK422(sK428,sK427) != sK421(sK428,sK427)
| ~ spl472_565 ),
inference(resolution,[],[f28893,f3058]) ).
fof(f100714,plain,
( $false
| ~ spl472_565
| ~ spl472_1040
| ~ spl472_1041 ),
inference(forward_subsumption_resolution,[],[f100713,f98714]) ).
fof(f100715,plain,
( ~ spl472_565
| ~ spl472_1040
| ~ spl472_1041 ),
inference(avatar_contradiction_clause,[],[f100714]) ).
fof(f102597,plain,
( element(sK420(sK428,sK427),powerset(the_carrier(sK427)))
| ~ spl472_34
| ~ spl472_58
| ~ spl472_565 ),
inference(resolution,[],[f94823,f36256]) ).
fof(f102652,plain,
( $false
| ~ spl472_34
| ~ spl472_58
| ~ spl472_565
| spl472_1039 ),
inference(forward_subsumption_resolution,[],[f102597,f35205]) ).
fof(f102653,plain,
( ~ spl472_34
| ~ spl472_58
| ~ spl472_565
| spl472_1039 ),
inference(avatar_contradiction_clause,[],[f102652]) ).
fof(f102673,plain,
( $false
| spl472_56
| ~ spl472_73 ),
inference(forward_subsumption_resolution,[],[f31263,f4690]) ).
fof(f102674,plain,
( spl472_56
| ~ spl472_73 ),
inference(avatar_contradiction_clause,[],[f102673]) ).
cnf(s30,plain,
spl472_34,
inference(sat_conversion,[],[f4497]) ).
cnf(s41,plain,
( ~ spl472_56
| spl472_57
| spl472_58 ),
inference(sat_conversion,[],[f4621]) ).
cnf(s42,plain,
( ~ spl472_56
| spl472_58
| spl472_59 ),
inference(sat_conversion,[],[f4626]) ).
cnf(s51,plain,
( spl472_58
| ~ spl472_72 ),
inference(sat_conversion,[],[f4686]) ).
cnf(s53,plain,
( spl472_58
| spl472_73 ),
inference(sat_conversion,[],[f4692]) ).
cnf(s76,plain,
( ~ spl472_96
| spl472_97 ),
inference(sat_conversion,[],[f4886]) ).
cnf(s934,plain,
( ~ spl472_34
| spl472_96
| spl472_881 ),
inference(sat_conversion,[],[f32258]) ).
cnf(s937,plain,
( ~ spl472_34
| spl472_96
| spl472_879 ),
inference(sat_conversion,[],[f32260]) ).
cnf(s941,plain,
( ~ spl472_34
| spl472_96
| spl472_880 ),
inference(sat_conversion,[],[f32263]) ).
cnf(s978,plain,
( ~ spl472_57
| ~ spl472_59
| spl472_72 ),
inference(sat_conversion,[],[f32795]) ).
cnf(s1103,plain,
( ~ spl472_565
| ~ spl472_1039
| spl472_1040 ),
inference(sat_conversion,[],[f35210]) ).
cnf(s1104,plain,
( ~ spl472_565
| ~ spl472_1039
| spl472_1041 ),
inference(sat_conversion,[],[f35215]) ).
cnf(s3141,plain,
( spl472_565
| spl472_1012 ),
inference(sat_conversion,[],[f95438]) ).
cnf(s3142,plain,
( spl472_96
| spl472_565
| ~ spl472_1011 ),
inference(sat_conversion,[],[f95508]) ).
cnf(s3143,plain,
( spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| spl472_1010 ),
inference(sat_conversion,[],[f95509]) ).
cnf(s3243,plain,
( spl472_565
| ~ spl472_879
| ~ spl472_880
| ~ spl472_881
| ~ spl472_1010
| spl472_1011
| ~ spl472_1012 ),
inference(sat_conversion,[],[f98169]) ).
cnf(s3288,plain,
( ~ spl472_96
| ~ spl472_97 ),
inference(sat_conversion,[],[f98541]) ).
cnf(s3394,plain,
( ~ spl472_565
| ~ spl472_1040
| ~ spl472_1041 ),
inference(sat_conversion,[],[f100715]) ).
cnf(s3430,plain,
( ~ spl472_34
| ~ spl472_58
| ~ spl472_565
| spl472_1039 ),
inference(sat_conversion,[],[f102653]) ).
cnf(s3435,plain,
( spl472_56
| ~ spl472_73 ),
inference(sat_conversion,[],[f102674]) ).
cnf(s3571,plain,
( spl472_565
| spl472_96 ),
inference(rat,[],[s3243,s3141,s3142,s3143,s941,s937,s934,s30]) ).
cnf(s3572,plain,
( ~ spl472_1039
| ~ spl472_565 ),
inference(rat,[],[s3394,s1103,s1104]) ).
cnf(s3573,plain,
( ~ spl472_565
| ~ spl472_58 ),
inference(rat,[],[s3572,s3430,s30]) ).
cnf(s3574,plain,
~ spl472_96,
inference(rat,[],[s76,s3288]) ).
cnf(s3578,plain,
spl472_565,
inference(rat,[],[s3571,s3574]) ).
cnf(s3585,plain,
~ spl472_58,
inference(rat,[],[s3573,s3578]) ).
cnf(s3588,plain,
spl472_73,
inference(rat,[],[s53,s3585]) ).
cnf(s3589,plain,
~ spl472_72,
inference(rat,[],[s51,s3585]) ).
cnf(s3591,plain,
spl472_56,
inference(rat,[],[s3435,s3588]) ).
cnf(s3595,plain,
spl472_59,
inference(rat,[],[s42,s3585,s3591]) ).
cnf(s3596,plain,
spl472_57,
inference(rat,[],[s41,s3585,s3591]) ).
cnf(s3600,plain,
$false,
inference(rat,[],[s978,s3589,s3596,s3595]) ).
fof(f103342,plain,
$false,
inference(avatar_sat_refutation,[],[s3600]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU334+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n003.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Mon Sep 28 04:49:01 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.10/2.64 % (1193596)Detected formulas, will run a generic FOF schedule.
% 12.10/2.64 % (1193602)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=1652138684:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.10/2.64 % (1193603)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=2461299886:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.10/2.64 % (1193605)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3558676286:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.10/2.64 % (1193606)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3803969655:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.10/2.64 % (1193604)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=501925771:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.10/2.64 % (1193607)dis-21_1_sil=8000:lcm=predicate:random_seed=1722008186: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)
% 12.10/2.64 % (1193601)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=1510110443:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.10/2.64 % (1193604)Instruction limit reached!
% 12.10/2.64 % (1193604)------------------------------
% 12.10/2.64 % (1193604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.64 % (1193604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.64 % (1193604)CaDiCaL version: 2.1.3
% 12.10/2.64 % (1193604)Termination reason: Instruction limit
% 12.10/2.64 % (1193604)Termination phase: Saturation
% 12.10/2.64 % (1193604)Time elapsed: 0.059 s
% 12.10/2.64 % (1193604)Peak memory usage: 91 MB
% 12.10/2.64 % (1193604)Instructions burned: 111 (million)
% 12.10/2.64 % (1193607)Instruction limit reached!
% 12.10/2.64 % (1193607)------------------------------
% 12.10/2.64 % (1193607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.64 % (1193607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.64 % (1193607)CaDiCaL version: 2.1.3
% 12.10/2.64 % (1193607)Termination reason: Instruction limit
% 12.10/2.64 % (1193607)Termination phase: Saturation
% 12.10/2.64 % (1193607)Time elapsed: 0.065 s
% 12.10/2.64 % (1193607)Peak memory usage: 91 MB
% 12.10/2.64 % (1193607)Instructions burned: 131 (million)
% 12.10/2.64 % (1193605)Instruction limit reached!
% 12.10/2.64 % (1193605)------------------------------
% 12.10/2.64 % (1193605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.64 % (1193605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.64 % (1193605)CaDiCaL version: 2.1.3
% 12.10/2.64 % (1193605)Termination reason: Instruction limit
% 12.10/2.64 % (1193605)Termination phase: Saturation
% 12.10/2.64 % (1193605)Time elapsed: 0.070 s
% 12.10/2.64 % (1193605)Peak memory usage: 90 MB
% 12.10/2.64 % (1193605)Instructions burned: 119 (million)
% 12.10/2.64 % (1193606)Instruction limit reached!
% 12.10/2.64 % (1193606)------------------------------
% 12.10/2.64 % (1193606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.64 % (1193606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.64 % (1193606)CaDiCaL version: 2.1.3
% 12.10/2.64 % (1193606)Termination reason: Instruction limit
% 12.10/2.64 % (1193606)Termination phase: Saturation
% 12.10/2.64 % (1193606)Time elapsed: 0.091 s
% 12.10/2.64 % (1193606)Peak memory usage: 91 MB
% 12.10/2.64 % (1193606)Instructions burned: 140 (million)
% 12.10/2.64 % (1193615)lrs+10_1_sil=8000:sp=occurrence:random_seed=1956319491:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.10/2.64 % (1193616)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3078378008:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.10/2.64 % (1193617)lrs+1011_1_sil=32000:sp=occurrence:random_seed=234979441:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.10/2.64 % (1193618)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=324233270:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.10/2.64 % (1193616)Instruction limit reached!
% 17.61/3.45 % (1193616)------------------------------
% 17.61/3.45 % (1193616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193616)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193616)Termination reason: Instruction limit
% 17.61/3.45 % (1193616)Termination phase: Saturation
% 17.61/3.45 % (1193616)Time elapsed: 0.087 s
% 17.61/3.45 % (1193616)Peak memory usage: 91 MB
% 17.61/3.45 % (1193616)Instructions burned: 157 (million)
% 17.61/3.45 % (1193618)Instruction limit reached!
% 17.61/3.45 % (1193618)------------------------------
% 17.61/3.45 % (1193618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193618)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193618)Termination reason: Instruction limit
% 17.61/3.45 % (1193618)Termination phase: Saturation
% 17.61/3.45 % (1193618)Time elapsed: 0.149 s
% 17.61/3.45 % (1193618)Peak memory usage: 94 MB
% 17.61/3.45 % (1193618)Instructions burned: 249 (million)
% 17.61/3.45 % (1193615)Instruction limit reached!
% 17.61/3.45 % (1193615)------------------------------
% 17.61/3.45 % (1193615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193615)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193615)Termination reason: Instruction limit
% 17.61/3.45 % (1193615)Termination phase: Saturation
% 17.61/3.45 % (1193615)Time elapsed: 0.186 s
% 17.61/3.45 % (1193615)Peak memory usage: 95 MB
% 17.61/3.45 % (1193615)Instructions burned: 286 (million)
% 17.61/3.45 % (1193623)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2696649297:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 17.61/3.45 % (1193617)Instruction limit reached!
% 17.61/3.45 % (1193617)------------------------------
% 17.61/3.45 % (1193617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193617)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193617)Termination reason: Instruction limit
% 17.61/3.45 % (1193617)Termination phase: Saturation
% 17.61/3.45 % (1193617)Time elapsed: 0.224 s
% 17.61/3.45 % (1193617)Peak memory usage: 95 MB
% 17.61/3.45 % (1193617)Instructions burned: 325 (million)
% 17.61/3.45 % (1193623)Instruction limit reached!
% 17.61/3.45 % (1193623)------------------------------
% 17.61/3.45 % (1193623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193623)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193623)Termination reason: Instruction limit
% 17.61/3.45 % (1193623)Termination phase: Saturation
% 17.61/3.45 % (1193623)Time elapsed: 0.102 s
% 17.61/3.45 % (1193623)Peak memory usage: 93 MB
% 17.61/3.45 % (1193623)Instructions burned: 296 (million)
% 17.61/3.45 % (1193625)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1924557764:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.61/3.45 % (1193624)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4173768287:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 17.61/3.45 % (1193627)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=461353255:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 17.61/3.45 % (1193625)Instruction limit reached!
% 17.61/3.45 % (1193625)------------------------------
% 17.61/3.45 % (1193625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.45 % (1193625)CaDiCaL version: 2.1.3
% 17.61/3.45 % (1193625)Termination reason: Instruction limit
% 17.61/3.45 % (1193625)Termination phase: Saturation
% 17.61/3.45 % (1193625)Time elapsed: 0.066 s
% 17.61/3.45 % (1193625)Peak memory usage: 91 MB
% 17.61/3.45 % (1193625)Instructions burned: 113 (million)
% 17.61/3.45 % (1193628)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4054880106:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 17.61/3.45 % (1193627)Instruction limit reached!
% 17.61/3.45 % (1193627)------------------------------
% 17.61/3.45 % (1193627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.45 % (1193627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.46 % (1193627)CaDiCaL version: 2.1.3
% 53.46/8.46 % (1193627)Termination reason: Instruction limit
% 53.46/8.46 % (1193627)Termination phase: Saturation
% 53.46/8.46 % (1193627)Time elapsed: 0.072 s
% 53.46/8.46 % (1193627)Peak memory usage: 91 MB
% 53.46/8.46 % (1193627)Instructions burned: 128 (million)
% 53.46/8.46 % (1193628)Instruction limit reached!
% 53.46/8.46 % (1193628)------------------------------
% 53.46/8.46 % (1193628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.46/8.46 % (1193628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.46 % (1193628)CaDiCaL version: 2.1.3
% 53.46/8.46 % (1193628)Termination reason: Instruction limit
% 53.46/8.46 % (1193628)Termination phase: Saturation
% 53.46/8.46 % (1193628)Time elapsed: 0.029 s
% 53.46/8.46 % (1193628)Peak memory usage: 90 MB
% 53.46/8.46 % (1193628)Instructions burned: 116 (million)
% 53.46/8.46 % (1193632)lrs+10_1_sil=8000:sp=occurrence:random_seed=1782575886:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 53.46/8.46 % (1193634)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3613771875:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 53.46/8.47 % (1193635)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2579039140:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 53.46/8.47 % (1193634)Instruction limit reached!
% 53.46/8.47 % (1193634)------------------------------
% 53.46/8.47 % (1193634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.46/8.47 % (1193634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.47 % (1193634)CaDiCaL version: 2.1.3
% 53.46/8.47 % (1193634)Termination reason: Instruction limit
% 53.46/8.47 % (1193634)Termination phase: Saturation
% 53.46/8.47 % (1193634)Time elapsed: 0.142 s
% 53.46/8.47 % (1193634)Peak memory usage: 95 MB
% 53.46/8.47 % (1193634)Instructions burned: 437 (million)
% 53.46/8.47 % (1193639)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3741157431:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 53.46/8.47 % (1193639)Instruction limit reached!
% 53.46/8.47 % (1193639)------------------------------
% 53.46/8.47 % (1193639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.46/8.47 % (1193639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.47 % (1193639)CaDiCaL version: 2.1.3
% 53.46/8.47 % (1193639)Termination reason: Instruction limit
% 53.46/8.47 % (1193639)Termination phase: Saturation
% 53.46/8.47 % (1193639)Time elapsed: 0.039 s
% 53.46/8.47 % (1193639)Peak memory usage: 92 MB
% 53.46/8.47 % (1193639)Instructions burned: 135 (million)
% 53.46/8.47 % (1193641)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2671441927:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 53.46/8.47 % (1193632)Instruction limit reached!
% 53.46/8.47 % (1193632)------------------------------
% 53.46/8.47 % (1193632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.46/8.47 % (1193632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.47 % (1193632)CaDiCaL version: 2.1.3
% 53.46/8.47 % (1193632)Termination reason: Instruction limit
% 53.46/8.47 % (1193632)Termination phase: Saturation
% 53.46/8.47 % (1193632)Time elapsed: 0.582 s
% 53.46/8.47 % (1193632)Peak memory usage: 104 MB
% 53.46/8.47 % (1193632)Instructions burned: 907 (million)
% 53.46/8.47 % (1193641)Instruction limit reached!
% 53.46/8.47 % (1193641)------------------------------
% 53.46/8.47 % (1193641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.46/8.47 % (1193641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.46/8.47 % (1193641)CaDiCaL version: 2.1.3
% 53.46/8.47 % (1193641)Termination reason: Instruction limit
% 53.46/8.47 % (1193641)Termination phase: Saturation
% 53.46/8.47 % (1193641)Time elapsed: 0.195 s
% 53.46/8.47 % (1193641)Peak memory usage: 100 MB
% 53.46/8.47 % (1193641)Instructions burned: 595 (million)
% 53.46/8.47 % (1193643)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1110774210:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 53.46/8.47 % (1193644)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=3215894137:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 75.50/11.55 % (1193644)Instruction limit reached!
% 75.50/11.55 % (1193644)------------------------------
% 75.50/11.55 % (1193644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193644)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193644)Termination reason: Instruction limit
% 75.50/11.55 % (1193644)Termination phase: Saturation
% 75.50/11.55 % (1193644)Time elapsed: 0.044 s
% 75.50/11.55 % (1193644)Peak memory usage: 92 MB
% 75.50/11.55 % (1193644)Instructions burned: 126 (million)
% 75.50/11.55 % (1193647)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2738577046:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 75.50/11.55 % (1193647)Instruction limit reached!
% 75.50/11.55 % (1193647)------------------------------
% 75.50/11.55 % (1193647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193647)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193647)Termination reason: Instruction limit
% 75.50/11.55 % (1193647)Termination phase: Saturation
% 75.50/11.55 % (1193647)Time elapsed: 0.040 s
% 75.50/11.55 % (1193647)Peak memory usage: 92 MB
% 75.50/11.55 % (1193647)Instructions burned: 136 (million)
% 75.50/11.55 % (1193649)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1463718124:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 75.50/11.55 % (1193649)Instruction limit reached!
% 75.50/11.55 % (1193649)------------------------------
% 75.50/11.55 % (1193649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193649)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193649)Termination reason: Instruction limit
% 75.50/11.55 % (1193649)Termination phase: Saturation
% 75.50/11.55 % (1193649)Time elapsed: 0.039 s
% 75.50/11.55 % (1193649)Peak memory usage: 92 MB
% 75.50/11.55 % (1193649)Instructions burned: 142 (million)
% 75.50/11.55 % (1193624)Instruction limit reached!
% 75.50/11.55 % (1193624)------------------------------
% 75.50/11.55 % (1193624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193624)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193624)Termination reason: Instruction limit
% 75.50/11.55 % (1193624)Termination phase: Saturation
% 75.50/11.55 % (1193624)Time elapsed: 1.493 s
% 75.50/11.55 % (1193624)Peak memory usage: 149 MB
% 75.50/11.55 % (1193624)Instructions burned: 2351 (million)
% 75.50/11.55 % (1193651)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=679131852:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 75.50/11.55 % (1193651)Instruction limit reached!
% 75.50/11.55 % (1193651)------------------------------
% 75.50/11.55 % (1193651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193651)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193651)Termination reason: Instruction limit
% 75.50/11.55 % (1193651)Termination phase: Saturation
% 75.50/11.55 % (1193651)Time elapsed: 0.137 s
% 75.50/11.55 % (1193651)Peak memory usage: 95 MB
% 75.50/11.55 % (1193651)Instructions burned: 431 (million)
% 75.50/11.55 % (1193652)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3025421646:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 75.50/11.55 % (1193654)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=241023294:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 75.50/11.55 % (1193654)Instruction limit reached!
% 75.50/11.55 % (1193654)------------------------------
% 75.50/11.55 % (1193654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.50/11.55 % (1193654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.50/11.55 % (1193654)CaDiCaL version: 2.1.3
% 75.50/11.55 % (1193654)Termination reason: Instruction limit
% 75.50/11.55 % (1193654)Termination phase: Saturation
% 75.50/11.55 % (1193654)Time elapsed: 0.046 s
% 75.50/11.55 % (1193654)Peak memory usage: 92 MB
% 104.39/15.63 % (1193654)Instructions burned: 152 (million)
% 104.39/15.63 % (1193657)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3603280061:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi)
% 104.39/15.63 % (1193635)Instruction limit reached!
% 104.39/15.63 % (1193635)------------------------------
% 104.39/15.63 % (1193635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193635)CaDiCaL version: 2.1.3
% 104.39/15.63 % (1193635)Termination reason: Instruction limit
% 104.39/15.63 % (1193635)Termination phase: Saturation
% 104.39/15.63 % (1193635)Time elapsed: 3.115 s
% 104.39/15.63 % (1193635)Peak memory usage: 156 MB
% 104.39/15.63 % (1193635)Instructions burned: 5202 (million)
% 104.39/15.63 % (1193659)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2557370336:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 104.39/15.63 % (1193659)Instruction limit reached!
% 104.39/15.63 % (1193659)------------------------------
% 104.39/15.63 % (1193659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193659)CaDiCaL version: 2.1.3
% 104.39/15.63 % (1193659)Termination reason: Instruction limit
% 104.39/15.63 % (1193659)Termination phase: Saturation
% 104.39/15.63 % (1193659)Time elapsed: 0.319 s
% 104.39/15.63 % (1193659)Peak memory usage: 92 MB
% 104.39/15.63 % (1193659)Instructions burned: 667 (million)
% 104.39/15.63 % (1193661)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1405949253:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 104.39/15.63 % (1193661)Instruction limit reached!
% 104.39/15.63 % (1193661)------------------------------
% 104.39/15.63 % (1193661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193661)CaDiCaL version: 2.1.3
% 104.39/15.63 % (1193661)Termination reason: Instruction limit
% 104.39/15.63 % (1193661)Termination phase: Saturation
% 104.39/15.63 % (1193661)Time elapsed: 0.098 s
% 104.39/15.63 % (1193661)Peak memory usage: 92 MB
% 104.39/15.63 % (1193661)Instructions burned: 186 (million)
% 104.39/15.63 % (1193663)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3990194567:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 104.39/15.63 % (1193663)Instruction limit reached!
% 104.39/15.63 % (1193663)------------------------------
% 104.39/15.63 % (1193663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193663)CaDiCaL version: 2.1.3
% 104.39/15.63 % (1193663)Termination reason: Instruction limit
% 104.39/15.63 % (1193663)Termination phase: Saturation
% 104.39/15.63 % (1193663)Time elapsed: 0.119 s
% 104.39/15.63 % (1193663)Peak memory usage: 94 MB
% 104.39/15.63 % (1193663)Instructions burned: 194 (million)
% 104.39/15.63 % (1193665)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3260739748:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2947 on theBenchmark for (2947ds/4850Mi)
% 104.39/15.63 % (1193652)Instruction limit reached!
% 104.39/15.63 % (1193652)------------------------------
% 104.39/15.63 % (1193652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193652)CaDiCaL version: 2.1.3
% 104.39/15.63 % (1193652)Termination reason: Instruction limit
% 104.39/15.63 % (1193652)Termination phase: Saturation
% 104.39/15.63 % (1193652)Time elapsed: 3.797 s
% 104.39/15.63 % (1193652)Peak memory usage: 174 MB
% 104.39/15.63 % (1193652)Instructions burned: 6061 (million)
% 104.39/15.63 % (1193667)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3324320568:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 104.39/15.63 % (1193657)Instruction limit reached!
% 104.39/15.63 % (1193657)------------------------------
% 104.39/15.63 % (1193657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.39/15.63 % (1193657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.39/15.63 % (1193657)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193657)Termination reason: Instruction limit
% 139.35/20.58 % (1193657)Termination phase: Saturation
% 139.35/20.58 % (1193657)Time elapsed: 4.886 s
% 139.35/20.58 % (1193657)Peak memory usage: 195 MB
% 139.35/20.58 % (1193657)Instructions burned: 14155 (million)
% 139.35/20.58 % (1193669)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3218838093:i=319:kws=precedence:fsr=off_2924 on theBenchmark for (2924ds/319Mi)
% 139.35/20.58 % (1193669)Instruction limit reached!
% 139.35/20.58 % (1193669)------------------------------
% 139.35/20.58 % (1193669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193669)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193669)Termination reason: Instruction limit
% 139.35/20.58 % (1193669)Termination phase: Saturation
% 139.35/20.58 % (1193669)Time elapsed: 0.097 s
% 139.35/20.58 % (1193669)Peak memory usage: 95 MB
% 139.35/20.58 % (1193669)Instructions burned: 327 (million)
% 139.35/20.58 % (1193671)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3699942173:i=2064:ep=RST_2921 on theBenchmark for (2921ds/2064Mi)
% 139.35/20.58 % (1193665)Instruction limit reached!
% 139.35/20.58 % (1193665)------------------------------
% 139.35/20.58 % (1193665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193665)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193665)Termination reason: Instruction limit
% 139.35/20.58 % (1193665)Termination phase: Saturation
% 139.35/20.58 % (1193665)Time elapsed: 2.963 s
% 139.35/20.58 % (1193665)Peak memory usage: 146 MB
% 139.35/20.58 % (1193665)Instructions burned: 4850 (million)
% 139.35/20.58 % (1193673)dis-1011_128_sil=32000:random_seed=2038574466:i=3706:ep=RST:av=off_2916 on theBenchmark for (2916ds/3706Mi)
% 139.35/20.58 % (1193671)Instruction limit reached!
% 139.35/20.58 % (1193671)------------------------------
% 139.35/20.58 % (1193671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193671)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193671)Termination reason: Instruction limit
% 139.35/20.58 % (1193671)Termination phase: Saturation
% 139.35/20.58 % (1193671)Time elapsed: 0.597 s
% 139.35/20.58 % (1193671)Peak memory usage: 117 MB
% 139.35/20.58 % (1193671)Instructions burned: 2067 (million)
% 139.35/20.58 % (1193675)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1478816362:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2914 on theBenchmark for (2914ds/757Mi)
% 139.35/20.58 % (1193675)Instruction limit reached!
% 139.35/20.58 % (1193675)------------------------------
% 139.35/20.58 % (1193675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193675)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193675)Termination reason: Instruction limit
% 139.35/20.58 % (1193675)Termination phase: Saturation
% 139.35/20.58 % (1193675)Time elapsed: 0.278 s
% 139.35/20.58 % (1193675)Peak memory usage: 109 MB
% 139.35/20.58 % (1193675)Instructions burned: 758 (million)
% 139.35/20.58 % (1193677)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3429449590:i=13913:ss=axioms:sgt=8_2910 on theBenchmark for (2910ds/13913Mi)
% 139.35/20.58 % (1193643)Instruction limit reached!
% 139.35/20.58 % (1193643)------------------------------
% 139.35/20.58 % (1193643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193643)CaDiCaL version: 2.1.3
% 139.35/20.58 % (1193643)Termination reason: Instruction limit
% 139.35/20.58 % (1193643)Termination phase: Saturation
% 139.35/20.58 % (1193643)Time elapsed: 8.119 s
% 139.35/20.58 % (1193643)Peak memory usage: 238 MB
% 139.35/20.58 % (1193643)Instructions burned: 13193 (million)
% 139.35/20.58 % (1193679)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=869124272:i=9925:aac=none_2901 on theBenchmark for (2901ds/9925Mi)
% 139.35/20.58 % (1193673)Instruction limit reached!
% 139.35/20.58 % (1193673)------------------------------
% 139.35/20.58 % (1193673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.35/20.58 % (1193673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.35/20.58 % (1193673)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193673)Termination reason: Instruction limit
% 159.92/23.41 % (1193673)Termination phase: Saturation
% 159.92/23.41 % (1193673)Time elapsed: 2.152 s
% 159.92/23.41 % (1193673)Peak memory usage: 109 MB
% 159.92/23.41 % (1193673)Instructions burned: 3707 (million)
% 159.92/23.41 % (1193682)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1774184373:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/2479Mi)
% 159.92/23.41 % (1193682)Instruction limit reached!
% 159.92/23.41 % (1193682)------------------------------
% 159.92/23.41 % (1193682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/23.41 % (1193682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/23.41 % (1193682)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193682)Termination reason: Instruction limit
% 159.92/23.41 % (1193682)Termination phase: Saturation
% 159.92/23.41 % (1193682)Time elapsed: 1.446 s
% 159.92/23.41 % (1193682)Peak memory usage: 111 MB
% 159.92/23.41 % (1193682)Instructions burned: 2479 (million)
% 159.92/23.41 % (1193684)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=469072608:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2877 on theBenchmark for (2877ds/440Mi)
% 159.92/23.41 % (1193684)Instruction limit reached!
% 159.92/23.41 % (1193684)------------------------------
% 159.92/23.41 % (1193684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/23.41 % (1193684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/23.41 % (1193684)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193684)Termination reason: Instruction limit
% 159.92/23.41 % (1193684)Termination phase: Saturation
% 159.92/23.41 % (1193684)Time elapsed: 0.245 s
% 159.92/23.41 % (1193684)Peak memory usage: 96 MB
% 159.92/23.41 % (1193684)Instructions burned: 440 (million)
% 159.92/23.41 % (1193686)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2192186113:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2873 on theBenchmark for (2873ds/11145Mi)
% 159.92/23.41 % (1193677)Instruction limit reached!
% 159.92/23.41 % (1193677)------------------------------
% 159.92/23.41 % (1193677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/23.41 % (1193677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/23.41 % (1193677)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193677)Termination reason: Instruction limit
% 159.92/23.41 % (1193677)Termination phase: Saturation
% 159.92/23.41 % (1193677)Time elapsed: 4.558 s
% 159.92/23.41 % (1193677)Peak memory usage: 218 MB
% 159.92/23.41 % (1193677)Instructions burned: 13916 (million)
% 159.92/23.41 % (1193688)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=567069025:cts=off:i=3034:av=off:er=known:fsd=on_2863 on theBenchmark for (2863ds/3034Mi)
% 159.92/23.41 % (1193667)Instruction limit reached!
% 159.92/23.41 % (1193667)------------------------------
% 159.92/23.41 % (1193667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/23.41 % (1193667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/23.41 % (1193667)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193667)Termination reason: Instruction limit
% 159.92/23.41 % (1193667)Termination phase: Saturation
% 159.92/23.41 % (1193667)Time elapsed: 7.638 s
% 159.92/23.41 % (1193667)Peak memory usage: 250 MB
% 159.92/23.41 % (1193667)Instructions burned: 12111 (million)
% 159.92/23.41 % (1193690)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1085869813:st=2:s2a=on:i=524:s2at=2:ss=axioms_2859 on theBenchmark for (2859ds/524Mi)
% 159.92/23.41 % (1193690)Instruction limit reached!
% 159.92/23.41 % (1193690)------------------------------
% 159.92/23.41 % (1193690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.92/23.41 % (1193690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.92/23.41 % (1193690)CaDiCaL version: 2.1.3
% 159.92/23.41 % (1193690)Termination reason: Instruction limit
% 159.92/23.41 % (1193690)Termination phase: Saturation
% 159.92/23.41 % (1193690)Time elapsed: 0.296 s
% 159.92/23.41 % (1193690)Peak memory usage: 98 MB
% 159.92/23.41 % (1193690)Instructions burned: 525 (million)
% 159.92/23.41 % (1193692)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3248049680:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2854 on theBenchmark for (2854ds/1016Mi)
% 159.92/23.41 % (1193688)Instruction limit reached!
% 159.92/23.41 % (1193688)------------------------------
% 159.92/23.41 % (1193688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193688)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193688)Termination reason: Instruction limit
% 189.03/27.54 % (1193688)Termination phase: Saturation
% 189.03/27.54 % (1193688)Time elapsed: 0.978 s
% 189.03/27.54 % (1193688)Peak memory usage: 145 MB
% 189.03/27.54 % (1193688)Instructions burned: 3036 (million)
% 189.03/27.54 % (1193694)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2879674598:i=14123:bd=preordered:ins=4_2852 on theBenchmark for (2852ds/14123Mi)
% 189.03/27.54 % (1193692)Instruction limit reached!
% 189.03/27.54 % (1193692)------------------------------
% 189.03/27.54 % (1193692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193692)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193692)Termination reason: Instruction limit
% 189.03/27.54 % (1193692)Termination phase: Saturation
% 189.03/27.54 % (1193692)Time elapsed: 0.633 s
% 189.03/27.54 % (1193692)Peak memory usage: 119 MB
% 189.03/27.54 % (1193692)Instructions burned: 1018 (million)
% 189.03/27.54 % (1193696)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1410771635:i=5781:kws=precedence:bd=all:rawr=on_2846 on theBenchmark for (2846ds/5781Mi)
% 189.03/27.54 % (1193679)Instruction limit reached!
% 189.03/27.54 % (1193679)------------------------------
% 189.03/27.54 % (1193679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193679)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193679)Termination reason: Instruction limit
% 189.03/27.54 % (1193679)Termination phase: Saturation
% 189.03/27.54 % (1193679)Time elapsed: 5.763 s
% 189.03/27.54 % (1193679)Peak memory usage: 199 MB
% 189.03/27.54 % (1193679)Instructions burned: 9926 (million)
% 189.03/27.54 % (1193698)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2158236594:i=2448:gtgl=5:bd=preordered:gtg=all_2841 on theBenchmark for (2841ds/2448Mi)
% 189.03/27.54 % (1193698)Instruction limit reached!
% 189.03/27.54 % (1193698)------------------------------
% 189.03/27.54 % (1193698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193698)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193698)Termination reason: Instruction limit
% 189.03/27.54 % (1193698)Termination phase: Saturation
% 189.03/27.54 % (1193698)Time elapsed: 1.435 s
% 189.03/27.54 % (1193698)Peak memory usage: 150 MB
% 189.03/27.54 % (1193698)Instructions burned: 2449 (million)
% 189.03/27.54 % (1193700)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2600382744:i=3223:kws=precedence:fgj=on:av=off_2825 on theBenchmark for (2825ds/3223Mi)
% 189.03/27.54 % (1193696)Instruction limit reached!
% 189.03/27.54 % (1193696)------------------------------
% 189.03/27.54 % (1193696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193696)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193696)Termination reason: Instruction limit
% 189.03/27.54 % (1193696)Termination phase: Saturation
% 189.03/27.54 % (1193696)Time elapsed: 2.930 s
% 189.03/27.54 % (1193696)Peak memory usage: 117 MB
% 189.03/27.54 % (1193696)Instructions burned: 5786 (million)
% 189.03/27.54 % (1193702)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1002338290:st=5.6:i=2033:sd=3:ss=axioms_2815 on theBenchmark for (2815ds/2033Mi)
% 189.03/27.54 % (1193700)Instruction limit reached!
% 189.03/27.54 % (1193700)------------------------------
% 189.03/27.54 % (1193700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.03/27.54 % (1193700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.03/27.54 % (1193700)CaDiCaL version: 2.1.3
% 189.03/27.54 % (1193700)Termination reason: Instruction limit
% 189.03/27.54 % (1193700)Termination phase: Saturation
% 189.03/27.54 % (1193700)Time elapsed: 2.055 s
% 189.03/27.54 % (1193700)Peak memory usage: 154 MB
% 189.03/27.54 % (1193700)Instructions burned: 3223 (million)
% 189.03/27.54 % (1193694)Instruction limit reached!
% 189.03/27.54 % (1193694)------------------------------
% 189.03/27.54 % (1193694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193694)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193694)Termination reason: Instruction limit
% 229.99/33.36 % (1193694)Termination phase: Saturation
% 229.99/33.36 % (1193694)Time elapsed: 4.816 s
% 229.99/33.36 % (1193694)Peak memory usage: 209 MB
% 229.99/33.36 % (1193694)Instructions burned: 14125 (million)
% 229.99/33.36 % (1193702)Instruction limit reached!
% 229.99/33.36 % (1193702)------------------------------
% 229.99/33.36 % (1193702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193702)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193702)Termination reason: Instruction limit
% 229.99/33.36 % (1193702)Termination phase: Saturation
% 229.99/33.36 % (1193702)Time elapsed: 1.230 s
% 229.99/33.36 % (1193702)Peak memory usage: 146 MB
% 229.99/33.36 % (1193702)Instructions burned: 2034 (million)
% 229.99/33.36 % (1193705)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1697257486:i=21611:sd=3:ss=axioms_2803 on theBenchmark for (2803ds/21611Mi)
% 229.99/33.36 % (1193704)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2602314152:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2803 on theBenchmark for (2803ds/2055Mi)
% 229.99/33.36 % (1193706)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2684045958:i=4835:sd=13:ss=axioms:sgt=23_2801 on theBenchmark for (2801ds/4835Mi)
% 229.99/33.36 % (1193686)Instruction limit reached!
% 229.99/33.36 % (1193686)------------------------------
% 229.99/33.36 % (1193686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193686)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193686)Termination reason: Instruction limit
% 229.99/33.36 % (1193686)Termination phase: Saturation
% 229.99/33.36 % (1193686)Time elapsed: 7.465 s
% 229.99/33.36 % (1193686)Peak memory usage: 213 MB
% 229.99/33.36 % (1193686)Instructions burned: 11147 (million)
% 229.99/33.36 % (1193710)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1083167855:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2796 on theBenchmark for (2796ds/797Mi)
% 229.99/33.36 % (1193710)Instruction limit reached!
% 229.99/33.36 % (1193710)------------------------------
% 229.99/33.36 % (1193710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193710)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193710)Termination reason: Instruction limit
% 229.99/33.36 % (1193710)Termination phase: Saturation
% 229.99/33.36 % (1193710)Time elapsed: 0.417 s
% 229.99/33.36 % (1193710)Peak memory usage: 95 MB
% 229.99/33.36 % (1193710)Instructions burned: 799 (million)
% 229.99/33.36 % (1193712)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=715728684:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2790 on theBenchmark for (2790ds/2326Mi)
% 229.99/33.36 % (1193704)Instruction limit reached!
% 229.99/33.36 % (1193704)------------------------------
% 229.99/33.36 % (1193704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193704)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193704)Termination reason: Instruction limit
% 229.99/33.36 % (1193704)Termination phase: Saturation
% 229.99/33.36 % (1193704)Time elapsed: 1.317 s
% 229.99/33.36 % (1193704)Peak memory usage: 138 MB
% 229.99/33.36 % (1193704)Instructions burned: 2057 (million)
% 229.99/33.36 % (1193714)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2431962736:i=6038:nm=6_2788 on theBenchmark for (2788ds/6038Mi)
% 229.99/33.36 % (1193712)Instruction limit reached!
% 229.99/33.36 % (1193712)------------------------------
% 229.99/33.36 % (1193712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.99/33.36 % (1193712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.99/33.36 % (1193712)CaDiCaL version: 2.1.3
% 229.99/33.36 % (1193712)Termination reason: Instruction limit
% 229.99/33.36 % (1193712)Termination phase: Saturation
% 133.06/40.44 % (1193712)Time elapsed: 1.429 s
% 133.06/40.44 % (1193712)Peak memory usage: 117 MB
% 133.06/40.44 % (1193712)Instructions burned: 2326 (million)
% 133.06/40.44 % (1193716)lrs+10_1_sil=32000:sp=occurrence:random_seed=468396183:st=2:i=33334:sd=3:ss=included:sgt=32_2774 on theBenchmark for (2774ds/33334Mi)
% 133.06/40.44 % (1193706)Instruction limit reached!
% 133.06/40.44 % (1193706)------------------------------
% 133.06/40.44 % (1193706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193706)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193706)Termination reason: Instruction limit
% 133.06/40.44 % (1193706)Termination phase: Saturation
% 133.06/40.44 % (1193706)Time elapsed: 3.011 s
% 133.06/40.44 % (1193706)Peak memory usage: 137 MB
% 133.06/40.44 % (1193706)Instructions burned: 4835 (million)
% 133.06/40.44 % (1193718)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2832625067:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2770 on theBenchmark for (2770ds/1008Mi)
% 133.06/40.44 % (1193718)Instruction limit reached!
% 133.06/40.44 % (1193718)------------------------------
% 133.06/40.44 % (1193718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193718)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193718)Termination reason: Instruction limit
% 133.06/40.44 % (1193718)Termination phase: Saturation
% 133.06/40.44 % (1193718)Time elapsed: 0.526 s
% 133.06/40.44 % (1193718)Peak memory usage: 97 MB
% 133.06/40.44 % (1193718)Instructions burned: 1009 (million)
% 133.06/40.44 % (1193720)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=451943955:i=8327:s2at=5:bd=preordered_2763 on theBenchmark for (2763ds/8327Mi)
% 133.06/40.44 % (1193714)Instruction limit reached!
% 133.06/40.44 % (1193714)------------------------------
% 133.06/40.44 % (1193714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193714)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193714)Termination reason: Instruction limit
% 133.06/40.44 % (1193714)Termination phase: Saturation
% 133.06/40.44 % (1193714)Time elapsed: 3.208 s
% 133.06/40.44 % (1193714)Peak memory usage: 176 MB
% 133.06/40.44 % (1193714)Instructions burned: 6039 (million)
% 133.06/40.44 % (1193722)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1626961260:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2754 on theBenchmark for (2754ds/1083Mi)
% 133.06/40.44 % (1193722)Instruction limit reached!
% 133.06/40.44 % (1193722)------------------------------
% 133.06/40.44 % (1193722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193722)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193722)Termination reason: Instruction limit
% 133.06/40.44 % (1193722)Termination phase: Saturation
% 133.06/40.44 % (1193722)Time elapsed: 0.483 s
% 133.06/40.44 % (1193722)Peak memory usage: 101 MB
% 133.06/40.44 % (1193722)Instructions burned: 1085 (million)
% 133.06/40.44 % (1193724)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=794495489:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2748 on theBenchmark for (2748ds/1084Mi)
% 133.06/40.44 % (1193724)Instruction limit reached!
% 133.06/40.44 % (1193724)------------------------------
% 133.06/40.44 % (1193724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193724)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193724)Termination reason: Instruction limit
% 133.06/40.44 % (1193724)Termination phase: Saturation
% 133.06/40.44 % (1193724)Time elapsed: 0.671 s
% 133.06/40.44 % (1193724)Peak memory usage: 105 MB
% 133.06/40.44 % (1193724)Instructions burned: 1085 (million)
% 133.06/40.44 % (1193726)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2333549947:i=6995:s2at=5:gtg=all_2739 on theBenchmark for (2739ds/6995Mi)
% 133.06/40.44 % (1193705)Instruction limit reached!
% 133.06/40.44 % (1193705)------------------------------
% 133.06/40.44 % (1193705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193705)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193705)Termination reason: Instruction limit
% 133.06/40.44 % (1193705)Termination phase: Saturation
% 133.06/40.44 % (1193705)Time elapsed: 6.835 s
% 133.06/40.44 % (1193705)Peak memory usage: 297 MB
% 133.06/40.44 % (1193705)Instructions burned: 21613 (million)
% 133.06/40.44 % (1193728)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1451731692:st=2:i=6225:sd=15:ss=axioms_2733 on theBenchmark for (2733ds/6225Mi)
% 133.06/40.44 % (1193728)Instruction limit reached!
% 133.06/40.44 % (1193728)------------------------------
% 133.06/40.44 % (1193728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193728)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193728)Termination reason: Instruction limit
% 133.06/40.44 % (1193728)Termination phase: Saturation
% 133.06/40.44 % (1193728)Time elapsed: 1.851 s
% 133.06/40.44 % (1193728)Peak memory usage: 178 MB
% 133.06/40.44 % (1193728)Instructions burned: 6229 (million)
% 133.06/40.44 % (1193730)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1415569367:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2713 on theBenchmark for (2713ds/3372Mi)
% 133.06/40.44 % (1193720)Instruction limit reached!
% 133.06/40.44 % (1193720)------------------------------
% 133.06/40.44 % (1193720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193720)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193720)Termination reason: Instruction limit
% 133.06/40.44 % (1193720)Termination phase: Saturation
% 133.06/40.44 % (1193720)Time elapsed: 5.327 s
% 133.06/40.44 % (1193720)Peak memory usage: 183 MB
% 133.06/40.44 % (1193720)Instructions burned: 8329 (million)
% 133.06/40.44 % (1193732)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3694005615:st=2.3:i=26457:sd=10:ss=included:sgt=8_2708 on theBenchmark for (2708ds/26457Mi)
% 133.06/40.44 % (1193730)Instruction limit reached!
% 133.06/40.44 % (1193730)------------------------------
% 133.06/40.44 % (1193730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193730)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193730)Termination reason: Instruction limit
% 133.06/40.44 % (1193730)Termination phase: Saturation
% 133.06/40.44 % (1193730)Time elapsed: 1.261 s
% 133.06/40.44 % (1193730)Peak memory usage: 150 MB
% 133.06/40.44 % (1193730)Instructions burned: 3373 (million)
% 133.06/40.44 % (1193734)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=49962614:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2699 on theBenchmark for (2699ds/13494Mi)
% 133.06/40.44 % (1193726)Instruction limit reached!
% 133.06/40.44 % (1193726)------------------------------
% 133.06/40.44 % (1193726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193726)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193726)Termination reason: Instruction limit
% 133.06/40.44 % (1193726)Termination phase: Saturation
% 133.06/40.44 % (1193726)Time elapsed: 4.265 s
% 133.06/40.44 % (1193726)Peak memory usage: 172 MB
% 133.06/40.44 % (1193726)Instructions burned: 6996 (million)
% 133.06/40.44 % (1193736)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1280929312:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2695 on theBenchmark for (2695ds/2503Mi)
% 133.06/40.44 % (1193736)Instruction limit reached!
% 133.06/40.44 % (1193736)------------------------------
% 133.06/40.44 % (1193736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193736)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193736)Termination reason: Instruction limit
% 133.06/40.44 % (1193736)Termination phase: Saturation
% 133.06/40.44 % (1193736)Time elapsed: 1.566 s
% 133.06/40.44 % (1193736)Peak memory usage: 155 MB
% 133.06/40.44 % (1193736)Instructions burned: 2503 (million)
% 133.06/40.44 % (1193738)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3014352496:i=2559:sd=1:ep=RSTC:ss=axioms_2678 on theBenchmark for (2678ds/2559Mi)
% 133.06/40.44 % (1193738)Instruction limit reached!
% 133.06/40.44 % (1193738)------------------------------
% 133.06/40.44 % (1193738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193738)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193738)Termination reason: Instruction limit
% 133.06/40.44 % (1193738)Termination phase: Saturation
% 133.06/40.44 % (1193738)Time elapsed: 1.573 s
% 133.06/40.44 % (1193738)Peak memory usage: 149 MB
% 133.06/40.44 % (1193738)Instructions burned: 2559 (million)
% 133.06/40.44 % (1193740)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1061432902:i=30753:av=off:ss=included_2659 on theBenchmark for (2659ds/30753Mi)
% 133.06/40.44 % (1193734)Instruction limit reached!
% 133.06/40.44 % (1193734)------------------------------
% 133.06/40.44 % (1193734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/40.44 % (1193734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/40.44 % (1193734)CaDiCaL version: 2.1.3
% 133.06/40.44 % (1193734)Termination reason: Instruction limit
% 133.06/40.44 % (1193734)Termination phase: Saturation
% 133.06/40.44 % (1193734)Time elapsed: 4.564 s
% 133.06/40.44 % (1193734)Peak memory usage: 243 MB
% 133.06/40.44 % (1193734)Instructions burned: 13495 (million)
% 133.06/40.44 % (1193742)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=140798831:i=26473:ep=RSTC_2652 on theBenchmark for (2652ds/26473Mi)
% 133.06/40.44 % (1193732)First to succeed.
% 133.06/40.44 % (1193732)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1193596"
% 133.06/40.44 % (1193732)Refutation found. Thanks to Tanya!
% 133.06/40.44 % SZS status Theorem for theBenchmark
% 133.06/40.44 % SZS output start Proof for theBenchmark
% See solution above
% 280.72/40.64 % (1193732)------------------------------
% 280.72/40.64 % (1193732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 280.72/40.64 % (1193732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 280.72/40.64 % (1193732)CaDiCaL version: 2.1.3
% 280.72/40.64 % (1193732)Termination reason: Refutation
% 280.72/40.64 % (1193732)Time elapsed: 9.838 s
% 280.72/40.64 % (1193732)Peak memory usage: 240 MB
% 280.72/40.64 % (1193732)Instructions burned: 16025 (million)
% 280.72/40.64 % (1193732)------------------------------
% 280.72/40.64 % (1193732)------------------------------
% 280.72/40.64 % (1193596)Success in time 39.543 s
% 280.72/40.64 % Vampire exiting
%------------------------------------------------------------------------------