%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU331+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:23 PM UTC 2026
% Result : Theorem 5.42s 2.15s
% Output : Refutation 9.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 31
% Syntax : Number of formulae : 308 ( 18 unt; 23 def)
% Number of atoms : 1407 ( 351 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 1863 ( 764 ~; 841 |; 160 &)
% ( 38 <=>; 59 =>; 0 <=; 1 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 30 ( 28 usr; 23 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 4 con; 0-3 aty)
% Number of variables : 498 ( 0 sgn 443 !; 55 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [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(f2,negated_conjecture,
~ ! [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) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f33,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) ) )
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
=> ? [X2] :
( relation(X2)
& function(X2)
& ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X3,complements_of_subsets(the_carrier(X0),X1))
& in(X3,complements_of_subsets(the_carrier(X0),X1))
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X3
=> X4 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_funct_1__e4_7_1__tops_2__1) ).
fof(f36,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f37,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f38,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f39,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f53,axiom,
? [X0] :
( relation(X0)
& function(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_funct_1) ).
fof(f61,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
<=> in(X2,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(f65,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,[],[f2]) ).
fof(f66,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) ) )
& in(X2,complements_of_subsets(the_carrier(X0),X1))
& ! [X6] :
( element(X6,powerset(the_carrier(X0)))
=> ( X6 = X2
=> X4 = subset_complement(the_carrier(X0),X6) ) ) )
=> X3 = X4 )
=> ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( in(ordered_pair(X8,X9),X7)
<=> ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( element(X10,powerset(the_carrier(X0)))
=> ( X8 = X10
=> subset_complement(the_carrier(X0),X10) = X9 ) ) ) ) ) ) ),
inference(rectify,[],[f33]) ).
fof(f67,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] :
( 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,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,[],[f65]) ).
fof(f68,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] :
( 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,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,[],[f67]) ).
fof(f90,plain,
! [X0,X1] :
( ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( in(ordered_pair(X8,X9),X7)
<=> ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(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))) )
& in(X2,complements_of_subsets(the_carrier(X0),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,[],[f66]) ).
fof(f91,plain,
! [X0,X1] :
( ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( in(ordered_pair(X8,X9),X7)
<=> ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(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))) )
& in(X2,complements_of_subsets(the_carrier(X0),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,[],[f90]) ).
fof(f94,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f95,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f103,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( in(X2,X0)
<~> in(X2,X1) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f107,definition,
! [X1,X0] :
( ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( in(ordered_pair(X8,X9),X7)
<=> ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) ) ) )
| ~ sP0(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f108,plain,
! [X0,X1] :
( sP0(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))) )
& in(X2,complements_of_subsets(the_carrier(X0),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,[],[f91,f107]) ).
fof(f109,plain,
? [X0,X1] :
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| complements_of_subsets(the_carrier(X0),X1) != relation_dom(X2)
| ? [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)) ) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ in(X5,complements_of_subsets(the_carrier(X0),X1))
| ? [X8] :
( subset_complement(the_carrier(X0),X8) != X6
& X5 = X8
& element(X8,powerset(the_carrier(X0))) )
| ? [X9] :
( subset_complement(the_carrier(X0),X9) != X7
& X5 = X9
& element(X9,powerset(the_carrier(X0))) ) )
& ! [X10] :
( ~ in(X10,complements_of_subsets(the_carrier(X0),X1))
| ? [X11] :
! [X12] :
( subset_complement(the_carrier(X0),X12) = X11
| X10 != X12
| ~ element(X12,powerset(the_carrier(X0))) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(rectify,[],[f68]) ).
fof(f110,plain,
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != complements_of_subsets(the_carrier(sK1),sK2)
| ( apply(X2,sK3(X2)) != subset_complement(the_carrier(sK1),sK4(X2))
& sK3(X2) = sK4(X2)
& element(sK4(X2),powerset(the_carrier(sK1)))
& in(sK3(X2),complements_of_subsets(the_carrier(sK1),sK2)) ) )
& ! [X5,X6,X7] :
( X6 = X7
| ~ in(X5,complements_of_subsets(the_carrier(sK1),sK2))
| ( subset_complement(the_carrier(sK1),sK5(X5,X6)) != X6
& sK5(X5,X6) = X5
& element(sK5(X5,X6),powerset(the_carrier(sK1))) )
| ( subset_complement(the_carrier(sK1),sK6(X5,X7)) != X7
& sK6(X5,X7) = X5
& element(sK6(X5,X7),powerset(the_carrier(sK1))) ) )
& ! [X10] :
( ~ in(X10,complements_of_subsets(the_carrier(sK1),sK2))
| ! [X12] :
( sK7(X10) = subset_complement(the_carrier(sK1),X12)
| X10 != X12
| ~ element(X12,powerset(the_carrier(sK1))) ) )
& one_sorted_str(sK1)
& element(sK2,powerset(powerset(the_carrier(sK1)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X3,sK3(X2)),skolemize(X4,sK4(X2)),skolemize(X8,sK5(X5,X6)),skolemize(X9,sK6(X5,X7)),skolemize(X11,sK7(X10))],[f109]) ).
fof(f114,plain,
! [X1,X0] :
( ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( ( in(ordered_pair(X8,X9),X7)
| ~ in(X8,complements_of_subsets(the_carrier(X0),X1))
| ~ in(X8,complements_of_subsets(the_carrier(X0),X1))
| ? [X10] :
( subset_complement(the_carrier(X0),X10) != X9
& X8 = X10
& element(X10,powerset(the_carrier(X0))) ) )
& ( ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) )
| ~ in(ordered_pair(X8,X9),X7) ) ) )
| ~ sP0(X1,X0) ),
inference(nnf_transformation,[],[f107]) ).
fof(f115,plain,
! [X1,X0] :
( ? [X7] :
( relation(X7)
& function(X7)
& ! [X8,X9] :
( ( in(ordered_pair(X8,X9),X7)
| ~ in(X8,complements_of_subsets(the_carrier(X0),X1))
| ~ in(X8,complements_of_subsets(the_carrier(X0),X1))
| ? [X10] :
( subset_complement(the_carrier(X0),X10) != X9
& X8 = X10
& element(X10,powerset(the_carrier(X0))) ) )
& ( ( in(X8,complements_of_subsets(the_carrier(X0),X1))
& in(X8,complements_of_subsets(the_carrier(X0),X1))
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) )
| ~ in(ordered_pair(X8,X9),X7) ) ) )
| ~ sP0(X1,X0) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0,X1] :
( ? [X2] :
( relation(X2)
& function(X2)
& ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ? [X5] :
( subset_complement(the_carrier(X1),X5) != X4
& X3 = X5
& element(X5,powerset(the_carrier(X1))) ) )
& ( ( in(X3,complements_of_subsets(the_carrier(X1),X0))
& in(X3,complements_of_subsets(the_carrier(X1),X0))
& ! [X6] :
( subset_complement(the_carrier(X1),X6) = X4
| X3 != X6
| ~ element(X6,powerset(the_carrier(X1))) ) )
| ~ in(ordered_pair(X3,X4),X2) ) ) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( relation(sK11(X0,X1))
& function(sK11(X0,X1))
& ! [X3,X4] :
( ( in(ordered_pair(X3,X4),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ( subset_complement(the_carrier(X1),sK12(X1,X3,X4)) != X4
& sK12(X1,X3,X4) = X3
& element(sK12(X1,X3,X4),powerset(the_carrier(X1))) ) )
& ( ( in(X3,complements_of_subsets(the_carrier(X1),X0))
& in(X3,complements_of_subsets(the_carrier(X1),X0))
& ! [X6] :
( subset_complement(the_carrier(X1),X6) = X4
| X3 != X6
| ~ element(X6,powerset(the_carrier(X1))) ) )
| ~ in(ordered_pair(X3,X4),sK11(X0,X1)) ) ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X2,sK11(X0,X1)),skolemize(X5,sK12(X1,X3,X4))],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( sP0(X1,X0)
| ( sK14(X0,X1) != sK15(X0,X1)
& in(sK13(X0,X1),complements_of_subsets(the_carrier(X0),X1))
& ! [X5] :
( subset_complement(the_carrier(X0),X5) = sK14(X0,X1)
| sK13(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X0))) )
& in(sK13(X0,X1),complements_of_subsets(the_carrier(X0),X1))
& ! [X6] :
( subset_complement(the_carrier(X0),X6) = sK15(X0,X1)
| sK13(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,[sK13,sK14,sK15]),skolemize(X2,sK13(X0,X1)),skolemize(X3,sK14(X0,X1)),skolemize(X4,sK15(X0,X1))],[f108]) ).
fof(f119,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0) )
& ( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ) )
| ~ in(X1,relation_dom(X0)) )
& ( ( ( X2 = apply(X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| apply(X0,X1) != X2 ) )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f95]) ).
fof(f120,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] : ~ in(ordered_pair(X2,X3),X0) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f96]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X4] : in(ordered_pair(X2,X4),X0)
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( ? [X7] : in(ordered_pair(X5,X7),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ( ( ! [X3] : ~ in(ordered_pair(sK16(X0,X1),X3),X0)
| ~ in(sK16(X0,X1),X1) )
& ( in(ordered_pair(sK16(X0,X1),sK17(X0,X1)),X0)
| in(sK16(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( in(ordered_pair(X5,sK18(X0,X5)),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X2,sK16(X0,X1)),skolemize(X4,sK17(X0,X1)),skolemize(X7,sK18(X0,X5))],[f121]) ).
fof(f124,plain,
( relation(sK20)
& function(sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X0,sK20)],[f53]) ).
fof(f130,plain,
! [X0,X1] :
( X0 = X1
| ? [X2] :
( ( ~ in(X2,X1)
| ~ in(X2,X0) )
& ( in(X2,X1)
| in(X2,X0) ) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f131,plain,
! [X0,X1] :
( X0 = X1
| ( ( ~ in(sK26(X0,X1),X1)
| ~ in(sK26(X0,X1),X0) )
& ( in(sK26(X0,X1),X1)
| in(sK26(X0,X1),X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X2,sK26(X0,X1))],[f130]) ).
fof(f132,plain,
element(sK2,powerset(powerset(the_carrier(sK1)))),
inference(cnf_transformation,[],[f110]) ).
fof(f133,plain,
one_sorted_str(sK1),
inference(cnf_transformation,[],[f110]) ).
fof(f134,plain,
! [X10,X12] :
( ~ in(X10,complements_of_subsets(the_carrier(sK1),sK2))
| sK7(X10) = subset_complement(the_carrier(sK1),X12)
| X10 != X12
| ~ element(X12,powerset(the_carrier(sK1))) ),
inference(cnf_transformation,[],[f110]) ).
fof(f135,plain,
! [X6,X7,X5] :
( ~ in(X5,complements_of_subsets(the_carrier(sK1),sK2))
| X6 = X7
| element(sK5(X5,X6),powerset(the_carrier(sK1)))
| element(sK6(X5,X7),powerset(the_carrier(sK1))) ),
inference(cnf_transformation,[],[f110]) ).
fof(f136,plain,
! [X6,X7,X5] :
( ~ in(X5,complements_of_subsets(the_carrier(sK1),sK2))
| X6 = X7
| element(sK5(X5,X6),powerset(the_carrier(sK1)))
| sK6(X5,X7) = X5 ),
inference(cnf_transformation,[],[f110]) ).
fof(f138,plain,
! [X6,X7,X5] :
( ~ in(X5,complements_of_subsets(the_carrier(sK1),sK2))
| X6 = X7
| sK5(X5,X6) = X5
| element(sK6(X5,X7),powerset(the_carrier(sK1))) ),
inference(cnf_transformation,[],[f110]) ).
fof(f139,plain,
! [X6,X7,X5] :
( ~ in(X5,complements_of_subsets(the_carrier(sK1),sK2))
| X6 = X7
| sK5(X5,X6) = X5
| sK6(X5,X7) = X5 ),
inference(cnf_transformation,[],[f110]) ).
fof(f144,plain,
! [X2] :
( in(sK3(X2),complements_of_subsets(the_carrier(sK1),sK2))
| ~ function(X2)
| relation_dom(X2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f145,plain,
! [X2] :
( relation_dom(X2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ function(X2)
| ~ relation(X2)
| element(sK4(X2),powerset(the_carrier(sK1))) ),
inference(cnf_transformation,[],[f110]) ).
fof(f146,plain,
! [X2] :
( relation_dom(X2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ function(X2)
| ~ relation(X2)
| sK3(X2) = sK4(X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f147,plain,
! [X2] :
( apply(X2,sK3(X2)) != subset_complement(the_carrier(sK1),sK4(X2))
| ~ function(X2)
| relation_dom(X2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f110]) ).
fof(f203,plain,
! [X3,X0,X1,X6,X4] :
( subset_complement(the_carrier(X1),X6) = X4
| X3 != X6
| ~ element(X6,powerset(the_carrier(X1)))
| ~ in(ordered_pair(X3,X4),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f204,plain,
! [X3,X0,X1,X4] :
( in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(ordered_pair(X3,X4),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f207,plain,
! [X3,X0,X1,X4] :
( in(ordered_pair(X3,X4),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| sK12(X1,X3,X4) = X3
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f208,plain,
! [X3,X0,X1,X4] :
( in(ordered_pair(X3,X4),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| subset_complement(the_carrier(X1),sK12(X1,X3,X4)) != X4
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f209,plain,
! [X0,X1] :
( function(sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f210,plain,
! [X0,X1] :
( relation(sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f211,plain,
! [X0,X1,X6] :
( sP0(X1,X0)
| subset_complement(the_carrier(X0),X6) = sK15(X0,X1)
| sK13(X0,X1) != X6
| ~ element(X6,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f118]) ).
fof(f212,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| in(sK13(X0,X1),complements_of_subsets(the_carrier(X0),X1))
| sP0(X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f118]) ).
fof(f213,plain,
! [X0,X1,X5] :
( sP0(X1,X0)
| subset_complement(the_carrier(X0),X5) = sK14(X0,X1)
| sK13(X0,X1) != X5
| ~ element(X5,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f118]) ).
fof(f215,plain,
! [X0,X1] :
( sK14(X0,X1) != sK15(X0,X1)
| sP0(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f118]) ).
fof(f218,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f219,plain,
! [X2,X0,X1] :
( empty_set = X2
| apply(X0,X1) != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f221,plain,
! [X2,X0,X1] :
( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f222,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f223,plain,
! [X0,X1,X5] :
( in(ordered_pair(X5,sK18(X0,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f224,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f227,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f39]) ).
fof(f241,plain,
function(sK20),
inference(cnf_transformation,[],[f124]) ).
fof(f242,plain,
relation(sK20),
inference(cnf_transformation,[],[f124]) ).
fof(f253,plain,
! [X0,X1] :
( in(sK26(X0,X1),X1)
| in(sK26(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f131]) ).
fof(f254,plain,
! [X0,X1] :
( ~ in(sK26(X0,X1),X1)
| X0 = X1
| ~ in(sK26(X0,X1),X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f258,plain,
! [X3,X0,X1,X4] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| subset_complement(the_carrier(X1),sK12(X1,X3,X4)) != X4
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f208,f227]) ).
fof(f259,plain,
! [X3,X0,X1,X4] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| sK12(X1,X3,X4) = X3
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f207,f227]) ).
fof(f262,plain,
! [X3,X0,X1,X4] :
( in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f204,f227]) ).
fof(f263,plain,
! [X3,X0,X1,X6,X4] :
( subset_complement(the_carrier(X1),X6) = X4
| X3 != X6
| ~ element(X6,powerset(the_carrier(X1)))
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f203,f227]) ).
fof(f264,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f222,f227]) ).
fof(f265,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f221,f227]) ).
fof(f268,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f224,f227]) ).
fof(f269,plain,
! [X0,X1,X5] :
( in(unordered_pair(unordered_pair(X5,sK18(X0,X5)),singleton(X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f223,f227]) ).
fof(f271,plain,
! [X12] :
( ~ element(X12,powerset(the_carrier(sK1)))
| subset_complement(the_carrier(sK1),X12) = sK7(X12)
| ~ in(X12,complements_of_subsets(the_carrier(sK1),sK2)) ),
inference(equality_resolution,[],[f134]) ).
fof(f272,plain,
! [X0,X1,X6,X4] :
( subset_complement(the_carrier(X1),X6) = X4
| ~ element(X6,powerset(the_carrier(X1)))
| ~ in(unordered_pair(unordered_pair(X6,X4),singleton(X6)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(equality_resolution,[],[f263]) ).
fof(f273,plain,
! [X0,X1] :
( ~ element(sK13(X0,X1),powerset(the_carrier(X0)))
| sK14(X0,X1) = subset_complement(the_carrier(X0),sK13(X0,X1))
| sP0(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f213]) ).
fof(f274,plain,
! [X0,X1] :
( ~ element(sK13(X0,X1),powerset(the_carrier(X0)))
| sK15(X0,X1) = subset_complement(the_carrier(X0),sK13(X0,X1))
| sP0(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f211]) ).
fof(f275,plain,
! [X0,X1] :
( ~ function(X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| in(unordered_pair(unordered_pair(X1,apply(X0,X1)),singleton(X1)),X0) ),
inference(equality_resolution,[],[f265]) ).
fof(f277,plain,
! [X0,X1] :
( in(X1,relation_dom(X0))
| apply(X0,X1) = empty_set
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f219]) ).
fof(f278,plain,
! [X0,X6,X5] :
( ~ relation(X0)
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| in(X5,relation_dom(X0)) ),
inference(equality_resolution,[],[f268]) ).
fof(f279,plain,
! [X0,X5] :
( ~ relation(X0)
| ~ in(X5,relation_dom(X0))
| in(unordered_pair(unordered_pair(X5,sK18(X0,X5)),singleton(X5)),X0) ),
inference(equality_resolution,[],[f269]) ).
fof(f281,plain,
! [X3,X0,X1,X4] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| sK12(X1,X3,X4) = X3
| ~ sP0(X0,X1) ),
inference(duplicate_literal_removal,[],[f259]) ).
fof(f282,plain,
! [X3,X0,X1,X4] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK11(X0,X1))
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| subset_complement(the_carrier(X1),sK12(X1,X3,X4)) != X4
| ~ sP0(X0,X1) ),
inference(duplicate_literal_removal,[],[f258]) ).
fof(f283,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| ~ relation(X0)
| ~ function(X0) ),
inference(forward_subsumption_resolution,[],[f264,f278]) ).
fof(f284,plain,
! [X0,X1,X6,X4] :
( ~ element(X6,powerset(the_carrier(X1)))
| subset_complement(the_carrier(X1),X6) = X4
| ~ in(unordered_pair(singleton(X6),unordered_pair(X6,X4)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(forward_demodulation,[],[f272,f218]) ).
fof(f285,plain,
! [X3,X0,X1,X4] :
( ~ sP0(X0,X1)
| in(X3,complements_of_subsets(the_carrier(X1),X0))
| ~ in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),sK11(X0,X1)) ),
inference(forward_demodulation,[],[f262,f218]) ).
fof(f288,plain,
! [X3,X0,X1,X4] :
( ~ sP0(X0,X1)
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| sK12(X1,X3,X4) = X3
| in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),sK11(X0,X1)) ),
inference(forward_demodulation,[],[f281,f218]) ).
fof(f289,plain,
! [X3,X0,X1,X4] :
( subset_complement(the_carrier(X1),sK12(X1,X3,X4)) != X4
| ~ in(X3,complements_of_subsets(the_carrier(X1),X0))
| in(unordered_pair(singleton(X3),unordered_pair(X3,X4)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(forward_demodulation,[],[f282,f218]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ function(X0)
| apply(X0,X1) = X2
| ~ relation(X0)
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),X0) ),
inference(forward_demodulation,[],[f283,f218]) ).
fof(f295,plain,
! [X0] :
( ~ element(X0,powerset(powerset(the_carrier(sK1))))
| sP0(X0,sK1)
| in(sK13(sK1,X0),complements_of_subsets(the_carrier(sK1),X0)) ),
inference(resolution,[],[f212,f133]) ).
fof(f305,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK11(X2,X3))
| in(X0,relation_dom(sK11(X2,X3)))
| ~ sP0(X2,X3) ),
inference(resolution,[],[f278,f210]) ).
fof(f306,plain,
! [X2,X3,X0,X1] :
( ~ sP0(X2,X3)
| in(X0,relation_dom(sK11(X2,X3)))
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(X2,X3)) ),
inference(forward_demodulation,[],[f305,f218]) ).
fof(f307,plain,
! [X2,X3,X0,X1] :
( apply(sK11(X0,X1),X2) = X3
| ~ relation(sK11(X0,X1))
| ~ in(unordered_pair(singleton(X2),unordered_pair(X2,X3)),sK11(X0,X1))
| ~ sP0(X0,X1) ),
inference(resolution,[],[f290,f209]) ).
fof(f308,plain,
! [X2,X3,X0,X1] :
( ~ sP0(X0,X1)
| ~ in(unordered_pair(singleton(X2),unordered_pair(X2,X3)),sK11(X0,X1))
| apply(sK11(X0,X1),X2) = X3 ),
inference(forward_subsumption_resolution,[],[f307,f210]) ).
fof(f309,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(sK11(X1,X2)))
| ~ relation(sK11(X1,X2))
| in(unordered_pair(unordered_pair(X0,apply(sK11(X1,X2),X0)),singleton(X0)),sK11(X1,X2))
| ~ sP0(X1,X2) ),
inference(resolution,[],[f275,f209]) ).
fof(f310,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(sK11(X1,X2)))
| in(unordered_pair(unordered_pair(X0,apply(sK11(X1,X2),X0)),singleton(X0)),sK11(X1,X2))
| ~ sP0(X1,X2) ),
inference(forward_subsumption_resolution,[],[f309,f210]) ).
fof(f311,plain,
! [X2,X0,X1] :
( ~ sP0(X1,X2)
| ~ in(X0,relation_dom(sK11(X1,X2)))
| in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(X1,X2),X0))),sK11(X1,X2)) ),
inference(forward_demodulation,[],[f310,f218]) ).
fof(f315,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(sK11(X1,X2)))
| in(unordered_pair(unordered_pair(X0,sK18(sK11(X1,X2),X0)),singleton(X0)),sK11(X1,X2))
| ~ sP0(X1,X2) ),
inference(resolution,[],[f279,f210]) ).
fof(f316,plain,
! [X2,X0,X1] :
( ~ sP0(X1,X2)
| ~ in(X0,relation_dom(sK11(X1,X2)))
| in(unordered_pair(singleton(X0),unordered_pair(X0,sK18(sK11(X1,X2),X0))),sK11(X1,X2)) ),
inference(forward_demodulation,[],[f315,f218]) ).
fof(f317,plain,
( sP0(sK2,sK1)
| in(sK13(sK1,sK2),complements_of_subsets(the_carrier(sK1),sK2)) ),
inference(resolution,[],[f295,f132]) ).
fof(f319,definition,
( spl27_1
<=> in(sK13(sK1,sK2),complements_of_subsets(the_carrier(sK1),sK2)) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f320,plain,
( in(sK13(sK1,sK2),complements_of_subsets(the_carrier(sK1),sK2))
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,definition,
( spl27_2
<=> sP0(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f323,plain,
( sP0(sK2,sK1)
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( spl27_1
| spl27_2 ),
inference(avatar_split_clause,[],[f317,f322,f319]) ).
fof(f405,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK11(sK2,sK1)))
| in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(sK2,sK1),X0))),sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f311,f323]) ).
fof(f407,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(sK2,sK1),X0))),sK11(sK2,sK1))
| empty_set = apply(sK11(sK2,sK1),X0)
| ~ relation(sK11(sK2,sK1))
| ~ function(sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f405,f277]) ).
fof(f411,definition,
( spl27_7
<=> function(sK11(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f412,plain,
( ~ function(sK11(sK2,sK1))
| spl27_7 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,definition,
( spl27_8
<=> relation(sK11(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
fof(f415,plain,
( ~ relation(sK11(sK2,sK1))
| spl27_8 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,definition,
( spl27_9
<=> ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(sK2,sK1),X0))),sK11(sK2,sK1))
| empty_set = apply(sK11(sK2,sK1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f418,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(sK2,sK1),X0))),sK11(sK2,sK1))
| empty_set = apply(sK11(sK2,sK1),X0) )
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( ~ spl27_7
| ~ spl27_8
| spl27_9
| ~ spl27_2 ),
inference(avatar_split_clause,[],[f407,f322,f417,f414,f411]) ).
fof(f421,plain,
( ~ sP0(sK2,sK1)
| spl27_7 ),
inference(resolution,[],[f412,f209]) ).
fof(f423,plain,
( $false
| ~ spl27_2
| spl27_7 ),
inference(forward_subsumption_resolution,[],[f421,f323]) ).
fof(f424,plain,
( ~ spl27_2
| spl27_7 ),
inference(avatar_contradiction_clause,[],[f423]) ).
fof(f459,definition,
( spl27_11
<=> element(sK13(sK1,sK2),powerset(the_carrier(sK1))) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f460,plain,
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f468,plain,
( ~ sP0(sK2,sK1)
| spl27_8 ),
inference(resolution,[],[f415,f210]) ).
fof(f469,plain,
( $false
| ~ spl27_2
| spl27_8 ),
inference(forward_subsumption_resolution,[],[f468,f323]) ).
fof(f470,plain,
( ~ spl27_2
| spl27_8 ),
inference(avatar_contradiction_clause,[],[f469]) ).
fof(f474,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| apply(sK11(sK2,sK1),X0) = X1 )
| ~ spl27_2 ),
inference(resolution,[],[f323,f308]) ).
fof(f475,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| in(X0,complements_of_subsets(the_carrier(sK1),sK2)) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f285]) ).
fof(f476,plain,
( ! [X0,X1] :
( ~ in(X0,complements_of_subsets(the_carrier(sK1),sK2))
| sK12(sK1,X0,X1) = X0
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f288]) ).
fof(f484,plain,
( ! [X0] :
( in(X0,complements_of_subsets(the_carrier(sK1),sK2))
| empty_set = apply(sK11(sK2,sK1),X0) )
| ~ spl27_2
| ~ spl27_9 ),
inference(resolution,[],[f418,f475]) ).
fof(f488,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| sK12(sK1,X0,X1) = X0
| empty_set = apply(sK11(sK2,sK1),X0) )
| ~ spl27_2
| ~ spl27_9 ),
inference(resolution,[],[f484,f476]) ).
fof(f599,definition,
( spl27_18
<=> complements_of_subsets(the_carrier(sK1),sK2) = relation_dom(sK11(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_18])],[avatar_definition]) ).
fof(f600,plain,
( complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| spl27_18 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f1066,plain,
( ! [X0,X1] :
( sK12(sK1,X0,X1) = X0
| empty_set = apply(sK11(sK2,sK1),X0)
| apply(sK11(sK2,sK1),X0) = X1 )
| ~ spl27_2
| ~ spl27_9 ),
inference(resolution,[],[f488,f474]) ).
fof(f1173,plain,
( ! [X0,X1] :
( element(sK5(sK13(sK1,sK2),X0),powerset(the_carrier(sK1)))
| element(sK6(sK13(sK1,sK2),X1),powerset(the_carrier(sK1)))
| X0 = X1 )
| ~ spl27_1 ),
inference(resolution,[],[f320,f135]) ).
fof(f1174,plain,
( ! [X0,X1] :
( element(sK5(sK13(sK1,sK2),X0),powerset(the_carrier(sK1)))
| X0 = X1
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),X1) )
| ~ spl27_1 ),
inference(resolution,[],[f320,f136]) ).
fof(f1175,plain,
( ! [X0,X1] :
( element(sK6(sK13(sK1,sK2),X1),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),X0)
| X0 = X1 )
| ~ spl27_1 ),
inference(resolution,[],[f320,f138]) ).
fof(f1176,plain,
( ! [X0,X1] :
( X0 = X1
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),X0)
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),X1) )
| ~ spl27_1 ),
inference(resolution,[],[f320,f139]) ).
fof(f1178,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK15(sK1,sK2)
| sP0(sK2,sK1)
| ~ one_sorted_str(sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_11 ),
inference(resolution,[],[f460,f274]) ).
fof(f1179,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK14(sK1,sK2)
| sP0(sK2,sK1)
| ~ one_sorted_str(sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_11 ),
inference(resolution,[],[f460,f273]) ).
fof(f1180,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK7(sK13(sK1,sK2))
| ~ in(sK13(sK1,sK2),complements_of_subsets(the_carrier(sK1),sK2))
| ~ spl27_11 ),
inference(resolution,[],[f460,f271]) ).
fof(f1186,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK7(sK13(sK1,sK2))
| ~ spl27_1
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f1180,f320]) ).
fof(f1187,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK14(sK1,sK2)
| sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f1179,f133]) ).
fof(f1188,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK15(sK1,sK2)
| sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f1178,f133]) ).
fof(f1189,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK14(sK1,sK2)
| sP0(sK2,sK1)
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f1187,f132]) ).
fof(f1190,plain,
( subset_complement(the_carrier(sK1),sK13(sK1,sK2)) = sK15(sK1,sK2)
| sP0(sK2,sK1)
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f1188,f132]) ).
fof(f1191,plain,
( sK7(sK13(sK1,sK2)) = sK14(sK1,sK2)
| sP0(sK2,sK1)
| ~ spl27_1
| ~ spl27_11 ),
inference(forward_demodulation,[],[f1189,f1186]) ).
fof(f1192,plain,
( sK7(sK13(sK1,sK2)) = sK15(sK1,sK2)
| sP0(sK2,sK1)
| ~ spl27_1
| ~ spl27_11 ),
inference(forward_demodulation,[],[f1190,f1186]) ).
fof(f1194,definition,
( spl27_34
<=> sK7(sK13(sK1,sK2)) = sK14(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition]) ).
fof(f1195,plain,
( sK7(sK13(sK1,sK2)) = sK14(sK1,sK2)
| ~ spl27_34 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1196,plain,
( spl27_2
| spl27_34
| ~ spl27_1
| ~ spl27_11 ),
inference(avatar_split_clause,[],[f1191,f459,f319,f1194,f322]) ).
fof(f1198,definition,
( spl27_35
<=> sK7(sK13(sK1,sK2)) = sK15(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition]) ).
fof(f1199,plain,
( sK7(sK13(sK1,sK2)) = sK15(sK1,sK2)
| ~ spl27_35 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1200,plain,
( spl27_2
| spl27_35
| ~ spl27_1
| ~ spl27_11 ),
inference(avatar_split_clause,[],[f1192,f459,f319,f1198,f322]) ).
fof(f1207,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| in(X0,complements_of_subsets(the_carrier(sK1),sK2)) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f285]) ).
fof(f1209,plain,
( ! [X0,X1] :
( ~ in(X0,complements_of_subsets(the_carrier(sK1),sK2))
| sK12(sK1,X0,X1) = X0
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f288]) ).
fof(f1210,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| in(X0,relation_dom(sK11(sK2,sK1))) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f306]) ).
fof(f1211,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK11(sK2,sK1))
| apply(sK11(sK2,sK1),X0) = X1 )
| ~ spl27_2 ),
inference(resolution,[],[f323,f308]) ).
fof(f1212,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK11(sK2,sK1)))
| in(unordered_pair(singleton(X0),unordered_pair(X0,apply(sK11(sK2,sK1),X0))),sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f323,f311]) ).
fof(f1221,plain,
( ! [X0] :
( sK13(sK1,sK2) != X0
| sK6(sK13(sK1,sK2),X0) = X0
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),sK6(sK13(sK1,sK2),X0)) )
| ~ spl27_1 ),
inference(equality_factoring,[],[f1176]) ).
fof(f2762,plain,
( sK13(sK1,sK2) = sK6(sK13(sK1,sK2),sK13(sK1,sK2))
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),sK6(sK13(sK1,sK2),sK13(sK1,sK2)))
| ~ spl27_1 ),
inference(equality_resolution,[],[f1221]) ).
fof(f2764,definition,
( spl27_59
<=> sK13(sK1,sK2) = sK5(sK13(sK1,sK2),sK6(sK13(sK1,sK2),sK13(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl27_59])],[avatar_definition]) ).
fof(f2765,plain,
( sK13(sK1,sK2) = sK5(sK13(sK1,sK2),sK6(sK13(sK1,sK2),sK13(sK1,sK2)))
| ~ spl27_59 ),
inference(avatar_component_clause,[],[f2764]) ).
fof(f2767,definition,
( spl27_60
<=> sK13(sK1,sK2) = sK6(sK13(sK1,sK2),sK13(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl27_60])],[avatar_definition]) ).
fof(f2768,plain,
( sK13(sK1,sK2) = sK6(sK13(sK1,sK2),sK13(sK1,sK2))
| ~ spl27_60 ),
inference(avatar_component_clause,[],[f2767]) ).
fof(f2769,plain,
( spl27_59
| spl27_60
| ~ spl27_1 ),
inference(avatar_split_clause,[],[f2762,f319,f2767,f2764]) ).
fof(f2825,definition,
( spl27_61
<=> ! [X0] :
( sK13(sK1,sK2) = X0
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_61])],[avatar_definition]) ).
fof(f2826,plain,
( ! [X0] :
( sK13(sK1,sK2) = sK5(sK13(sK1,sK2),X0)
| sK13(sK1,sK2) = X0 )
| ~ spl27_61 ),
inference(avatar_component_clause,[],[f2825]) ).
fof(f2843,definition,
( spl27_64
<=> ! [X0] :
( sK6(sK13(sK1,sK2),sK13(sK1,sK2)) = X0
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_64])],[avatar_definition]) ).
fof(f2844,plain,
( ! [X0] :
( sK6(sK13(sK1,sK2),sK13(sK1,sK2)) = X0
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),X0) )
| ~ spl27_64 ),
inference(avatar_component_clause,[],[f2843]) ).
fof(f2853,plain,
( ! [X0] :
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| element(sK5(sK13(sK1,sK2),X0),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = X0 )
| ~ spl27_1
| ~ spl27_60 ),
inference(superposition,[],[f1173,f2768]) ).
fof(f2854,plain,
( ! [X0] :
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = sK5(sK13(sK1,sK2),X0)
| sK13(sK1,sK2) = X0 )
| ~ spl27_1
| ~ spl27_60 ),
inference(superposition,[],[f1175,f2768]) ).
fof(f3126,plain,
( ! [X0] :
( subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != X0
| ~ function(sK11(sK2,sK1))
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| sK3(sK11(sK2,sK1)) = sK12(sK1,sK3(sK11(sK2,sK1)),X0)
| empty_set = apply(sK11(sK2,sK1),sK3(sK11(sK2,sK1))) )
| ~ spl27_2
| ~ spl27_9 ),
inference(superposition,[],[f147,f1066]) ).
fof(f3572,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),X0)),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),X0),apply(sK11(sK2,sK1),sK26(relation_dom(sK11(sK2,sK1)),X0)))),sK11(sK2,sK1))
| in(sK26(relation_dom(sK11(sK2,sK1)),X0),X0)
| relation_dom(sK11(sK2,sK1)) = X0 )
| ~ spl27_2 ),
inference(resolution,[],[f1212,f253]) ).
fof(f3580,plain,
( ! [X0] :
( in(sK26(relation_dom(sK11(sK2,sK1)),X0),X0)
| in(sK26(relation_dom(sK11(sK2,sK1)),X0),complements_of_subsets(the_carrier(sK1),sK2))
| relation_dom(sK11(sK2,sK1)) = X0 )
| ~ spl27_2 ),
inference(resolution,[],[f3572,f1207]) ).
fof(f3613,plain,
( in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),complements_of_subsets(the_carrier(sK1),sK2))
| complements_of_subsets(the_carrier(sK1),sK2) = relation_dom(sK11(sK2,sK1))
| ~ spl27_2 ),
inference(factoring,[],[f3580]) ).
fof(f3616,plain,
( in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),complements_of_subsets(the_carrier(sK1),sK2))
| ~ spl27_2
| spl27_18 ),
inference(forward_subsumption_resolution,[],[f3613,f600]) ).
fof(f3618,plain,
( complements_of_subsets(the_carrier(sK1),sK2) = relation_dom(sK11(sK2,sK1))
| ~ in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),relation_dom(sK11(sK2,sK1)))
| ~ spl27_2
| spl27_18 ),
inference(resolution,[],[f3616,f254]) ).
fof(f3620,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)),sK11(sK2,sK1))
| sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)) = sK12(sK1,sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0) )
| ~ spl27_2
| spl27_18 ),
inference(resolution,[],[f3616,f1209]) ).
fof(f3626,plain,
( ~ in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),relation_dom(sK11(sK2,sK1)))
| ~ spl27_2
| spl27_18 ),
inference(forward_subsumption_resolution,[],[f3618,f600]) ).
fof(f3638,plain,
( ! [X0] :
( sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)) = sK12(sK1,sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)
| in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),relation_dom(sK11(sK2,sK1))) )
| ~ spl27_2
| spl27_18 ),
inference(resolution,[],[f3620,f1210]) ).
fof(f3644,plain,
( ! [X0] : sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)) = sK12(sK1,sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)
| ~ spl27_2
| spl27_18 ),
inference(forward_subsumption_resolution,[],[f3638,f3626]) ).
fof(f3646,plain,
( ! [X0,X1] :
( ~ sP0(X1,sK1)
| ~ in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)),sK11(X1,sK1))
| subset_complement(the_carrier(sK1),sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))) != X0 )
| ~ spl27_2
| spl27_18 ),
inference(superposition,[],[f289,f3644]) ).
fof(f3663,plain,
( ! [X0] :
( ~ in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),complements_of_subsets(the_carrier(sK1),sK2))
| in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)),sK11(sK2,sK1))
| subset_complement(the_carrier(sK1),sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))) != X0 )
| ~ spl27_2
| spl27_18 ),
inference(resolution,[],[f3646,f323]) ).
fof(f3664,plain,
( ! [X0] :
( subset_complement(the_carrier(sK1),sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))) != X0
| in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),X0)),sK11(sK2,sK1)) )
| ~ spl27_2
| spl27_18 ),
inference(forward_subsumption_resolution,[],[f3663,f3616]) ).
fof(f3667,plain,
( in(unordered_pair(singleton(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))),unordered_pair(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),subset_complement(the_carrier(sK1),sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))))),sK11(sK2,sK1))
| ~ spl27_2
| spl27_18 ),
inference(equality_resolution,[],[f3664]) ).
fof(f3672,plain,
( in(sK26(relation_dom(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)),relation_dom(sK11(sK2,sK1)))
| ~ spl27_2
| spl27_18 ),
inference(resolution,[],[f3667,f1210]) ).
fof(f3678,plain,
( $false
| ~ spl27_2
| spl27_18 ),
inference(forward_subsumption_resolution,[],[f3672,f3626]) ).
fof(f3679,plain,
( ~ spl27_2
| spl27_18 ),
inference(avatar_contradiction_clause,[],[f3678]) ).
fof(f3682,definition,
( spl27_74
<=> empty_set = apply(sK11(sK2,sK1),sK3(sK11(sK2,sK1))) ),
introduced(definition,[new_symbols(definition,[spl27_74])],[avatar_definition]) ).
fof(f3683,plain,
( empty_set = apply(sK11(sK2,sK1),sK3(sK11(sK2,sK1)))
| ~ spl27_74 ),
inference(avatar_component_clause,[],[f3682]) ).
fof(f3685,definition,
( spl27_75
<=> ! [X0] :
( subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != X0
| sK3(sK11(sK2,sK1)) = sK12(sK1,sK3(sK11(sK2,sK1)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_75])],[avatar_definition]) ).
fof(f3686,plain,
( ! [X0] :
( sK3(sK11(sK2,sK1)) = sK12(sK1,sK3(sK11(sK2,sK1)),X0)
| subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != X0 )
| ~ spl27_75 ),
inference(avatar_component_clause,[],[f3685]) ).
fof(f3687,plain,
( spl27_74
| ~ spl27_8
| ~ spl27_18
| ~ spl27_7
| spl27_75
| ~ spl27_2
| ~ spl27_9 ),
inference(avatar_split_clause,[],[f3126,f417,f322,f3685,f411,f599,f414,f3682]) ).
fof(f3695,plain,
( complements_of_subsets(the_carrier(sK1),sK2) = relation_dom(sK11(sK2,sK1))
| ~ spl27_18 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f3712,plain,
( complements_of_subsets(the_carrier(sK1),sK2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| element(sK4(sK11(sK2,sK1)),powerset(the_carrier(sK1)))
| ~ spl27_18 ),
inference(superposition,[],[f145,f3695]) ).
fof(f3713,plain,
( complements_of_subsets(the_carrier(sK1),sK2) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| sK3(sK11(sK2,sK1)) = sK4(sK11(sK2,sK1))
| ~ spl27_18 ),
inference(superposition,[],[f146,f3695]) ).
fof(f3723,plain,
( ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| sK3(sK11(sK2,sK1)) = sK4(sK11(sK2,sK1))
| ~ spl27_18 ),
inference(trivial_inequality_removal,[],[f3713]) ).
fof(f3724,plain,
( ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| element(sK4(sK11(sK2,sK1)),powerset(the_carrier(sK1)))
| ~ spl27_18 ),
inference(trivial_inequality_removal,[],[f3712]) ).
fof(f3742,definition,
( spl27_83
<=> sK3(sK11(sK2,sK1)) = sK4(sK11(sK2,sK1)) ),
introduced(definition,[new_symbols(definition,[spl27_83])],[avatar_definition]) ).
fof(f3743,plain,
( sK3(sK11(sK2,sK1)) = sK4(sK11(sK2,sK1))
| ~ spl27_83 ),
inference(avatar_component_clause,[],[f3742]) ).
fof(f3744,plain,
( spl27_83
| ~ spl27_8
| ~ spl27_7
| ~ spl27_18 ),
inference(avatar_split_clause,[],[f3723,f599,f411,f414,f3742]) ).
fof(f3746,definition,
( spl27_84
<=> element(sK4(sK11(sK2,sK1)),powerset(the_carrier(sK1))) ),
introduced(definition,[new_symbols(definition,[spl27_84])],[avatar_definition]) ).
fof(f3747,plain,
( element(sK4(sK11(sK2,sK1)),powerset(the_carrier(sK1)))
| ~ spl27_84 ),
inference(avatar_component_clause,[],[f3746]) ).
fof(f3748,plain,
( spl27_84
| ~ spl27_8
| ~ spl27_7
| ~ spl27_18 ),
inference(avatar_split_clause,[],[f3724,f599,f411,f414,f3746]) ).
fof(f3749,plain,
( element(sK3(sK11(sK2,sK1)),powerset(the_carrier(sK1)))
| ~ spl27_83
| ~ spl27_84 ),
inference(forward_demodulation,[],[f3747,f3743]) ).
fof(f3798,plain,
( empty_set != subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_74 ),
inference(superposition,[],[f147,f3683]) ).
fof(f3800,plain,
( subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) = sK7(sK3(sK11(sK2,sK1)))
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))
| ~ spl27_83
| ~ spl27_84 ),
inference(resolution,[],[f3749,f271]) ).
fof(f3801,plain,
( ! [X0,X1] :
( ~ sP0(X1,sK1)
| ~ in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) = X0 )
| ~ spl27_83
| ~ spl27_84 ),
inference(resolution,[],[f3749,f284]) ).
fof(f3807,definition,
( spl27_91
<=> in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2)) ),
introduced(definition,[new_symbols(definition,[spl27_91])],[avatar_definition]) ).
fof(f3808,plain,
( ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))
| spl27_91 ),
inference(avatar_component_clause,[],[f3807]) ).
fof(f3810,definition,
( spl27_92
<=> subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) = sK7(sK3(sK11(sK2,sK1))) ),
introduced(definition,[new_symbols(definition,[spl27_92])],[avatar_definition]) ).
fof(f3811,plain,
( subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) = sK7(sK3(sK11(sK2,sK1)))
| ~ spl27_92 ),
inference(avatar_component_clause,[],[f3810]) ).
fof(f3812,plain,
( ~ spl27_91
| spl27_92
| ~ spl27_83
| ~ spl27_84 ),
inference(avatar_split_clause,[],[f3800,f3746,f3742,f3810,f3807]) ).
fof(f3813,plain,
( ~ function(sK11(sK2,sK1))
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| spl27_91 ),
inference(resolution,[],[f3808,f144]) ).
fof(f3815,plain,
( ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_18
| spl27_91 ),
inference(forward_subsumption_resolution,[],[f3813,f3695]) ).
fof(f3816,plain,
( ~ spl27_8
| ~ spl27_7
| ~ spl27_18
| spl27_91 ),
inference(avatar_split_clause,[],[f3815,f3807,f599,f411,f414]) ).
fof(f3903,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) != X0
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| ~ sP0(X1,sK1)
| subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != X0 )
| ~ spl27_75 ),
inference(superposition,[],[f289,f3686]) ).
fof(f3904,plain,
( ! [X0,X1] :
( sK7(sK3(sK11(sK2,sK1))) != X0
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| ~ sP0(X1,sK1)
| subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != X0 )
| ~ spl27_75
| ~ spl27_92 ),
inference(forward_demodulation,[],[f3903,f3811]) ).
fof(f3905,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) != X0
| sK7(sK3(sK11(sK2,sK1))) != X0
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| ~ sP0(X1,sK1) )
| ~ spl27_75
| ~ spl27_83
| ~ spl27_92 ),
inference(forward_demodulation,[],[f3904,f3743]) ).
fof(f3906,plain,
( ! [X0,X1] :
( sK7(sK3(sK11(sK2,sK1))) != X0
| sK7(sK3(sK11(sK2,sK1))) != X0
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| ~ sP0(X1,sK1) )
| ~ spl27_75
| ~ spl27_83
| ~ spl27_92 ),
inference(forward_demodulation,[],[f3905,f3811]) ).
fof(f3907,plain,
( ! [X0,X1] :
( ~ sP0(X1,sK1)
| ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),X1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(X1,sK1))
| sK7(sK3(sK11(sK2,sK1))) != X0 )
| ~ spl27_75
| ~ spl27_83
| ~ spl27_92 ),
inference(duplicate_literal_removal,[],[f3906]) ).
fof(f3909,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(sK2,sK1))
| subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) = X0 )
| ~ spl27_2
| ~ spl27_83
| ~ spl27_84 ),
inference(resolution,[],[f3801,f323]) ).
fof(f3910,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(sK2,sK1))
| sK7(sK3(sK11(sK2,sK1))) = X0 )
| ~ spl27_2
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(forward_demodulation,[],[f3909,f3811]) ).
fof(f4001,plain,
( ! [X0] :
( ~ in(sK3(sK11(sK2,sK1)),complements_of_subsets(the_carrier(sK1),sK2))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(sK2,sK1))
| sK7(sK3(sK11(sK2,sK1))) != X0 )
| ~ spl27_2
| ~ spl27_75
| ~ spl27_83
| ~ spl27_92 ),
inference(resolution,[],[f3907,f323]) ).
fof(f4003,definition,
( spl27_111
<=> ! [X0] :
( in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(sK2,sK1))
| sK7(sK3(sK11(sK2,sK1))) != X0 ) ),
introduced(definition,[new_symbols(definition,[spl27_111])],[avatar_definition]) ).
fof(f4004,plain,
( ! [X0] :
( sK7(sK3(sK11(sK2,sK1))) != X0
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),X0)),sK11(sK2,sK1)) )
| ~ spl27_111 ),
inference(avatar_component_clause,[],[f4003]) ).
fof(f4005,plain,
( spl27_111
| ~ spl27_91
| ~ spl27_2
| ~ spl27_75
| ~ spl27_83
| ~ spl27_92 ),
inference(avatar_split_clause,[],[f4001,f3810,f3742,f3685,f322,f3807,f4003]) ).
fof(f4006,plain,
( in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),sK7(sK3(sK11(sK2,sK1))))),sK11(sK2,sK1))
| ~ spl27_111 ),
inference(equality_resolution,[],[f4004]) ).
fof(f4012,plain,
( apply(sK11(sK2,sK1),sK3(sK11(sK2,sK1))) = sK7(sK3(sK11(sK2,sK1)))
| ~ spl27_2
| ~ spl27_111 ),
inference(resolution,[],[f4006,f1211]) ).
fof(f4642,definition,
( spl27_119
<=> ! [X0] :
( element(sK5(sK13(sK1,sK2),X0),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl27_119])],[avatar_definition]) ).
fof(f4643,plain,
( ! [X0] :
( element(sK5(sK13(sK1,sK2),X0),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = X0 )
| ~ spl27_119 ),
inference(avatar_component_clause,[],[f4642]) ).
fof(f5384,definition,
( spl27_132
<=> ! [X0] : sK13(sK1,sK2) = X0 ),
introduced(definition,[new_symbols(definition,[spl27_132])],[avatar_definition]) ).
fof(f5385,plain,
( ! [X0] : sK13(sK1,sK2) = X0
| ~ spl27_132 ),
inference(avatar_component_clause,[],[f5384]) ).
fof(f8213,plain,
( ! [X0] :
( ~ in(X0,relation_dom(sK11(sK2,sK1)))
| in(unordered_pair(singleton(X0),unordered_pair(X0,sK18(sK11(sK2,sK1),X0))),sK11(sK2,sK1)) )
| ~ spl27_2 ),
inference(resolution,[],[f316,f323]) ).
fof(f8214,plain,
( ! [X0] :
( ~ in(X0,complements_of_subsets(the_carrier(sK1),sK2))
| in(unordered_pair(singleton(X0),unordered_pair(X0,sK18(sK11(sK2,sK1),X0))),sK11(sK2,sK1)) )
| ~ spl27_2
| ~ spl27_18 ),
inference(forward_demodulation,[],[f8213,f3695]) ).
fof(f8661,plain,
( ! [X0] :
( ~ function(X0)
| in(unordered_pair(singleton(sK3(X0)),unordered_pair(sK3(X0),sK18(sK11(sK2,sK1),sK3(X0)))),sK11(sK2,sK1))
| relation_dom(X0) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ relation(X0) )
| ~ spl27_2
| ~ spl27_18 ),
inference(resolution,[],[f8214,f144]) ).
fof(f9096,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(sK3(sK11(X0,X1))),unordered_pair(sK3(sK11(X0,X1)),sK18(sK11(sK2,sK1),sK3(sK11(X0,X1))))),sK11(sK2,sK1))
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(X0,X1))
| ~ relation(sK11(X0,X1))
| ~ sP0(X0,X1) )
| ~ spl27_2
| ~ spl27_18 ),
inference(resolution,[],[f8661,f209]) ).
fof(f9098,plain,
( ! [X0,X1] :
( ~ sP0(X0,X1)
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(X0,X1))
| in(unordered_pair(singleton(sK3(sK11(X0,X1))),unordered_pair(sK3(sK11(X0,X1)),sK18(sK11(sK2,sK1),sK3(sK11(X0,X1))))),sK11(sK2,sK1)) )
| ~ spl27_2
| ~ spl27_18 ),
inference(forward_subsumption_resolution,[],[f9096,f210]) ).
fof(f9315,plain,
( complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),sK18(sK11(sK2,sK1),sK3(sK11(sK2,sK1))))),sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18 ),
inference(resolution,[],[f9098,f323]) ).
fof(f9316,plain,
( in(unordered_pair(singleton(sK3(sK11(sK2,sK1))),unordered_pair(sK3(sK11(sK2,sK1)),sK18(sK11(sK2,sK1),sK3(sK11(sK2,sK1))))),sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18 ),
inference(forward_subsumption_resolution,[],[f9315,f3695]) ).
fof(f9317,plain,
( sK7(sK3(sK11(sK2,sK1))) = sK18(sK11(sK2,sK1),sK3(sK11(sK2,sK1)))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(resolution,[],[f9316,f3910]) ).
fof(f9318,plain,
( apply(sK11(sK2,sK1),sK3(sK11(sK2,sK1))) = sK18(sK11(sK2,sK1),sK3(sK11(sK2,sK1)))
| ~ spl27_2
| ~ spl27_18 ),
inference(resolution,[],[f9316,f1211]) ).
fof(f9323,plain,
( empty_set = sK18(sK11(sK2,sK1),sK3(sK11(sK2,sK1)))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_74 ),
inference(forward_demodulation,[],[f9318,f3683]) ).
fof(f9360,plain,
( empty_set = sK7(sK3(sK11(sK2,sK1)))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(superposition,[],[f9323,f9317]) ).
fof(f9372,plain,
( empty_set != subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_18
| ~ spl27_74 ),
inference(forward_subsumption_resolution,[],[f3798,f3695]) ).
fof(f9378,plain,
( empty_set != subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83 ),
inference(forward_demodulation,[],[f9372,f3743]) ).
fof(f9384,plain,
( empty_set != sK7(sK3(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83
| ~ spl27_92 ),
inference(forward_demodulation,[],[f9378,f3811]) ).
fof(f9390,plain,
( ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(forward_subsumption_resolution,[],[f9384,f9360]) ).
fof(f9396,plain,
( ~ spl27_8
| ~ spl27_7
| ~ spl27_2
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(avatar_split_clause,[],[f9390,f3810,f3746,f3742,f3682,f599,f322,f411,f414]) ).
fof(f10079,plain,
( subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != sK7(sK3(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| complements_of_subsets(the_carrier(sK1),sK2) != relation_dom(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_111 ),
inference(superposition,[],[f147,f4012]) ).
fof(f10080,plain,
( subset_complement(the_carrier(sK1),sK4(sK11(sK2,sK1))) != sK7(sK3(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_111 ),
inference(forward_subsumption_resolution,[],[f10079,f3695]) ).
fof(f10081,plain,
( subset_complement(the_carrier(sK1),sK3(sK11(sK2,sK1))) != sK7(sK3(sK11(sK2,sK1)))
| ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_83
| ~ spl27_111 ),
inference(forward_demodulation,[],[f10080,f3743]) ).
fof(f10082,plain,
( ~ function(sK11(sK2,sK1))
| ~ relation(sK11(sK2,sK1))
| ~ spl27_2
| ~ spl27_18
| ~ spl27_83
| ~ spl27_92
| ~ spl27_111 ),
inference(forward_subsumption_resolution,[],[f10081,f3811]) ).
fof(f10083,plain,
( ~ spl27_8
| ~ spl27_7
| ~ spl27_2
| ~ spl27_18
| ~ spl27_83
| ~ spl27_92
| ~ spl27_111 ),
inference(avatar_split_clause,[],[f10082,f4003,f3810,f3742,f599,f322,f411,f414]) ).
fof(f10157,plain,
( sK15(sK1,sK2) = sK14(sK1,sK2)
| ~ spl27_34
| ~ spl27_35 ),
inference(forward_demodulation,[],[f1199,f1195]) ).
fof(f10228,plain,
( sK14(sK1,sK2) != sK14(sK1,sK2)
| sP0(sK2,sK1)
| ~ one_sorted_str(sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_34
| ~ spl27_35 ),
inference(superposition,[],[f215,f10157]) ).
fof(f10229,plain,
( sP0(sK2,sK1)
| ~ one_sorted_str(sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_34
| ~ spl27_35 ),
inference(trivial_inequality_removal,[],[f10228]) ).
fof(f10230,plain,
( sP0(sK2,sK1)
| ~ element(sK2,powerset(powerset(the_carrier(sK1))))
| ~ spl27_34
| ~ spl27_35 ),
inference(forward_subsumption_resolution,[],[f10229,f133]) ).
fof(f10231,plain,
( sP0(sK2,sK1)
| ~ spl27_34
| ~ spl27_35 ),
inference(forward_subsumption_resolution,[],[f10230,f132]) ).
fof(f10232,plain,
( spl27_2
| ~ spl27_34
| ~ spl27_35 ),
inference(avatar_split_clause,[],[f10231,f1198,f1194,f322]) ).
fof(f10494,plain,
( spl27_61
| spl27_11
| ~ spl27_1
| ~ spl27_60 ),
inference(avatar_split_clause,[],[f2854,f2767,f319,f459,f2825]) ).
fof(f10495,plain,
( spl27_119
| spl27_11
| ~ spl27_1
| ~ spl27_60 ),
inference(avatar_split_clause,[],[f2853,f2767,f319,f459,f4642]) ).
fof(f11768,plain,
( ! [X0] :
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| sK6(sK13(sK1,sK2),sK13(sK1,sK2)) = X0
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),X0) )
| ~ spl27_1
| ~ spl27_59 ),
inference(superposition,[],[f1174,f2765]) ).
fof(f11830,plain,
( spl27_64
| spl27_11
| ~ spl27_1
| ~ spl27_59 ),
inference(avatar_split_clause,[],[f11768,f2764,f319,f459,f2843]) ).
fof(f11924,plain,
( ! [X0] :
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = X0
| sK13(sK1,sK2) = X0 )
| ~ spl27_61
| ~ spl27_119 ),
inference(superposition,[],[f4643,f2826]) ).
fof(f11931,plain,
( ! [X0] :
( element(sK13(sK1,sK2),powerset(the_carrier(sK1)))
| sK13(sK1,sK2) = X0 )
| ~ spl27_61
| ~ spl27_119 ),
inference(duplicate_literal_removal,[],[f11924]) ).
fof(f11933,plain,
( spl27_132
| spl27_11
| ~ spl27_61
| ~ spl27_119 ),
inference(avatar_split_clause,[],[f11931,f4642,f2825,f459,f5384]) ).
fof(f16187,plain,
( ! [X0,X1] : X0 = X1
| ~ spl27_132 ),
inference(superposition,[],[f5385,f5385]) ).
fof(f16411,plain,
( ! [X0] :
( subset_complement(the_carrier(sK1),sK4(X0)) != sK13(sK1,sK2)
| ~ function(X0)
| relation_dom(X0) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ relation(X0) )
| ~ spl27_132 ),
inference(superposition,[],[f147,f5385]) ).
fof(f16619,plain,
( ! [X0] :
( ~ function(X0)
| relation_dom(X0) != complements_of_subsets(the_carrier(sK1),sK2)
| ~ relation(X0) )
| ~ spl27_132 ),
inference(forward_subsumption_resolution,[],[f16411,f5385]) ).
fof(f16799,plain,
( ! [X0] :
( ~ function(X0)
| ~ relation(X0) )
| ~ spl27_132 ),
inference(forward_subsumption_resolution,[],[f16619,f16187]) ).
fof(f18543,plain,
( sK13(sK1,sK2) != sK13(sK1,sK2)
| sK13(sK1,sK2) = sK6(sK13(sK1,sK2),sK13(sK1,sK2))
| ~ spl27_64 ),
inference(equality_factoring,[],[f2844]) ).
fof(f18544,plain,
( sK13(sK1,sK2) = sK6(sK13(sK1,sK2),sK13(sK1,sK2))
| ~ spl27_64 ),
inference(trivial_inequality_removal,[],[f18543]) ).
fof(f18652,plain,
( ~ relation(sK20)
| ~ spl27_132 ),
inference(resolution,[],[f16799,f241]) ).
fof(f18653,plain,
( $false
| ~ spl27_132 ),
inference(forward_subsumption_resolution,[],[f18652,f242]) ).
fof(f18654,plain,
~ spl27_132,
inference(avatar_contradiction_clause,[],[f18653]) ).
fof(f18662,plain,
( spl27_60
| ~ spl27_64 ),
inference(avatar_split_clause,[],[f18544,f2843,f2767]) ).
cnf(s1,plain,
( spl27_1
| spl27_2 ),
inference(sat_conversion,[],[f324]) ).
cnf(s4,plain,
( ~ spl27_2
| ~ spl27_7
| ~ spl27_8
| spl27_9 ),
inference(sat_conversion,[],[f419]) ).
cnf(s6,plain,
( ~ spl27_2
| spl27_7 ),
inference(sat_conversion,[],[f424]) ).
cnf(s9,plain,
( ~ spl27_2
| spl27_8 ),
inference(sat_conversion,[],[f470]) ).
cnf(s21,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_11
| spl27_34 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s22,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_11
| spl27_35 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s44,plain,
( ~ spl27_1
| spl27_59
| spl27_60 ),
inference(sat_conversion,[],[f2769]) ).
cnf(s58,plain,
( ~ spl27_2
| spl27_18 ),
inference(sat_conversion,[],[f3679]) ).
cnf(s59,plain,
( ~ spl27_2
| ~ spl27_7
| ~ spl27_8
| ~ spl27_9
| ~ spl27_18
| spl27_74
| spl27_75 ),
inference(sat_conversion,[],[f3687]) ).
cnf(s68,plain,
( ~ spl27_7
| ~ spl27_8
| ~ spl27_18
| spl27_83 ),
inference(sat_conversion,[],[f3744]) ).
cnf(s69,plain,
( ~ spl27_7
| ~ spl27_8
| ~ spl27_18
| spl27_84 ),
inference(sat_conversion,[],[f3748]) ).
cnf(s77,plain,
( ~ spl27_83
| ~ spl27_84
| ~ spl27_91
| spl27_92 ),
inference(sat_conversion,[],[f3812]) ).
cnf(s78,plain,
( ~ spl27_7
| ~ spl27_8
| ~ spl27_18
| spl27_91 ),
inference(sat_conversion,[],[f3816]) ).
cnf(s99,plain,
( ~ spl27_2
| ~ spl27_75
| ~ spl27_83
| ~ spl27_91
| ~ spl27_92
| spl27_111 ),
inference(sat_conversion,[],[f4005]) ).
cnf(s226,plain,
( ~ spl27_2
| ~ spl27_7
| ~ spl27_8
| ~ spl27_18
| ~ spl27_74
| ~ spl27_83
| ~ spl27_84
| ~ spl27_92 ),
inference(sat_conversion,[],[f9396]) ).
cnf(s293,plain,
( ~ spl27_2
| ~ spl27_7
| ~ spl27_8
| ~ spl27_18
| ~ spl27_83
| ~ spl27_92
| ~ spl27_111 ),
inference(sat_conversion,[],[f10083]) ).
cnf(s313,plain,
( spl27_2
| ~ spl27_34
| ~ spl27_35 ),
inference(sat_conversion,[],[f10232]) ).
cnf(s412,plain,
( ~ spl27_1
| spl27_11
| ~ spl27_60
| spl27_61 ),
inference(sat_conversion,[],[f10494]) ).
cnf(s413,plain,
( ~ spl27_1
| spl27_11
| ~ spl27_60
| spl27_119 ),
inference(sat_conversion,[],[f10495]) ).
cnf(s754,plain,
( ~ spl27_1
| spl27_11
| ~ spl27_59
| spl27_64 ),
inference(sat_conversion,[],[f11830]) ).
cnf(s768,plain,
( spl27_11
| ~ spl27_61
| ~ spl27_119
| spl27_132 ),
inference(sat_conversion,[],[f11933]) ).
cnf(s1598,plain,
~ spl27_132,
inference(sat_conversion,[],[f18654]) ).
cnf(s1599,plain,
( spl27_60
| ~ spl27_64 ),
inference(sat_conversion,[],[f18662]) ).
cnf(s1610,plain,
( spl27_11
| ~ spl27_61
| ~ spl27_119 ),
inference(rat,[],[s768,s1598]) ).
cnf(s1612,plain,
~ spl27_2,
inference(rat,[],[s59,s99,s226,s293,s77,s4,s68,s69,s78,s6,s9,s58]) ).
cnf(s1613,plain,
spl27_1,
inference(rat,[],[s1,s1612]) ).
cnf(s1614,plain,
~ spl27_11,
inference(rat,[],[s313,s21,s22,s1612,s1613]) ).
cnf(s1651,plain,
~ spl27_60,
inference(rat,[],[s1610,s412,s413,s1614,s1613]) ).
cnf(s1652,plain,
~ spl27_64,
inference(rat,[],[s1599,s1651]) ).
cnf(s1654,plain,
spl27_59,
inference(rat,[],[s44,s1613,s1651]) ).
cnf(s1655,plain,
$false,
inference(rat,[],[s754,s1614,s1613,s1652,s1654]) ).
fof(f18936,plain,
$false,
inference(avatar_sat_refutation,[],[s1655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU331+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 04:44:39 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 5.42/2.15 % (1882892)Detected formulas, will run a generic FOF schedule.
% 5.42/2.15 % (1882898)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=1217090167:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.42/2.15 % (1882900)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2164631382:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.42/2.15 % (1882902)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1435435817:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.42/2.15 % (1882897)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=3265306944:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.42/2.15 % (1882899)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=3282295064:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.42/2.15 % (1882903)dis-21_1_sil=8000:lcm=predicate:random_seed=1491257129:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.42/2.15 % (1882901)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2389119388:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.42/2.15 % (1882900)Instruction limit reached!
% 5.42/2.15 % (1882900)------------------------------
% 5.42/2.15 % (1882900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882900)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882900)Termination reason: Instruction limit
% 5.42/2.15 % (1882900)Termination phase: Saturation
% 5.42/2.15 % (1882900)Time elapsed: 0.063 s
% 5.42/2.15 % (1882900)Peak memory usage: 89 MB
% 5.42/2.15 % (1882900)Instructions burned: 109 (million)
% 5.42/2.15 % (1882901)Instruction limit reached!
% 5.42/2.15 % (1882901)------------------------------
% 5.42/2.15 % (1882901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882901)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882901)Termination reason: Instruction limit
% 5.42/2.15 % (1882901)Termination phase: Saturation
% 5.42/2.15 % (1882901)Time elapsed: 0.071 s
% 5.42/2.15 % (1882901)Peak memory usage: 88 MB
% 5.42/2.15 % (1882901)Instructions burned: 119 (million)
% 5.42/2.15 % (1882903)Instruction limit reached!
% 5.42/2.15 % (1882903)------------------------------
% 5.42/2.15 % (1882903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882903)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882903)Termination reason: Instruction limit
% 5.42/2.15 % (1882903)Termination phase: Saturation
% 5.42/2.15 % (1882903)Time elapsed: 0.080 s
% 5.42/2.15 % (1882903)Peak memory usage: 89 MB
% 5.42/2.15 % (1882903)Instructions burned: 130 (million)
% 5.42/2.15 % (1882902)Instruction limit reached!
% 5.42/2.15 % (1882902)------------------------------
% 5.42/2.15 % (1882902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882902)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882902)Termination reason: Instruction limit
% 5.42/2.15 % (1882902)Termination phase: Saturation
% 5.42/2.15 % (1882902)Time elapsed: 0.090 s
% 5.42/2.15 % (1882902)Peak memory usage: 90 MB
% 5.42/2.15 % (1882902)Instructions burned: 140 (million)
% 5.42/2.15 % (1882912)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1268898201:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.42/2.15 % (1882911)lrs+10_1_sil=8000:sp=occurrence:random_seed=3907639394:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.42/2.15 % (1882913)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3792325100:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.42/2.15 % (1882914)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=1230176727:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.42/2.15 % (1882912)Instruction limit reached!
% 5.42/2.15 % (1882912)------------------------------
% 5.42/2.15 % (1882912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882912)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882912)Termination reason: Instruction limit
% 5.42/2.15 % (1882912)Termination phase: Saturation
% 5.42/2.15 % (1882912)Time elapsed: 0.095 s
% 5.42/2.15 % (1882912)Peak memory usage: 90 MB
% 5.42/2.15 % (1882912)Instructions burned: 158 (million)
% 5.42/2.15 % (1882911)Instruction limit reached!
% 5.42/2.15 % (1882911)------------------------------
% 5.42/2.15 % (1882911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882911)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882911)Termination reason: Instruction limit
% 5.42/2.15 % (1882911)Termination phase: Saturation
% 5.42/2.15 % (1882911)Time elapsed: 0.165 s
% 5.42/2.15 % (1882911)Peak memory usage: 90 MB
% 5.42/2.15 % (1882911)Instructions burned: 286 (million)
% 5.42/2.15 % (1882914)Instruction limit reached!
% 5.42/2.15 % (1882914)------------------------------
% 5.42/2.15 % (1882914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882914)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882914)Termination reason: Instruction limit
% 5.42/2.15 % (1882914)Termination phase: Saturation
% 5.42/2.15 % (1882914)Time elapsed: 0.149 s
% 5.42/2.15 % (1882914)Peak memory usage: 90 MB
% 5.42/2.15 % (1882914)Instructions burned: 248 (million)
% 5.42/2.15 % (1882913)Instruction limit reached!
% 5.42/2.15 % (1882913)------------------------------
% 5.42/2.15 % (1882913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882913)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882913)Termination reason: Instruction limit
% 5.42/2.15 % (1882913)Termination phase: Saturation
% 5.42/2.15 % (1882913)Time elapsed: 0.203 s
% 5.42/2.15 % (1882913)Peak memory usage: 92 MB
% 5.42/2.15 % (1882913)Instructions burned: 326 (million)
% 5.42/2.15 % (1882919)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=399865398:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.42/2.15 % (1882920)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1540235707:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.42/2.15 % (1882921)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=472101372:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.42/2.15 % (1882922)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2103696900:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.42/2.15 % (1882919)Instruction limit reached!
% 5.42/2.15 % (1882919)------------------------------
% 5.42/2.15 % (1882919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882919)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882919)Termination reason: Instruction limit
% 5.42/2.15 % (1882919)Termination phase: Saturation
% 5.42/2.15 % (1882919)Time elapsed: 0.155 s
% 5.42/2.15 % (1882919)Peak memory usage: 89 MB
% 5.42/2.15 % (1882919)Instructions burned: 294 (million)
% 5.42/2.15 % (1882921)Instruction limit reached!
% 5.42/2.15 % (1882921)------------------------------
% 5.42/2.15 % (1882921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882921)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882921)Termination reason: Instruction limit
% 5.42/2.15 % (1882921)Termination phase: Saturation
% 5.42/2.15 % (1882921)Time elapsed: 0.078 s
% 5.42/2.15 % (1882921)Peak memory usage: 90 MB
% 5.42/2.15 % (1882921)Instructions burned: 114 (million)
% 5.42/2.15 % (1882922)Instruction limit reached!
% 5.42/2.15 % (1882922)------------------------------
% 5.42/2.15 % (1882922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882922)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882922)Termination reason: Instruction limit
% 5.42/2.15 % (1882922)Termination phase: Saturation
% 5.42/2.15 % (1882922)Time elapsed: 0.062 s
% 5.42/2.15 % (1882922)Peak memory usage: 88 MB
% 5.42/2.15 % (1882922)Instructions burned: 129 (million)
% 5.42/2.15 % (1882927)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1027608615:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 5.42/2.15 % (1882928)lrs+10_1_sil=8000:sp=occurrence:random_seed=3551527588:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 5.42/2.15 % (1882929)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1514687826:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 5.42/2.15 % (1882927)Instruction limit reached!
% 5.42/2.15 % (1882927)------------------------------
% 5.42/2.15 % (1882927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882927)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882927)Termination reason: Instruction limit
% 5.42/2.15 % (1882927)Termination phase: Saturation
% 5.42/2.15 % (1882927)Time elapsed: 0.059 s
% 5.42/2.15 % (1882927)Peak memory usage: 89 MB
% 5.42/2.15 % (1882927)Instructions burned: 114 (million)
% 5.42/2.15 % (1882898)First to succeed.
% 5.42/2.15 % (1882898)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1882892"
% 5.42/2.15 % (1882933)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=613382064:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 5.42/2.15 % (1882929)Instruction limit reached!
% 5.42/2.15 % (1882929)------------------------------
% 5.42/2.15 % (1882929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/2.15 % (1882929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/2.15 % (1882929)CaDiCaL version: 2.1.3
% 5.42/2.15 % (1882929)Termination reason: Instruction limit
% 5.42/2.15 % (1882929)Termination phase: Saturation
% 5.42/2.15 % (1882929)Time elapsed: 0.247 s
% 5.42/2.15 % (1882929)Peak memory usage: 90 MB
% 5.42/2.15 % (1882929)Instructions burned: 438 (million)
% 5.42/2.15 % (1882898)Refutation found. Thanks to Tanya!
% 5.42/2.15 % SZS status Theorem for theBenchmark
% 5.42/2.15 % SZS output start Proof for theBenchmark
% See solution above
% 9.68/2.35 % (1882898)------------------------------
% 9.68/2.35 % (1882898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.35 % (1882898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.35 % (1882898)CaDiCaL version: 2.1.3
% 9.68/2.35 % (1882898)Termination reason: Refutation
% 9.68/2.35 % (1882898)Time elapsed: 1.0000 s
% 9.68/2.35 % (1882898)Peak memory usage: 141 MB
% 9.68/2.35 % (1882898)Instructions burned: 2988 (million)
% 9.68/2.35 % (1882898)------------------------------
% 9.68/2.35 % (1882898)------------------------------
% 9.68/2.35 % (1882892)Success in time 1.285 s
% 9.68/2.35 % Vampire exiting
%------------------------------------------------------------------------------