%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU332+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:52:54 PM UTC 2026
% Result : Theorem 1.51s 0.76s
% Output : Refutation 1.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 26
% Syntax : Number of formulae : 285 ( 10 unt; 22 def)
% Number of atoms : 1068 ( 191 equ)
% Maximal formula atoms : 23 ( 3 avg)
% Number of connectives : 1344 ( 561 ~; 661 |; 66 &)
% ( 28 <=>; 26 =>; 0 <=; 2 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 23 prp; 0-4 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-4 aty)
% Number of variables : 361 ( 0 sgn 305 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ! [X2] :
? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X1,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X1)
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X5
=> X6 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e4_7_2__tops_2__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ! [X2] :
? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X1,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X1)
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X5
=> X6 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f22,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,subset_complement(X0,X1)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f26,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> element(subset_complement(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f33,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ! [X2] :
( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X1)
& ! [X8] :
( element(X8,powerset(the_carrier(X0)))
=> ( X8 = X6
=> X7 = subset_complement(the_carrier(X0),X8) ) ) )
& X3 = X5
& ? [X9,X10] :
( ordered_pair(X9,X10) = X5
& in(X9,X1)
& ! [X11] :
( element(X11,powerset(the_carrier(X0)))
=> ( X11 = X9
=> X10 = subset_complement(the_carrier(X0),X11) ) ) ) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,cartesian_product2(X1,X2))
& X5 = X4
& ? [X12,X13] :
( ordered_pair(X12,X13) = X4
& in(X12,X1)
& ! [X14] :
( element(X14,powerset(the_carrier(X0)))
=> ( X14 = X12
=> X13 = subset_complement(the_carrier(X0),X14) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_tarski__e4_7_2__tops_2__2) ).
fof(f34,plain,
! [X0,X1] :
( ( one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) )
=> ! [X2] :
( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X1)
& ! [X8] :
( element(X8,powerset(the_carrier(X0)))
=> ( X8 = X6
=> X7 = subset_complement(the_carrier(X0),X8) ) ) )
& X3 = X5
& ? [X9,X10] :
( ordered_pair(X9,X10) = X5
& in(X9,X1)
& ! [X11] :
( element(X11,powerset(the_carrier(X0)))
=> ( X11 = X9
=> X10 = subset_complement(the_carrier(X0),X11) ) ) ) )
=> X4 = X5 )
=> ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,cartesian_product2(X1,X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,X1)
& ! [X17] :
( element(X17,powerset(the_carrier(X0)))
=> ( X15 = X17
=> subset_complement(the_carrier(X0),X17) = X16 ) ) ) ) ) ) ),
inference(rectify,[],[f33]) ).
fof(f51,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X1,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X1)
& ! [X7] :
( X6 = subset_complement(the_carrier(X0),X7)
| X5 != X7
| ~ element(X7,powerset(the_carrier(X0))) ) ) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f2]) ).
fof(f52,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X1,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X1)
& ! [X7] :
( X6 = subset_complement(the_carrier(X0),X7)
| X5 != X7
| ~ element(X7,powerset(the_carrier(X0))) ) ) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f51]) ).
fof(f66,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f22]) ).
fof(f68,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f26]) ).
fof(f69,plain,
! [X0,X1] :
( ! [X2] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,cartesian_product2(X1,X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,X1)
& ! [X17] :
( subset_complement(the_carrier(X0),X17) = X16
| X15 != X17
| ~ element(X17,powerset(the_carrier(X0))) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X1)
& ! [X8] :
( X7 = subset_complement(the_carrier(X0),X8)
| X6 != X8
| ~ element(X8,powerset(the_carrier(X0))) ) )
& X3 = X5
& ? [X9,X10] :
( ordered_pair(X9,X10) = X5
& in(X9,X1)
& ! [X11] :
( X10 = subset_complement(the_carrier(X0),X11)
| X9 != X11
| ~ element(X11,powerset(the_carrier(X0))) ) ) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(ennf_transformation,[],[f34]) ).
fof(f70,plain,
! [X0,X1] :
( ! [X2] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,cartesian_product2(X1,X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,X1)
& ! [X17] :
( subset_complement(the_carrier(X0),X17) = X16
| X15 != X17
| ~ element(X17,powerset(the_carrier(X0))) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X1)
& ! [X8] :
( X7 = subset_complement(the_carrier(X0),X8)
| X6 != X8
| ~ element(X8,powerset(the_carrier(X0))) ) )
& X3 = X5
& ? [X9,X10] :
( ordered_pair(X9,X10) = X5
& in(X9,X1)
& ! [X11] :
( X10 = subset_complement(the_carrier(X0),X11)
| X9 != X11
| ~ element(X11,powerset(the_carrier(X0))) ) ) ) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK3(X3)
| ~ in(X5,sK1)
| element(sK6(X5,X6),powerset(the_carrier(sK0)))
| ~ in(sK3(X3),cartesian_product2(sK1,sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f72,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK3(X3)
| ~ in(X5,sK1)
| sK6(X5,X6) = X5
| ~ in(sK3(X3),cartesian_product2(sK1,sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f73,plain,
! [X3,X6,X5] :
( subset_complement(the_carrier(sK0),sK6(X5,X6)) != X6
| ~ in(X5,sK1)
| ordered_pair(X5,X6) != sK3(X3)
| ~ in(sK3(X3),cartesian_product2(sK1,sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f74,plain,
! [X3,X7] :
( ~ element(X7,powerset(the_carrier(sK0)))
| sK4(X3) != X7
| sK5(X3) = subset_complement(the_carrier(sK0),X7)
| in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f75,plain,
! [X3] :
( in(sK4(X3),sK1)
| in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f76,plain,
! [X3] :
( in(sK3(X3),X3)
| sK3(X3) = ordered_pair(sK4(X3),sK5(X3)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f77,plain,
! [X3] :
( in(sK3(X3),cartesian_product2(sK1,sK2))
| in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f52]) ).
fof(f78,plain,
element(sK1,powerset(powerset(the_carrier(sK0)))),
inference(cnf_transformation,[],[f52]) ).
fof(f79,plain,
one_sorted_str(sK0),
inference(cnf_transformation,[],[f52]) ).
fof(f115,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,subset_complement(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f117,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f68]) ).
fof(f119,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f120,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( sK22(X0,X15,X16) = X15
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f121,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f122,plain,
! [X2,X0,X1,X17,X13] :
( ~ element(X17,powerset(the_carrier(X0)))
| sK20(X0,X1,X13) != X17
| subset_complement(the_carrier(X0),X17) = sK21(X0,X1,X13)
| ~ sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f123,plain,
! [X2,X0,X1,X13] :
( ~ sP18(X13,X2,X1,X0)
| in(sK20(X0,X1,X13),X1) ),
inference(cnf_transformation,[],[f70]) ).
fof(f124,plain,
! [X2,X0,X1,X13] :
( ~ sP18(X13,X2,X1,X0)
| ordered_pair(sK20(X0,X1,X13),sK21(X0,X1,X13)) = X13 ),
inference(cnf_transformation,[],[f70]) ).
fof(f125,plain,
! [X2,X0,X1,X13] :
( ~ sP18(X13,X2,X1,X0)
| sK19(X0,X1,X2,X13) = X13 ),
inference(cnf_transformation,[],[f70]) ).
fof(f126,plain,
! [X2,X0,X1,X13] :
( in(sK19(X0,X1,X2,X13),cartesian_product2(X1,X2))
| ~ sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f139,plain,
! [X2,X0,X1,X13] :
( sK11(X0,X1) != sK12(X0,X1)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ sP18(X13,X2,X1,X0)
| in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f140,plain,
! [X2,X0,X1,X13] :
( sK11(X0,X1) != sK12(X0,X1)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sP18(X13,X2,X1,X0)
| ~ in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f141,plain,
! [X2,X0,X1,X13] :
( ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sK10(X0,X1) = sK11(X0,X1)
| ~ sP18(X13,X2,X1,X0)
| in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f142,plain,
! [X2,X0,X1,X13] :
( ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sK10(X0,X1) = sK11(X0,X1)
| sP18(X13,X2,X1,X0)
| ~ in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f143,plain,
! [X2,X0,X1,X13] :
( ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sK10(X0,X1) = sK12(X0,X1)
| ~ sP18(X13,X2,X1,X0)
| in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f144,plain,
! [X2,X0,X1,X13] :
( ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| sK10(X0,X1) = sK12(X0,X1)
| sP18(X13,X2,X1,X0)
| ~ in(X13,sK13(X0,X1,X2)) ),
inference(cnf_transformation,[],[f70]) ).
fof(f145,plain,
! [X3] :
( ~ element(sK4(X3),powerset(the_carrier(sK0)))
| sK5(X3) = subset_complement(the_carrier(sK0),sK4(X3))
| in(sK3(X3),X3) ),
inference(equality_resolution,[],[f74]) ).
fof(f150,plain,
! [X2,X0,X1,X13] :
( ~ element(sK20(X0,X1,X13),powerset(the_carrier(X0)))
| sK21(X0,X1,X13) = subset_complement(the_carrier(X0),sK20(X0,X1,X13))
| ~ sP18(X13,X2,X1,X0) ),
inference(equality_resolution,[],[f122]) ).
fof(f151,plain,
! [X2,X0,X1,X16,X14,X15] :
( subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f121]) ).
fof(f152,plain,
! [X2,X0,X1,X16,X15] :
( subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| ~ in(X15,X1)
| ~ in(ordered_pair(X15,X16),cartesian_product2(X1,X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f151]) ).
fof(f153,plain,
! [X2,X0,X1,X16,X14,X15] :
( sK22(X0,X15,X16) = X15
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f120]) ).
fof(f154,plain,
! [X2,X0,X1,X16,X15] :
( ~ in(ordered_pair(X15,X16),cartesian_product2(X1,X2))
| ~ in(X15,X1)
| sK22(X0,X15,X16) = X15
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f153]) ).
fof(f155,plain,
! [X2,X0,X1,X16,X14,X15] :
( element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| ~ in(X15,X1)
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(X1,X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f156,plain,
! [X2,X0,X1,X16,X15] :
( ~ in(ordered_pair(X15,X16),cartesian_product2(X1,X2))
| ~ in(X15,X1)
| element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f155]) ).
fof(f164,plain,
sK1 = subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),
inference(resolution,[],[f115,f78]) ).
fof(f316,definition,
( spl23_6
<=> ! [X0,X1] :
( sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition]) ).
fof(f317,plain,
( ! [X0,X1] :
( ~ in(X0,sK13(sK0,sK1,X1))
| sP18(X0,X1,sK1,sK0) )
| ~ spl23_6 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f651,definition,
( spl23_56
<=> ! [X0,X1] :
( ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_56])],[avatar_definition]) ).
fof(f652,plain,
( ! [X0,X1] :
( ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_56 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f933,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| sK10(sK0,X0) = sK11(sK0,X0)
| ~ sP18(X1,X2,X0,sK0)
| in(X1,sK13(sK0,X0,X2)) ),
inference(resolution,[],[f141,f79]) ).
fof(f934,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X1,X2,subset_complement(powerset(the_carrier(sK0)),X0),sK0)
| in(X1,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),X0),X2))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) ),
inference(resolution,[],[f933,f117]) ).
fof(f944,definition,
( spl23_67
<=> sK10(sK0,sK1) = sK11(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl23_67])],[avatar_definition]) ).
fof(f946,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ spl23_67 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f960,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| sK10(sK0,X0) = sK11(sK0,X0)
| sP18(X1,X2,X0,sK0)
| ~ in(X1,sK13(sK0,X0,X2)) ),
inference(resolution,[],[f142,f79]) ).
fof(f966,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| sP18(X1,X2,subset_complement(powerset(the_carrier(sK0)),X0),sK0)
| ~ in(X1,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),X0),X2))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) ),
inference(resolution,[],[f960,f117]) ).
fof(f974,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(powerset(the_carrier(sK0))))
| in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),sK0) ),
inference(resolution,[],[f934,f117]) ).
fof(f1004,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(powerset(the_carrier(sK0))))
| ~ in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)))
| sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),sK0) ),
inference(resolution,[],[f966,f117]) ).
fof(f1213,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| sK10(sK0,X0) = sK12(sK0,X0)
| ~ sP18(X1,X2,X0,sK0)
| in(X1,sK13(sK0,X0,X2)) ),
inference(resolution,[],[f143,f79]) ).
fof(f1214,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X1,X2,subset_complement(powerset(the_carrier(sK0)),X0),sK0)
| in(X1,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),X0),X2))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) = sK12(sK0,subset_complement(powerset(the_carrier(sK0)),X0)) ),
inference(resolution,[],[f1213,f117]) ).
fof(f1220,definition,
( spl23_79
<=> sK11(sK0,sK1) = sK12(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl23_79])],[avatar_definition]) ).
fof(f1222,plain,
( sK11(sK0,sK1) = sK12(sK0,sK1)
| ~ spl23_79 ),
inference(avatar_component_clause,[],[f1220]) ).
fof(f1230,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(powerset(the_carrier(sK0))))
| in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2))) = sK12(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),X2)),sK0) ),
inference(resolution,[],[f1214,f117]) ).
fof(f1236,plain,
! [X0,X1] :
( in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(resolution,[],[f974,f78]) ).
fof(f1244,plain,
! [X0,X1] :
( in(X0,sK13(sK0,sK1,X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1236,f164]) ).
fof(f1245,plain,
! [X0,X1] :
( sK10(sK0,sK1) = sK11(sK0,sK1)
| in(X0,sK13(sK0,sK1,X1))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1244,f164]) ).
fof(f1250,plain,
! [X0,X1] :
( ~ in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(resolution,[],[f1004,f78]) ).
fof(f1254,plain,
! [X0,X1] :
( ~ in(X0,sK13(sK0,sK1,X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK11(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1250,f164]) ).
fof(f1255,plain,
! [X0,X1] :
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ in(X0,sK13(sK0,sK1,X1))
| sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1254,f164]) ).
fof(f1271,plain,
! [X0,X1] :
( in(X0,sK13(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK12(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(resolution,[],[f1230,f78]) ).
fof(f1274,plain,
! [X0,X1] :
( in(X0,sK13(sK0,sK1,X1))
| sK10(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1))) = sK12(sK0,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1271,f164]) ).
fof(f1275,plain,
! [X0,X1] :
( sK10(sK0,sK1) = sK12(sK0,sK1)
| in(X0,sK13(sK0,sK1,X1))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) ),
inference(forward_demodulation,[],[f1274,f164]) ).
fof(f1276,plain,
( ! [X0,X1] :
( sK11(sK0,sK1) = sK12(sK0,sK1)
| in(X0,sK13(sK0,sK1,X1))
| ~ sP18(X0,X1,subset_complement(powerset(the_carrier(sK0)),subset_complement(powerset(the_carrier(sK0)),sK1)),sK0) )
| ~ spl23_67 ),
inference(forward_demodulation,[],[f1275,f946]) ).
fof(f1277,plain,
( ! [X0,X1] :
( ~ sP18(X0,X1,sK1,sK0)
| sK11(sK0,sK1) = sK12(sK0,sK1)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_67 ),
inference(forward_demodulation,[],[f1276,f164]) ).
fof(f1347,definition,
( spl23_82
<=> sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_82])],[avatar_definition]) ).
fof(f1348,plain,
( sK4(sK13(sK0,sK1,sK2)) != sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_82 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1349,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| ~ spl23_82 ),
inference(avatar_component_clause,[],[f1347]) ).
fof(f1351,definition,
( spl23_83
<=> sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_83])],[avatar_definition]) ).
fof(f1352,plain,
( sK3(sK13(sK0,sK1,sK2)) != sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| spl23_83 ),
inference(avatar_component_clause,[],[f1351]) ).
fof(f1353,plain,
( sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_83 ),
inference(avatar_component_clause,[],[f1351]) ).
fof(f1363,definition,
( spl23_85
<=> element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0))) ),
introduced(definition,[new_symbols(definition,[spl23_85])],[avatar_definition]) ).
fof(f1364,plain,
( ~ element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| spl23_85 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1365,plain,
( element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| ~ spl23_85 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1371,definition,
( spl23_86
<=> sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl23_86])],[avatar_definition]) ).
fof(f1372,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_86 ),
inference(avatar_component_clause,[],[f1371]) ).
fof(f1373,plain,
( ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| spl23_86 ),
inference(avatar_component_clause,[],[f1371]) ).
fof(f1384,definition,
( spl23_88
<=> sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_88])],[avatar_definition]) ).
fof(f1385,plain,
( sK3(sK13(sK0,sK1,sK2)) != ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_88 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1386,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| ~ spl23_88 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1388,definition,
( spl23_89
<=> element(sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))),powerset(the_carrier(sK0))) ),
introduced(definition,[new_symbols(definition,[spl23_89])],[avatar_definition]) ).
fof(f1390,plain,
( element(sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))),powerset(the_carrier(sK0)))
| ~ spl23_89 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1392,plain,
( ! [X2,X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1))
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| element(sK22(X2,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),powerset(the_carrier(X2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,X2) )
| ~ spl23_88 ),
inference(superposition,[],[f156,f1386]) ).
fof(f1393,plain,
( ! [X2,X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1))
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| sK4(sK13(sK0,sK1,sK2)) = sK22(X2,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,X2) )
| ~ spl23_88 ),
inference(superposition,[],[f154,f1386]) ).
fof(f1401,definition,
( spl23_91
<=> ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),cartesian_product2(sK1,sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl23_91])],[avatar_definition]) ).
fof(f1402,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),cartesian_product2(sK1,sK2)) )
| ~ spl23_91 ),
inference(avatar_component_clause,[],[f1401]) ).
fof(f1415,plain,
( ! [X0] :
( ~ in(sK4(sK13(sK0,sK1,sK2)),sK1)
| element(sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),powerset(the_carrier(X0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) )
| ~ spl23_88 ),
inference(resolution,[],[f1392,f77]) ).
fof(f1416,plain,
( ! [X0] :
( element(sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),powerset(the_carrier(X0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) )
| ~ spl23_88 ),
inference(forward_subsumption_resolution,[],[f1415,f75]) ).
fof(f1421,definition,
( spl23_92
<=> sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl23_92])],[avatar_definition]) ).
fof(f1422,plain,
( sK3(sK13(sK0,sK1,sK2)) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| spl23_92 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1423,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_92 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1425,definition,
( spl23_93
<=> ! [X0] :
( element(sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),powerset(the_carrier(X0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_93])],[avatar_definition]) ).
fof(f1426,plain,
( ! [X0] :
( element(sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),powerset(the_carrier(X0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0) )
| ~ spl23_93 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1449,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(powerset(the_carrier(sK0))))
| sK10(sK0,X0) = sK12(sK0,X0)
| sP18(X1,X2,X0,sK0)
| ~ in(X1,sK13(sK0,X0,X2)) ),
inference(resolution,[],[f144,f79]) ).
fof(f1482,plain,
! [X0,X1] :
( sK10(sK0,sK1) = sK12(sK0,sK1)
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) ),
inference(resolution,[],[f1449,f78]) ).
fof(f1498,plain,
( ! [X0] :
( ~ in(sK4(sK13(sK0,sK1,sK2)),sK1)
| sK4(sK13(sK0,sK1,sK2)) = sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) )
| ~ spl23_88 ),
inference(resolution,[],[f1393,f77]) ).
fof(f1499,plain,
( ! [X0] :
( sK4(sK13(sK0,sK1,sK2)) = sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) )
| ~ spl23_88 ),
inference(forward_subsumption_resolution,[],[f1498,f75]) ).
fof(f1623,definition,
( spl23_99
<=> in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1) ),
introduced(definition,[new_symbols(definition,[spl23_99])],[avatar_definition]) ).
fof(f1624,plain,
( in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| ~ spl23_99 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1625,plain,
( ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| spl23_99 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1725,plain,
( ! [X0,X1] :
( sK5(sK13(sK0,sK1,sK2)) != subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2)))
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| ~ in(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),cartesian_product2(X0,X1))
| sP18(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),X1,X0,sK0) )
| ~ spl23_82 ),
inference(superposition,[],[f152,f1349]) ).
fof(f1747,definition,
( spl23_102
<=> in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl23_102])],[avatar_definition]) ).
fof(f1748,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_102 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1749,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_102 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1750,plain,
( spl23_102
| spl23_93
| ~ spl23_88 ),
inference(avatar_split_clause,[],[f1416,f1384,f1425,f1747]) ).
fof(f1752,definition,
( spl23_103
<=> sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl23_103])],[avatar_definition]) ).
fof(f1754,plain,
( sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_103 ),
inference(avatar_component_clause,[],[f1752]) ).
fof(f1758,definition,
( spl23_104
<=> sK5(sK13(sK0,sK1,sK2)) = subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_104])],[avatar_definition]) ).
fof(f1763,definition,
( spl23_105
<=> ! [X0] :
( sK4(sK13(sK0,sK1,sK2)) = sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_105])],[avatar_definition]) ).
fof(f1764,plain,
( ! [X0] :
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,X0)
| sK4(sK13(sK0,sK1,sK2)) = sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))) )
| ~ spl23_105 ),
inference(avatar_component_clause,[],[f1763]) ).
fof(f1766,plain,
( spl23_102
| spl23_105
| ~ spl23_88 ),
inference(avatar_split_clause,[],[f1499,f1384,f1763,f1747]) ).
fof(f1772,plain,
( ! [X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1))
| sK5(sK13(sK0,sK1,sK2)) != subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2)))
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| sP18(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),X1,X0,sK0) )
| ~ spl23_82
| ~ spl23_88 ),
inference(forward_demodulation,[],[f1725,f1386]) ).
fof(f1773,plain,
( ! [X0,X1] :
( sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0)
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1))
| sK5(sK13(sK0,sK1,sK2)) != subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2)))
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0) )
| ~ spl23_82
| ~ spl23_88 ),
inference(forward_demodulation,[],[f1772,f1386]) ).
fof(f1775,definition,
( spl23_107
<=> ! [X0,X1] :
( sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0)
| ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_107])],[avatar_definition]) ).
fof(f1776,plain,
( ! [X0,X1] :
( ~ in(sK4(sK13(sK0,sK1,sK2)),X0)
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0)
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(X0,X1)) )
| ~ spl23_107 ),
inference(avatar_component_clause,[],[f1775]) ).
fof(f1777,plain,
( ~ spl23_104
| spl23_107
| ~ spl23_82
| ~ spl23_88 ),
inference(avatar_split_clause,[],[f1773,f1384,f1347,f1775,f1758]) ).
fof(f1785,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_6
| ~ spl23_102 ),
inference(resolution,[],[f1749,f317]) ).
fof(f1791,plain,
( in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| ~ spl23_6
| ~ spl23_102 ),
inference(resolution,[],[f1785,f123]) ).
fof(f1845,plain,
( element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_82
| ~ spl23_93 ),
inference(superposition,[],[f1426,f1349]) ).
fof(f1848,plain,
( element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0)))
| ~ spl23_89
| ~ spl23_103 ),
inference(superposition,[],[f1390,f1754]) ).
fof(f1849,plain,
( ! [X0] :
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| sK3(X0) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_103 ),
inference(superposition,[],[f73,f1754]) ).
fof(f1850,plain,
( ! [X0] :
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| sK3(X0) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_6
| ~ spl23_102
| ~ spl23_103 ),
inference(forward_subsumption_resolution,[],[f1849,f1791]) ).
fof(f1851,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_6
| ~ spl23_92
| ~ spl23_102
| ~ spl23_103 ),
inference(forward_demodulation,[],[f1850,f1423]) ).
fof(f1853,definition,
( spl23_110
<=> sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl23_110])],[avatar_definition]) ).
fof(f1854,plain,
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_110 ),
inference(avatar_component_clause,[],[f1853]) ).
fof(f1856,plain,
( ~ spl23_110
| spl23_91
| ~ spl23_6
| ~ spl23_92
| ~ spl23_102
| ~ spl23_103 ),
inference(avatar_split_clause,[],[f1851,f1752,f1747,f1421,f316,f1401,f1853]) ).
fof(f1863,definition,
( spl23_111
<=> ! [X0] : ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl23_111])],[avatar_definition]) ).
fof(f1864,plain,
( ! [X0] : ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0)
| ~ spl23_111 ),
inference(avatar_component_clause,[],[f1863]) ).
fof(f1876,plain,
( $false
| ~ spl23_6
| ~ spl23_102
| ~ spl23_111 ),
inference(resolution,[],[f1864,f1785]) ).
fof(f1880,plain,
( ~ spl23_6
| ~ spl23_102
| ~ spl23_111 ),
inference(avatar_contradiction_clause,[],[f1876]) ).
fof(f1881,plain,
( spl23_79
| spl23_56
| ~ spl23_67 ),
inference(avatar_split_clause,[],[f1277,f944,f651,f1220]) ).
fof(f1893,plain,
( ! [X0,X1] :
( sK11(sK0,sK1) = sK12(sK0,sK1)
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_67 ),
inference(forward_demodulation,[],[f1482,f946]) ).
fof(f1909,plain,
( spl23_6
| spl23_79
| ~ spl23_67 ),
inference(avatar_split_clause,[],[f1893,f944,f1220,f316]) ).
fof(f2000,plain,
! [X0,X1] :
( ~ sP18(X0,X1,sK1,sK0)
| sK10(sK0,sK1) = sK11(sK0,sK1)
| in(X0,sK13(sK0,sK1,X1)) ),
inference(forward_demodulation,[],[f1245,f164]) ).
fof(f2001,plain,
! [X0,X1] :
( sP18(X0,X1,sK1,sK0)
| sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ in(X0,sK13(sK0,sK1,X1)) ),
inference(forward_demodulation,[],[f1255,f164]) ).
fof(f2057,plain,
( spl23_67
| spl23_56 ),
inference(avatar_split_clause,[],[f2000,f651,f944]) ).
fof(f2058,plain,
( spl23_67
| spl23_6 ),
inference(avatar_split_clause,[],[f2001,f316,f944]) ).
fof(f2609,plain,
( ! [X0,X1] :
( sK11(sK0,sK1) != sK11(sK0,sK1)
| ~ one_sorted_str(sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(superposition,[],[f140,f1222]) ).
fof(f2610,plain,
( ! [X0,X1] :
( sK11(sK0,sK1) != sK11(sK0,sK1)
| ~ one_sorted_str(sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(superposition,[],[f139,f1222]) ).
fof(f2611,plain,
( ! [X0,X1] :
( ~ one_sorted_str(sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(trivial_inequality_removal,[],[f2610]) ).
fof(f2612,plain,
( ! [X0,X1] :
( ~ one_sorted_str(sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(trivial_inequality_removal,[],[f2609]) ).
fof(f2613,plain,
( ! [X0,X1] :
( ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(forward_subsumption_resolution,[],[f2612,f79]) ).
fof(f2614,plain,
( ! [X0,X1] :
( ~ in(X0,sK13(sK0,sK1,X1))
| sP18(X0,X1,sK1,sK0) )
| ~ spl23_79 ),
inference(forward_subsumption_resolution,[],[f2613,f78]) ).
fof(f2654,plain,
( ! [X0] :
( sP18(sK3(sK13(sK0,sK1,X0)),X0,sK1,sK0)
| sK3(sK13(sK0,sK1,X0)) = ordered_pair(sK4(sK13(sK0,sK1,X0)),sK5(sK13(sK0,sK1,X0))) )
| ~ spl23_79 ),
inference(resolution,[],[f2614,f76]) ).
fof(f2655,plain,
( ! [X0] :
( sP18(sK3(sK13(sK0,sK1,X0)),X0,sK1,sK0)
| in(sK3(sK13(sK0,sK1,X0)),cartesian_product2(sK1,sK2)) )
| ~ spl23_79 ),
inference(resolution,[],[f2614,f77]) ).
fof(f2657,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_79
| ~ spl23_102 ),
inference(resolution,[],[f2614,f1749]) ).
fof(f2661,plain,
( $false
| ~ spl23_79
| ~ spl23_102
| ~ spl23_111 ),
inference(forward_subsumption_resolution,[],[f2657,f1864]) ).
fof(f2662,plain,
( ~ spl23_79
| ~ spl23_102
| ~ spl23_111 ),
inference(avatar_contradiction_clause,[],[f2661]) ).
fof(f2670,plain,
( ! [X0,X1] :
( ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(forward_subsumption_resolution,[],[f2611,f79]) ).
fof(f2694,plain,
( ! [X0,X1] :
( ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_79 ),
inference(forward_subsumption_resolution,[],[f2670,f78]) ).
fof(f2860,plain,
( ! [X0] :
( sK3(sK13(sK0,sK1,X0)) = ordered_pair(sK4(sK13(sK0,sK1,X0)),sK5(sK13(sK0,sK1,X0)))
| sK3(sK13(sK0,sK1,X0)) = sK19(sK0,sK1,X0,sK3(sK13(sK0,sK1,X0))) )
| ~ spl23_79 ),
inference(resolution,[],[f2654,f125]) ).
fof(f2907,plain,
( sK3(sK13(sK0,sK1,sK2)) != sK3(sK13(sK0,sK1,sK2))
| sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_79
| spl23_88 ),
inference(superposition,[],[f1385,f2860]) ).
fof(f2912,plain,
( sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_79
| spl23_88 ),
inference(trivial_inequality_removal,[],[f2907]) ).
fof(f2915,plain,
( $false
| ~ spl23_79
| spl23_83
| spl23_88 ),
inference(forward_subsumption_resolution,[],[f2912,f1352]) ).
fof(f2916,plain,
( ~ spl23_79
| spl23_83
| spl23_88 ),
inference(avatar_contradiction_clause,[],[f2915]) ).
fof(f2933,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_79
| ~ spl23_102 ),
inference(resolution,[],[f2657,f124]) ).
fof(f2934,plain,
( sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_79
| ~ spl23_102 ),
inference(resolution,[],[f2657,f125]) ).
fof(f2935,plain,
( in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| ~ spl23_79
| ~ spl23_102 ),
inference(resolution,[],[f2657,f123]) ).
fof(f2936,plain,
( $false
| ~ spl23_79
| spl23_83
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f2934,f1352]) ).
fof(f2937,plain,
( ~ spl23_79
| spl23_83
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f2936]) ).
fof(f2938,plain,
( $false
| ~ spl23_79
| spl23_92
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f2933,f1422]) ).
fof(f2939,plain,
( ~ spl23_79
| spl23_92
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f2938]) ).
fof(f2945,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_102 ),
inference(resolution,[],[f1748,f76]) ).
fof(f2957,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ spl23_91 ),
inference(equality_resolution,[],[f1402]) ).
fof(f2962,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_79
| ~ spl23_105 ),
inference(resolution,[],[f1764,f2694]) ).
fof(f2966,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| ~ spl23_79
| spl23_102
| ~ spl23_105 ),
inference(forward_subsumption_resolution,[],[f2962,f1748]) ).
fof(f2967,plain,
( element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_79
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(superposition,[],[f1426,f2966]) ).
fof(f2969,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_79
| spl23_85
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(forward_subsumption_resolution,[],[f2967,f1364]) ).
fof(f2970,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_79
| spl23_85
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(resolution,[],[f2969,f2694]) ).
fof(f2978,plain,
( $false
| ~ spl23_79
| spl23_85
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(forward_subsumption_resolution,[],[f2970,f1748]) ).
fof(f2979,plain,
( ~ spl23_79
| spl23_85
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(avatar_contradiction_clause,[],[f2978]) ).
fof(f2980,plain,
( $false
| ~ spl23_79
| spl23_82
| spl23_102
| ~ spl23_105 ),
inference(forward_subsumption_resolution,[],[f1348,f2966]) ).
fof(f2981,plain,
( ~ spl23_79
| spl23_82
| spl23_102
| ~ spl23_105 ),
inference(avatar_contradiction_clause,[],[f2980]) ).
fof(f3011,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_83 ),
inference(superposition,[],[f126,f1353]) ).
fof(f3012,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ spl23_79
| ~ spl23_83 ),
inference(forward_subsumption_resolution,[],[f3011,f2655]) ).
fof(f3016,plain,
( $false
| spl23_88
| spl23_102 ),
inference(forward_subsumption_resolution,[],[f2945,f1385]) ).
fof(f3017,plain,
( spl23_88
| spl23_102 ),
inference(avatar_contradiction_clause,[],[f3016]) ).
fof(f3019,definition,
( spl23_174
<=> in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl23_174])],[avatar_definition]) ).
fof(f3020,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ spl23_174 ),
inference(avatar_component_clause,[],[f3019]) ).
fof(f3021,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| spl23_174 ),
inference(avatar_component_clause,[],[f3019]) ).
fof(f3022,plain,
( ~ spl23_174
| ~ spl23_102
| ~ spl23_91 ),
inference(avatar_split_clause,[],[f2957,f1401,f1747,f3019]) ).
fof(f3039,plain,
( $false
| ~ spl23_79
| ~ spl23_83
| spl23_174 ),
inference(forward_subsumption_resolution,[],[f3012,f3021]) ).
fof(f3040,plain,
( ~ spl23_79
| ~ spl23_83
| spl23_174 ),
inference(avatar_contradiction_clause,[],[f3039]) ).
fof(f3083,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| element(sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))),powerset(the_carrier(sK0)))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_92 ),
inference(superposition,[],[f71,f1423]) ).
fof(f3084,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_92 ),
inference(superposition,[],[f72,f1423]) ).
fof(f3101,plain,
( ! [X0] :
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| sK3(X0) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_103 ),
inference(superposition,[],[f73,f1754]) ).
fof(f3102,plain,
( ! [X0] :
( ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| sK3(X0) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_103
| ~ spl23_110 ),
inference(forward_subsumption_resolution,[],[f3101,f1854]) ).
fof(f3103,plain,
( ! [X0] :
( sK3(X0) != ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_99
| ~ spl23_103
| ~ spl23_110 ),
inference(forward_subsumption_resolution,[],[f3102,f1624]) ).
fof(f3104,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),cartesian_product2(sK1,sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_92
| ~ spl23_99
| ~ spl23_103
| ~ spl23_110 ),
inference(forward_demodulation,[],[f3103,f1423]) ).
fof(f3105,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_92
| ~ spl23_99
| ~ spl23_103
| ~ spl23_110 ),
inference(equality_resolution,[],[f3104]) ).
fof(f3106,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_92
| ~ spl23_99
| ~ spl23_103
| ~ spl23_110
| ~ spl23_174 ),
inference(forward_subsumption_resolution,[],[f3105,f3020]) ).
fof(f3107,plain,
( $false
| ~ spl23_92
| ~ spl23_99
| ~ spl23_102
| ~ spl23_103
| ~ spl23_110
| ~ spl23_174 ),
inference(forward_subsumption_resolution,[],[f3106,f1749]) ).
fof(f3108,plain,
( ~ spl23_92
| ~ spl23_99
| ~ spl23_102
| ~ spl23_103
| ~ spl23_110
| ~ spl23_174 ),
inference(avatar_contradiction_clause,[],[f3107]) ).
fof(f3109,plain,
( spl23_103
| ~ spl23_99
| spl23_91
| ~ spl23_92 ),
inference(avatar_split_clause,[],[f3084,f1421,f1401,f1623,f1752]) ).
fof(f3110,plain,
( spl23_89
| ~ spl23_99
| spl23_91
| ~ spl23_92 ),
inference(avatar_split_clause,[],[f3083,f1421,f1401,f1623,f1388]) ).
fof(f3166,plain,
( $false
| ~ spl23_79
| spl23_99
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f2935,f1625]) ).
fof(f3167,plain,
( ~ spl23_79
| spl23_99
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f3166]) ).
fof(f3208,plain,
( ! [X0] :
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0) )
| ~ spl23_89
| ~ spl23_103 ),
inference(resolution,[],[f1848,f150]) ).
fof(f3213,plain,
( spl23_111
| spl23_110
| ~ spl23_89
| ~ spl23_103 ),
inference(avatar_split_clause,[],[f3208,f1752,f1388,f1853,f1863]) ).
fof(f3349,plain,
( ! [X0] :
( sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0)
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,X0))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) )
| ~ spl23_107 ),
inference(resolution,[],[f1776,f75]) ).
fof(f3352,plain,
( ! [X0] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,X0))
| sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0) )
| spl23_102
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f3349,f1748]) ).
fof(f3358,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_102
| ~ spl23_107 ),
inference(resolution,[],[f3352,f77]) ).
fof(f3359,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_79
| spl23_102
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f3358,f2694]) ).
fof(f3361,plain,
( $false
| ~ spl23_79
| spl23_102
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f3359,f1748]) ).
fof(f3362,plain,
( ~ spl23_79
| spl23_102
| ~ spl23_107 ),
inference(avatar_contradiction_clause,[],[f3361]) ).
fof(f3385,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_6
| ~ spl23_102 ),
inference(resolution,[],[f1785,f124]) ).
fof(f3386,plain,
( sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_6
| ~ spl23_102 ),
inference(resolution,[],[f1785,f125]) ).
fof(f3530,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_6
| ~ spl23_102 ),
inference(superposition,[],[f126,f3386]) ).
fof(f3531,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(sK1,sK2))
| ~ spl23_6
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f3530,f1785]) ).
fof(f3577,plain,
( $false
| ~ spl23_6
| spl23_92
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f3385,f1422]) ).
fof(f3578,plain,
( ~ spl23_6
| spl23_92
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f3577]) ).
fof(f3581,plain,
( $false
| ~ spl23_6
| ~ spl23_102
| spl23_174 ),
inference(forward_subsumption_resolution,[],[f3021,f3531]) ).
fof(f3582,plain,
( ~ spl23_6
| ~ spl23_102
| spl23_174 ),
inference(avatar_contradiction_clause,[],[f3581]) ).
fof(f3649,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_56
| ~ spl23_105 ),
inference(resolution,[],[f1764,f652]) ).
fof(f3656,plain,
( spl23_86
| spl23_85
| ~ spl23_82
| ~ spl23_93 ),
inference(avatar_split_clause,[],[f1845,f1425,f1347,f1363,f1371]) ).
fof(f3657,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_56
| spl23_102
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f3358,f652]) ).
fof(f3659,plain,
( $false
| ~ spl23_56
| spl23_102
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f3657,f1748]) ).
fof(f3660,plain,
( ~ spl23_56
| spl23_102
| ~ spl23_107 ),
inference(avatar_contradiction_clause,[],[f3659]) ).
fof(f3662,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_56
| ~ spl23_86 ),
inference(resolution,[],[f1372,f652]) ).
fof(f3668,plain,
( $false
| ~ spl23_56
| ~ spl23_86
| spl23_102 ),
inference(forward_subsumption_resolution,[],[f3662,f1748]) ).
fof(f3669,plain,
( ~ spl23_56
| ~ spl23_86
| spl23_102 ),
inference(avatar_contradiction_clause,[],[f3668]) ).
fof(f3670,plain,
( spl23_102
| spl23_82
| ~ spl23_56
| ~ spl23_105 ),
inference(avatar_split_clause,[],[f3649,f1763,f651,f1347,f1747]) ).
fof(f3684,plain,
( sK5(sK13(sK0,sK1,sK2)) = subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2)))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_85 ),
inference(resolution,[],[f1365,f145]) ).
fof(f3689,plain,
( spl23_102
| spl23_104
| ~ spl23_85 ),
inference(avatar_split_clause,[],[f3684,f1363,f1758,f1747]) ).
fof(f3701,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_6
| ~ spl23_102 ),
inference(resolution,[],[f1749,f317]) ).
fof(f3704,plain,
( $false
| ~ spl23_6
| spl23_86
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f3701,f1373]) ).
fof(f3705,plain,
( ~ spl23_6
| spl23_86
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f3704]) ).
fof(f3712,plain,
( in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK1)
| ~ spl23_86 ),
inference(resolution,[],[f1372,f123]) ).
fof(f3714,plain,
( $false
| ~ spl23_86
| spl23_99 ),
inference(forward_subsumption_resolution,[],[f1625,f3712]) ).
fof(f3715,plain,
( ~ spl23_86
| spl23_99 ),
inference(avatar_contradiction_clause,[],[f3714]) ).
cnf(s82,plain,
( ~ spl23_88
| spl23_93
| spl23_102 ),
inference(sat_conversion,[],[f1750]) ).
cnf(s87,plain,
( ~ spl23_88
| spl23_102
| spl23_105 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s89,plain,
( ~ spl23_82
| ~ spl23_88
| ~ spl23_104
| spl23_107 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s93,plain,
( ~ spl23_6
| spl23_91
| ~ spl23_92
| ~ spl23_102
| ~ spl23_103
| ~ spl23_110 ),
inference(sat_conversion,[],[f1856]) ).
cnf(s95,plain,
( ~ spl23_6
| ~ spl23_102
| ~ spl23_111 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s96,plain,
( spl23_56
| ~ spl23_67
| spl23_79 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s104,plain,
( spl23_6
| ~ spl23_67
| spl23_79 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s127,plain,
( spl23_56
| spl23_67 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s128,plain,
( spl23_6
| spl23_67 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s192,plain,
( ~ spl23_79
| ~ spl23_102
| ~ spl23_111 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s211,plain,
( ~ spl23_79
| spl23_83
| spl23_88 ),
inference(sat_conversion,[],[f2916]) ).
cnf(s214,plain,
( ~ spl23_79
| spl23_83
| ~ spl23_102 ),
inference(sat_conversion,[],[f2937]) ).
cnf(s215,plain,
( ~ spl23_79
| spl23_92
| ~ spl23_102 ),
inference(sat_conversion,[],[f2939]) ).
cnf(s220,plain,
( ~ spl23_79
| spl23_85
| ~ spl23_93
| spl23_102
| ~ spl23_105 ),
inference(sat_conversion,[],[f2979]) ).
cnf(s221,plain,
( ~ spl23_79
| spl23_82
| spl23_102
| ~ spl23_105 ),
inference(sat_conversion,[],[f2981]) ).
cnf(s225,plain,
( spl23_88
| spl23_102 ),
inference(sat_conversion,[],[f3017]) ).
cnf(s226,plain,
( ~ spl23_91
| ~ spl23_102
| ~ spl23_174 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s229,plain,
( ~ spl23_79
| ~ spl23_83
| spl23_174 ),
inference(sat_conversion,[],[f3040]) ).
cnf(s232,plain,
( ~ spl23_92
| ~ spl23_99
| ~ spl23_102
| ~ spl23_103
| ~ spl23_110
| ~ spl23_174 ),
inference(sat_conversion,[],[f3108]) ).
cnf(s233,plain,
( spl23_91
| ~ spl23_92
| ~ spl23_99
| spl23_103 ),
inference(sat_conversion,[],[f3109]) ).
cnf(s234,plain,
( spl23_89
| spl23_91
| ~ spl23_92
| ~ spl23_99 ),
inference(sat_conversion,[],[f3110]) ).
cnf(s239,plain,
( ~ spl23_79
| spl23_99
| ~ spl23_102 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s242,plain,
( ~ spl23_89
| ~ spl23_103
| spl23_110
| spl23_111 ),
inference(sat_conversion,[],[f3213]) ).
cnf(s247,plain,
( ~ spl23_79
| spl23_102
| ~ spl23_107 ),
inference(sat_conversion,[],[f3362]) ).
cnf(s259,plain,
( ~ spl23_6
| spl23_92
| ~ spl23_102 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s261,plain,
( ~ spl23_6
| ~ spl23_102
| spl23_174 ),
inference(sat_conversion,[],[f3582]) ).
cnf(s265,plain,
( ~ spl23_82
| spl23_85
| spl23_86
| ~ spl23_93 ),
inference(sat_conversion,[],[f3656]) ).
cnf(s266,plain,
( ~ spl23_56
| spl23_102
| ~ spl23_107 ),
inference(sat_conversion,[],[f3660]) ).
cnf(s268,plain,
( ~ spl23_56
| ~ spl23_86
| spl23_102 ),
inference(sat_conversion,[],[f3669]) ).
cnf(s269,plain,
( ~ spl23_56
| spl23_82
| spl23_102
| ~ spl23_105 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s271,plain,
( ~ spl23_85
| spl23_102
| spl23_104 ),
inference(sat_conversion,[],[f3689]) ).
cnf(s272,plain,
( ~ spl23_6
| spl23_86
| ~ spl23_102 ),
inference(sat_conversion,[],[f3705]) ).
cnf(s273,plain,
( ~ spl23_86
| spl23_99 ),
inference(sat_conversion,[],[f3715]) ).
cnf(s312,plain,
( spl23_83
| spl23_82
| ~ spl23_79 ),
inference(rat,[],[s87,s221,s211,s214]) ).
cnf(s314,plain,
( ~ spl23_102
| ~ spl23_174
| ~ spl23_79 ),
inference(rat,[],[s242,s234,s232,s233,s226,s215,s239,s192]) ).
cnf(s315,plain,
( spl23_82
| ~ spl23_79 ),
inference(rat,[],[s87,s221,s225,s314,s229,s312]) ).
cnf(s316,plain,
( spl23_102
| ~ spl23_88
| ~ spl23_79 ),
inference(rat,[],[s271,s220,s89,s82,s87,s247,s315]) ).
cnf(s317,plain,
( ~ spl23_102
| ~ spl23_79 ),
inference(rat,[],[s229,s314,s214]) ).
cnf(s318,plain,
~ spl23_79,
inference(rat,[],[s316,s225,s317]) ).
cnf(s319,plain,
spl23_6,
inference(rat,[],[s104,s128,s318]) ).
cnf(s320,plain,
( spl23_102
| ~ spl23_56 ),
inference(rat,[],[s271,s89,s265,s269,s266,s82,s87,s268,s225]) ).
cnf(s321,plain,
~ spl23_102,
inference(rat,[],[s93,s242,s234,s233,s226,s273,s259,s95,s261,s272,s319]) ).
cnf(s327,plain,
~ spl23_56,
inference(rat,[],[s320,s321]) ).
cnf(s333,plain,
spl23_67,
inference(rat,[],[s127,s327]) ).
cnf(s334,plain,
$false,
inference(rat,[],[s96,s318,s333,s327]) ).
fof(f3716,plain,
$false,
inference(avatar_sat_refutation,[],[s334]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU332+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n015.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 04:47:16 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.51/0.75 % (2263197)Will run a generic schedule for satisfiability detection.
% 1.51/0.75 % (2263204)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1458198345:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.51/0.75 % (2263203)% WARNING: option uhcvi not known.
% 1.51/0.75 % (2263202)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3387707481_2999 on theBenchmark for (2999ds/0Mi)
% 1.51/0.75 % (2263203)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3749372043:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.51/0.75 % (2263205)dis+10_1_sil=32000:sp=arity:random_seed=2525062047:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.51/0.75 % (2263206)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3644841353:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.51/0.75 % (2263207)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1147148750:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.51/0.75 % (2263208)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1699955931:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.51/0.75 % TRYING [1]
% 1.51/0.75 % TRYING [2]
% 1.51/0.75 % TRYING [3]
% 1.51/0.75 % (2263205)Instruction limit reached!
% 1.51/0.75 % (2263205)------------------------------
% 1.51/0.75 % (2263205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.75 % (2263205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.75 % (2263205)CaDiCaL version: 2.1.3
% 1.51/0.75 % (2263205)Termination reason: Instruction limit
% 1.51/0.75 % (2263205)Termination phase: Saturation
% 1.51/0.75 % (2263205)Time elapsed: 0.064 s
% 1.51/0.75 % (2263205)Peak memory usage: 12 MB
% 1.51/0.75 % (2263205)Instructions burned: 107 (million)
% 1.51/0.75 % (2263206)Instruction limit reached!
% 1.51/0.75 % (2263206)------------------------------
% 1.51/0.75 % (2263206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.75 % (2263206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.75 % (2263206)CaDiCaL version: 2.1.3
% 1.51/0.75 % (2263206)Termination reason: Instruction limit
% 1.51/0.75 % (2263206)Termination phase: Saturation
% 1.51/0.75 % (2263206)Time elapsed: 0.067 s
% 1.51/0.75 % (2263206)Peak memory usage: 12 MB
% 1.51/0.75 % (2263206)Instructions burned: 116 (million)
% 1.51/0.75 % (2263207)Instruction limit reached!
% 1.51/0.75 % (2263207)------------------------------
% 1.51/0.75 % (2263207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.75 % (2263207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.75 % (2263207)CaDiCaL version: 2.1.3
% 1.51/0.75 % (2263207)Termination reason: Instruction limit
% 1.51/0.75 % (2263207)Termination phase: Saturation
% 1.51/0.75 % (2263207)Time elapsed: 0.078 s
% 1.51/0.75 % (2263207)Peak memory usage: 13 MB
% 1.51/0.75 % (2263207)Instructions burned: 132 (million)
% 1.51/0.75 % (2263216)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4074227431:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.51/0.75 % (2263217)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1406949888:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.51/0.75 % TRYING [1]
% 1.51/0.75 % TRYING [2]
% 1.51/0.75 % TRYING [3]
% 1.51/0.75 % (2263208)Instruction limit reached!
% 1.51/0.75 % (2263208)------------------------------
% 1.51/0.75 % (2263208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.75 % (2263208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.75 % (2263208)CaDiCaL version: 2.1.3
% 1.51/0.75 % (2263208)Termination reason: Instruction limit
% 1.51/0.75 % (2263208)Termination phase: Saturation
% 1.51/0.75 % (2263208)Time elapsed: 0.094 s
% 1.51/0.75 % (2263208)Peak memory usage: 14 MB
% 1.51/0.75 % (2263208)Instructions burned: 159 (million)
% 1.51/0.75 % (2263218)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3565094490:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.51/0.75 % (2263221)ott-21_1_sil=16000:fs=off:random_seed=2810727941:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.51/0.75 % TRYING [4]
% 1.51/0.75 % (2263217)Instruction limit reached!
% 1.51/0.75 % (2263217)------------------------------
% 1.51/0.75 % (2263217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.75 % (2263217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.76 % (2263217)CaDiCaL version: 2.1.3
% 1.51/0.76 % (2263217)Termination reason: Instruction limit
% 1.51/0.76 % (2263217)Termination phase: Saturation
% 1.51/0.76 % (2263217)Time elapsed: 0.085 s
% 1.51/0.76 % (2263217)Peak memory usage: 13 MB
% 1.51/0.76 % (2263217)Instructions burned: 132 (million)
% 1.51/0.76 % (2263224)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1450257529:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.51/0.76 % (2263221)Instruction limit reached!
% 1.51/0.76 % (2263221)------------------------------
% 1.51/0.76 % (2263221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.76 % (2263221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.76 % (2263221)CaDiCaL version: 2.1.3
% 1.51/0.76 % (2263221)Termination reason: Instruction limit
% 1.51/0.76 % (2263221)Termination phase: Saturation
% 1.51/0.76 % (2263221)Time elapsed: 0.086 s
% 1.51/0.76 % (2263221)Peak memory usage: 12 MB
% 1.51/0.76 % (2263221)Instructions burned: 181 (million)
% 1.51/0.76 % (2263226)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=240169055:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.51/0.76 % TRYING [1]
% 1.51/0.76 % TRYING [2]
% 1.51/0.76 % TRYING [4]
% 1.51/0.76 % TRYING [3]
% 1.51/0.76 % (2263218) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2263197-2263218"...
% 1.51/0.76 % (2263218)...printing done.
% 1.51/0.76 % (2263218)Refutation found. Thanks to Tanya!
% 1.51/0.76 % SZS status Theorem for theBenchmark
% 1.51/0.76 % SZS output start Proof for theBenchmark
% See solution above
% 1.51/0.76 % (2263218)------------------------------
% 1.51/0.76 % (2263218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.51/0.76 % (2263218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.51/0.76 % (2263218)CaDiCaL version: 2.1.3
% 1.51/0.76 % (2263218)Termination reason: Refutation
% 1.51/0.76 % (2263218)Time elapsed: 0.180 s
% 1.51/0.76 % (2263218)Peak memory usage: 15 MB
% 1.51/0.76 % (2263218)Instructions burned: 303 (million)
% 1.51/0.76 % (2263197)Success in time 0.32 s
% 1.51/0.76 % Vampire exiting
%------------------------------------------------------------------------------