%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU329+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 7.40s 1.52s
% Output : Refutation 7.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 16
% Syntax : Number of formulae : 202 ( 11 unt; 14 def)
% Number of atoms : 811 ( 162 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 1015 ( 406 ~; 497 |; 66 &)
% ( 20 <=>; 24 =>; 0 <=; 2 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 3 con; 0-4 aty)
% Number of variables : 269 ( 0 sgn 213 !; 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(complements_of_subsets(the_carrier(X0),X1),X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,complements_of_subsets(the_carrier(X0),X1))
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X5
=> X6 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e4_7_1__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(complements_of_subsets(the_carrier(X0),X1),X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,complements_of_subsets(the_carrier(X0),X1))
& ! [X7] :
( element(X7,powerset(the_carrier(X0)))
=> ( X7 = X5
=> X6 = subset_complement(the_carrier(X0),X7) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f35,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,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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(complements_of_subsets(the_carrier(X0),X1),X2))
& X5 = X4
& ? [X12,X13] :
( ordered_pair(X12,X13) = X4
& in(X12,complements_of_subsets(the_carrier(X0),X1))
& ! [X14] :
( element(X14,powerset(the_carrier(X0)))
=> ( X14 = X12
=> X13 = subset_complement(the_carrier(X0),X14) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_7_1__tops_2__2) ).
fof(f36,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,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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(complements_of_subsets(the_carrier(X0),X1),X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,complements_of_subsets(the_carrier(X0),X1))
& ! [X17] :
( element(X17,powerset(the_carrier(X0)))
=> ( X15 = X17
=> subset_complement(the_carrier(X0),X17) = X16 ) ) ) ) ) ) ),
inference(rectify,[],[f35]) ).
fof(f53,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,complements_of_subsets(the_carrier(X0),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(f54,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,complements_of_subsets(the_carrier(X0),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,[],[f53]) ).
fof(f73,plain,
! [X0,X1] :
( ! [X2] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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,[],[f36]) ).
fof(f74,plain,
! [X0,X1] :
( ! [X2] :
( ? [X12] :
! [X13] :
( in(X13,X12)
<=> ? [X14] :
( in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
& X13 = X14
& ? [X15,X16] :
( ordered_pair(X15,X16) = X13
& in(X15,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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,complements_of_subsets(the_carrier(X0),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,[],[f73]) ).
fof(f75,plain,
! [X3,X6,X5] :
( element(sK6(X5,X6),powerset(the_carrier(sK0)))
| ~ in(X5,complements_of_subsets(the_carrier(sK0),sK1))
| ordered_pair(X5,X6) != sK3(X3)
| ~ in(sK3(X3),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f76,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK3(X3)
| ~ in(X5,complements_of_subsets(the_carrier(sK0),sK1))
| sK6(X5,X6) = X5
| ~ in(sK3(X3),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f77,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK3(X3)
| ~ in(X5,complements_of_subsets(the_carrier(sK0),sK1))
| subset_complement(the_carrier(sK0),sK6(X5,X6)) != X6
| ~ in(sK3(X3),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f78,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,[],[f54]) ).
fof(f79,plain,
! [X3] :
( in(sK4(X3),complements_of_subsets(the_carrier(sK0),sK1))
| in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f80,plain,
! [X3] :
( in(sK3(X3),X3)
| sK3(X3) = ordered_pair(sK4(X3),sK5(X3)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f81,plain,
! [X3] :
( in(sK3(X3),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| in(sK3(X3),X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f82,plain,
element(sK1,powerset(powerset(the_carrier(sK0)))),
inference(cnf_transformation,[],[f54]) ).
fof(f83,plain,
one_sorted_str(sK0),
inference(cnf_transformation,[],[f54]) ).
fof(f125,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f126,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( sK22(X0,X15,X16) = X15
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f127,plain,
! [X2,X0,X1,X16,X14,X15,X13] :
( subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X13
| X13 != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f128,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,[],[f74]) ).
fof(f129,plain,
! [X2,X0,X1,X13] :
( in(sK20(X0,X1,X13),complements_of_subsets(the_carrier(X0),X1))
| ~ sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f130,plain,
! [X2,X0,X1,X13] :
( ~ sP18(X13,X2,X1,X0)
| ordered_pair(sK20(X0,X1,X13),sK21(X0,X1,X13)) = X13 ),
inference(cnf_transformation,[],[f74]) ).
fof(f131,plain,
! [X2,X0,X1,X13] :
( ~ sP18(X13,X2,X1,X0)
| sK19(X0,X1,X2,X13) = X13 ),
inference(cnf_transformation,[],[f74]) ).
fof(f132,plain,
! [X2,X0,X1,X13] :
( in(sK19(X0,X1,X2,X13),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| ~ sP18(X13,X2,X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f145,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,[],[f74]) ).
fof(f146,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,[],[f74]) ).
fof(f147,plain,
! [X2,X0,X1,X13] :
( in(X13,sK13(X0,X1,X2))
| ~ one_sorted_str(X0)
| sK10(X0,X1) = sK11(X0,X1)
| ~ sP18(X13,X2,X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f74]) ).
fof(f148,plain,
! [X2,X0,X1,X13] :
( ~ in(X13,sK13(X0,X1,X2))
| ~ one_sorted_str(X0)
| sK10(X0,X1) = sK11(X0,X1)
| sP18(X13,X2,X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f74]) ).
fof(f149,plain,
! [X2,X0,X1,X13] :
( in(X13,sK13(X0,X1,X2))
| ~ one_sorted_str(X0)
| sK10(X0,X1) = sK12(X0,X1)
| ~ sP18(X13,X2,X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f74]) ).
fof(f150,plain,
! [X2,X0,X1,X13] :
( ~ in(X13,sK13(X0,X1,X2))
| ~ one_sorted_str(X0)
| sK10(X0,X1) = sK12(X0,X1)
| sP18(X13,X2,X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f74]) ).
fof(f151,plain,
! [X3] :
( in(sK3(X3),X3)
| sK5(X3) = subset_complement(the_carrier(sK0),sK4(X3))
| ~ element(sK4(X3),powerset(the_carrier(sK0))) ),
inference(equality_resolution,[],[f78]) ).
fof(f156,plain,
! [X2,X0,X1,X13] :
( ~ element(sK20(X0,X1,X13),powerset(the_carrier(X0)))
| ~ sP18(X13,X2,X1,X0)
| sK21(X0,X1,X13) = subset_complement(the_carrier(X0),sK20(X0,X1,X13)) ),
inference(equality_resolution,[],[f128]) ).
fof(f157,plain,
! [X2,X0,X1,X16,X14,X15] :
( subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f127]) ).
fof(f158,plain,
! [X2,X0,X1,X16,X15] :
( ~ in(ordered_pair(X15,X16),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| subset_complement(the_carrier(X0),sK22(X0,X15,X16)) != X16
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f157]) ).
fof(f159,plain,
! [X2,X0,X1,X16,X14,X15] :
( sK22(X0,X15,X16) = X15
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f126]) ).
fof(f160,plain,
! [X2,X0,X1,X16,X15] :
( ~ in(ordered_pair(X15,X16),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| sK22(X0,X15,X16) = X15
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f159]) ).
fof(f161,plain,
! [X2,X0,X1,X16,X14,X15] :
( element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ordered_pair(X15,X16) != X14
| ~ in(X14,cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f125]) ).
fof(f162,plain,
! [X2,X0,X1,X16,X15] :
( element(sK22(X0,X15,X16),powerset(the_carrier(X0)))
| ~ in(X15,complements_of_subsets(the_carrier(X0),X1))
| ~ in(ordered_pair(X15,X16),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(ordered_pair(X15,X16),X2,X1,X0) ),
inference(equality_resolution,[],[f161]) ).
fof(f1262,definition,
( spl23_13
<=> sK10(sK0,sK1) = sK11(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition]) ).
fof(f1263,plain,
( sK10(sK0,sK1) != sK11(sK0,sK1)
| spl23_13 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1264,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ spl23_13 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1963,definition,
( spl23_17
<=> sK11(sK0,sK1) = sK12(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition]) ).
fof(f1965,plain,
( sK11(sK0,sK1) = sK12(sK0,sK1)
| ~ spl23_17 ),
inference(avatar_component_clause,[],[f1963]) ).
fof(f11557,definition,
( spl23_110
<=> sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl23_110])],[avatar_definition]) ).
fof(f11558,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_110 ),
inference(avatar_component_clause,[],[f11557]) ).
fof(f11559,plain,
( ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| spl23_110 ),
inference(avatar_component_clause,[],[f11557]) ).
fof(f11646,definition,
( spl23_113
<=> sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_113])],[avatar_definition]) ).
fof(f11647,plain,
( sK3(sK13(sK0,sK1,sK2)) != ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_113 ),
inference(avatar_component_clause,[],[f11646]) ).
fof(f11648,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| ~ spl23_113 ),
inference(avatar_component_clause,[],[f11646]) ).
fof(f11653,plain,
( ! [X2,X0,X1] :
( sK5(sK13(sK0,sK1,sK2)) != subset_complement(the_carrier(X0),sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(X0),X1))
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| sP18(sK3(sK13(sK0,sK1,sK2)),X2,X1,X0) )
| ~ spl23_113 ),
inference(superposition,[],[f158,f11648]) ).
fof(f11654,plain,
( ! [X2,X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(X0),X1),X2))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(X0),X1))
| sK4(sK13(sK0,sK1,sK2)) = sK22(X0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),X2,X1,X0) )
| ~ spl23_113 ),
inference(superposition,[],[f160,f11648]) ).
fof(f11816,definition,
( spl23_114
<=> element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0))) ),
introduced(definition,[new_symbols(definition,[spl23_114])],[avatar_definition]) ).
fof(f11817,plain,
( element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| ~ spl23_114 ),
inference(avatar_component_clause,[],[f11816]) ).
fof(f11818,plain,
( ~ element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| spl23_114 ),
inference(avatar_component_clause,[],[f11816]) ).
fof(f11820,definition,
( spl23_115
<=> subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) = sK5(sK13(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl23_115])],[avatar_definition]) ).
fof(f11821,plain,
( subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) != sK5(sK13(sK0,sK1,sK2))
| spl23_115 ),
inference(avatar_component_clause,[],[f11820]) ).
fof(f11822,plain,
( subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) = sK5(sK13(sK0,sK1,sK2))
| ~ spl23_115 ),
inference(avatar_component_clause,[],[f11820]) ).
fof(f12126,definition,
( spl23_116
<=> sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl23_116])],[avatar_definition]) ).
fof(f12128,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| ~ spl23_116 ),
inference(avatar_component_clause,[],[f12126]) ).
fof(f12146,definition,
( spl23_121
<=> ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl23_121])],[avatar_definition]) ).
fof(f12147,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),X0)
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2)) )
| ~ spl23_121 ),
inference(avatar_component_clause,[],[f12146]) ).
fof(f12177,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ spl23_121 ),
inference(equality_resolution,[],[f12147]) ).
fof(f12179,definition,
( spl23_122
<=> in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2)) ),
introduced(definition,[new_symbols(definition,[spl23_122])],[avatar_definition]) ).
fof(f12181,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| spl23_122 ),
inference(avatar_component_clause,[],[f12179]) ).
fof(f12183,definition,
( spl23_123
<=> in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl23_123])],[avatar_definition]) ).
fof(f12184,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_123 ),
inference(avatar_component_clause,[],[f12183]) ).
fof(f12185,plain,
( ~ in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_123 ),
inference(avatar_component_clause,[],[f12183]) ).
fof(f12186,plain,
( ~ spl23_122
| ~ spl23_123
| ~ spl23_121 ),
inference(avatar_split_clause,[],[f12177,f12146,f12183,f12179]) ).
fof(f12285,plain,
( ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),sK1))
| sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_113 ),
inference(resolution,[],[f11654,f81]) ).
fof(f12303,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_113 ),
inference(forward_subsumption_resolution,[],[f12285,f79]) ).
fof(f12305,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_110
| ~ spl23_113 ),
inference(forward_subsumption_resolution,[],[f12303,f11559]) ).
fof(f12307,plain,
( sK4(sK13(sK0,sK1,sK2)) = sK22(sK0,sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_110
| ~ spl23_113
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f12305,f12185]) ).
fof(f12308,plain,
( spl23_116
| spl23_110
| ~ spl23_113
| spl23_123 ),
inference(avatar_split_clause,[],[f12307,f12183,f11646,f11557,f12126]) ).
fof(f12313,plain,
( ~ one_sorted_str(sK0)
| sK10(sK0,sK1) = sK12(sK0,sK1)
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_123 ),
inference(resolution,[],[f12184,f150]) ).
fof(f12317,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f12313,f83]) ).
fof(f12322,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_110
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f12317,f11559]) ).
fof(f12327,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| spl23_110
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f12322,f82]) ).
fof(f12332,plain,
( sK11(sK0,sK1) = sK12(sK0,sK1)
| ~ spl23_13
| spl23_110
| ~ spl23_123 ),
inference(forward_demodulation,[],[f12327,f1264]) ).
fof(f12333,plain,
( spl23_17
| ~ spl23_13
| spl23_110
| ~ spl23_123 ),
inference(avatar_split_clause,[],[f12332,f12183,f11557,f1262,f1963]) ).
fof(f12352,plain,
( ~ one_sorted_str(sK0)
| sK10(sK0,sK1) = sK12(sK0,sK1)
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_123 ),
inference(resolution,[],[f12185,f149]) ).
fof(f12358,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f12352,f83]) ).
fof(f12363,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f12358,f11558]) ).
fof(f12368,plain,
( sK10(sK0,sK1) = sK12(sK0,sK1)
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f12363,f82]) ).
fof(f12373,plain,
( sK11(sK0,sK1) = sK12(sK0,sK1)
| ~ spl23_13
| ~ spl23_110
| spl23_123 ),
inference(forward_demodulation,[],[f12368,f1264]) ).
fof(f12374,plain,
( spl23_17
| ~ spl23_13
| ~ spl23_110
| spl23_123 ),
inference(avatar_split_clause,[],[f12373,f12183,f11557,f1262,f1963]) ).
fof(f12450,plain,
( ! [X0,X1] :
( element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0))
| ~ in(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| sP18(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),X1,X0,sK0) )
| ~ spl23_116 ),
inference(superposition,[],[f162,f12128]) ).
fof(f12456,plain,
( ! [X0,X1] :
( ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0))
| ~ in(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| sP18(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),X1,X0,sK0) )
| spl23_114
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f12450,f11818]) ).
fof(f12461,plain,
( ! [X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0))
| sP18(ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2))),X1,X0,sK0) )
| ~ spl23_113
| spl23_114
| ~ spl23_116 ),
inference(forward_demodulation,[],[f12456,f11648]) ).
fof(f12466,plain,
( ! [X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0)
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0)) )
| ~ spl23_113
| spl23_114
| ~ spl23_116 ),
inference(forward_demodulation,[],[f12461,f11648]) ).
fof(f12482,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),sK1))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_113
| spl23_114
| ~ spl23_116 ),
inference(resolution,[],[f12466,f81]) ).
fof(f12500,plain,
( ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),sK1))
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_110
| ~ spl23_113
| spl23_114
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f12482,f11559]) ).
fof(f12502,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_110
| ~ spl23_113
| spl23_114
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f12500,f79]) ).
fof(f12505,plain,
( $false
| spl23_110
| ~ spl23_113
| spl23_114
| ~ spl23_116
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f12502,f12185]) ).
fof(f12506,plain,
( spl23_110
| ~ spl23_113
| spl23_114
| ~ spl23_116
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f12505]) ).
fof(f13575,plain,
( ! [X0,X1] :
( subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) != sK5(sK13(sK0,sK1,sK2))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0))
| ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0) )
| ~ spl23_113
| ~ spl23_116 ),
inference(superposition,[],[f11653,f12128]) ).
fof(f13578,plain,
( ! [X0,X1] :
( ~ in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),X0),X1))
| ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),X0))
| sP18(sK3(sK13(sK0,sK1,sK2)),X1,X0,sK0) )
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f13575,f11822]) ).
fof(f13584,plain,
( ~ in(sK4(sK13(sK0,sK1,sK2)),complements_of_subsets(the_carrier(sK0),sK1))
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116 ),
inference(resolution,[],[f13578,f81]) ).
fof(f13602,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f13584,f79]) ).
fof(f13604,plain,
( in(sK3(sK13(sK0,sK1,sK2)),sK13(sK0,sK1,sK2))
| spl23_110
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f13602,f11559]) ).
fof(f13607,plain,
( $false
| spl23_110
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f13604,f12185]) ).
fof(f13608,plain,
( spl23_110
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f13607]) ).
fof(f13610,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_110 ),
inference(resolution,[],[f11558,f130]) ).
fof(f13611,plain,
( sK3(sK13(sK0,sK1,sK2)) = sK19(sK0,sK1,sK2,sK3(sK13(sK0,sK1,sK2)))
| ~ spl23_110 ),
inference(resolution,[],[f11558,f131]) ).
fof(f13638,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),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(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110 ),
inference(superposition,[],[f76,f13610]) ).
fof(f13639,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),sK1))
| sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))))
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110 ),
inference(superposition,[],[f77,f13610]) ).
fof(f14056,definition,
( spl23_133
<=> 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_133])],[avatar_definition]) ).
fof(f14058,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_133 ),
inference(avatar_component_clause,[],[f14056]) ).
fof(f14060,definition,
( spl23_134
<=> in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl23_134])],[avatar_definition]) ).
fof(f14061,plain,
( in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),sK1))
| ~ spl23_134 ),
inference(avatar_component_clause,[],[f14060]) ).
fof(f14062,plain,
( ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),sK1))
| spl23_134 ),
inference(avatar_component_clause,[],[f14060]) ).
fof(f14063,plain,
( spl23_133
| ~ spl23_134
| spl23_121
| ~ spl23_110 ),
inference(avatar_split_clause,[],[f13638,f11557,f12146,f14060,f14056]) ).
fof(f14065,plain,
( ! [X0] : ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0)
| spl23_134 ),
inference(resolution,[],[f14062,f129]) ).
fof(f14092,plain,
( $false
| ~ spl23_110
| spl23_134 ),
inference(resolution,[],[f14065,f11558]) ).
fof(f14098,plain,
( ~ spl23_110
| spl23_134 ),
inference(avatar_contradiction_clause,[],[f14092]) ).
fof(f14130,plain,
( ! [X0] :
( element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0)))
| ~ in(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),complements_of_subsets(the_carrier(sK0),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(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_133 ),
inference(superposition,[],[f75,f14058]) ).
fof(f14131,plain,
( ! [X0] :
( element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0)))
| 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(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_133
| ~ spl23_134 ),
inference(forward_subsumption_resolution,[],[f14130,f14061]) ).
fof(f14132,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0)))
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110
| ~ spl23_133
| ~ spl23_134 ),
inference(forward_demodulation,[],[f14131,f13610]) ).
fof(f14134,definition,
( spl23_135
<=> element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0))) ),
introduced(definition,[new_symbols(definition,[spl23_135])],[avatar_definition]) ).
fof(f14136,plain,
( element(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),powerset(the_carrier(sK0)))
| ~ spl23_135 ),
inference(avatar_component_clause,[],[f14134]) ).
fof(f14137,plain,
( spl23_135
| spl23_121
| ~ spl23_110
| ~ spl23_133
| ~ spl23_134 ),
inference(avatar_split_clause,[],[f14132,f14060,f14056,f11557,f12146,f14134]) ).
fof(f14156,plain,
( ! [X0] :
( ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0)
| sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))) )
| ~ spl23_135 ),
inference(resolution,[],[f14136,f156]) ).
fof(f14220,definition,
( spl23_136
<=> 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_136])],[avatar_definition]) ).
fof(f14221,plain,
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| spl23_136 ),
inference(avatar_component_clause,[],[f14220]) ).
fof(f14222,plain,
( sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) = subset_complement(the_carrier(sK0),sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))))
| ~ spl23_136 ),
inference(avatar_component_clause,[],[f14220]) ).
fof(f14610,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2))) != subset_complement(the_carrier(sK0),sK6(sK20(sK0,sK1,sK3(sK13(sK0,sK1,sK2))),sK21(sK0,sK1,sK3(sK13(sK0,sK1,sK2)))))
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110
| ~ spl23_134 ),
inference(forward_subsumption_resolution,[],[f13639,f14061]) ).
fof(f14611,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) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110
| ~ spl23_133
| ~ spl23_134 ),
inference(forward_demodulation,[],[f14610,f14058]) ).
fof(f14612,plain,
( ! [X0] :
( sK3(X0) != sK3(sK13(sK0,sK1,sK2))
| ~ in(sK3(X0),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ in(sK3(X0),X0) )
| ~ spl23_110
| ~ spl23_133
| ~ spl23_134
| ~ spl23_136 ),
inference(forward_subsumption_resolution,[],[f14611,f14222]) ).
fof(f14613,plain,
( spl23_121
| ~ spl23_110
| ~ spl23_133
| ~ spl23_134
| ~ spl23_136 ),
inference(avatar_split_clause,[],[f14612,f14220,f14060,f14056,f11557,f12146]) ).
fof(f14621,plain,
( ! [X0] : ~ sP18(sK3(sK13(sK0,sK1,sK2)),X0,sK1,sK0)
| ~ spl23_135
| spl23_136 ),
inference(forward_subsumption_resolution,[],[f14156,f14221]) ).
fof(f14647,plain,
( $false
| ~ spl23_110
| ~ spl23_135
| spl23_136 ),
inference(resolution,[],[f14621,f11558]) ).
fof(f14653,plain,
( ~ spl23_110
| ~ spl23_135
| spl23_136 ),
inference(avatar_contradiction_clause,[],[f14647]) ).
fof(f14659,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_17 ),
inference(superposition,[],[f146,f1965]) ).
fof(f14660,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_17 ),
inference(superposition,[],[f145,f1965]) ).
fof(f14661,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_17 ),
inference(trivial_inequality_removal,[],[f14660]) ).
fof(f14662,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_17 ),
inference(trivial_inequality_removal,[],[f14659]) ).
fof(f14663,plain,
( ! [X0,X1] :
( ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ sP18(X0,X1,sK1,sK0)
| in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_17 ),
inference(forward_subsumption_resolution,[],[f14661,f83]) ).
fof(f14664,plain,
( ! [X0,X1] :
( ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| sP18(X0,X1,sK1,sK0)
| ~ in(X0,sK13(sK0,sK1,X1)) )
| ~ spl23_17 ),
inference(forward_subsumption_resolution,[],[f14662,f83]) ).
fof(f14665,plain,
( ! [X0,X1] :
( in(X0,sK13(sK0,sK1,X1))
| ~ sP18(X0,X1,sK1,sK0) )
| ~ spl23_17 ),
inference(forward_subsumption_resolution,[],[f14663,f82]) ).
fof(f14666,plain,
( ! [X0,X1] :
( ~ in(X0,sK13(sK0,sK1,X1))
| sP18(X0,X1,sK1,sK0) )
| ~ spl23_17 ),
inference(forward_subsumption_resolution,[],[f14664,f82]) ).
fof(f14705,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_17
| ~ spl23_123 ),
inference(resolution,[],[f14666,f12184]) ).
fof(f15285,plain,
( in(sK3(sK13(sK0,sK1,sK2)),cartesian_product2(complements_of_subsets(the_carrier(sK0),sK1),sK2))
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_110 ),
inference(superposition,[],[f132,f13611]) ).
fof(f15286,plain,
( ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_110
| spl23_122 ),
inference(forward_subsumption_resolution,[],[f15285,f12181]) ).
fof(f15287,plain,
( $false
| ~ spl23_110
| spl23_122 ),
inference(forward_subsumption_resolution,[],[f15286,f11558]) ).
fof(f15288,plain,
( ~ spl23_110
| spl23_122 ),
inference(avatar_contradiction_clause,[],[f15287]) ).
fof(f15416,plain,
( ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ spl23_17
| spl23_123 ),
inference(resolution,[],[f12185,f14665]) ).
fof(f15422,plain,
( ~ one_sorted_str(sK0)
| sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_123 ),
inference(resolution,[],[f12185,f147]) ).
fof(f15432,plain,
( $false
| ~ spl23_17
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15416,f11558]) ).
fof(f15433,plain,
( ~ spl23_17
| ~ spl23_110
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f15432]) ).
fof(f15455,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15422,f83]) ).
fof(f15465,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15455,f11558]) ).
fof(f15467,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15465,f82]) ).
fof(f15469,plain,
( $false
| spl23_13
| ~ spl23_110
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15467,f1263]) ).
fof(f15470,plain,
( spl23_13
| ~ spl23_110
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f15469]) ).
fof(f15514,plain,
( ~ one_sorted_str(sK0)
| sK10(sK0,sK1) = sK11(sK0,sK1)
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_123 ),
inference(resolution,[],[f12184,f148]) ).
fof(f15517,plain,
( sK10(sK0,sK1) = sK11(sK0,sK1)
| sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f15514,f83]) ).
fof(f15522,plain,
( sP18(sK3(sK13(sK0,sK1,sK2)),sK2,sK1,sK0)
| ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_13
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f15517,f1263]) ).
fof(f15527,plain,
( ~ element(sK1,powerset(powerset(the_carrier(sK0))))
| spl23_13
| spl23_110
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f15522,f11559]) ).
fof(f15532,plain,
( $false
| spl23_13
| spl23_110
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f15527,f82]) ).
fof(f15533,plain,
( spl23_13
| spl23_110
| ~ spl23_123 ),
inference(avatar_contradiction_clause,[],[f15532]) ).
fof(f15709,plain,
( subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) = sK5(sK13(sK0,sK1,sK2))
| ~ element(sK4(sK13(sK0,sK1,sK2)),powerset(the_carrier(sK0)))
| spl23_123 ),
inference(resolution,[],[f12185,f151]) ).
fof(f15710,plain,
( sK3(sK13(sK0,sK1,sK2)) = ordered_pair(sK4(sK13(sK0,sK1,sK2)),sK5(sK13(sK0,sK1,sK2)))
| spl23_123 ),
inference(resolution,[],[f12185,f80]) ).
fof(f15721,plain,
( subset_complement(the_carrier(sK0),sK4(sK13(sK0,sK1,sK2))) = sK5(sK13(sK0,sK1,sK2))
| ~ spl23_114
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15709,f11817]) ).
fof(f16179,plain,
( $false
| ~ spl23_114
| spl23_115
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15721,f11821]) ).
fof(f16180,plain,
( ~ spl23_114
| spl23_115
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f16179]) ).
fof(f16940,plain,
( $false
| spl23_113
| spl23_123 ),
inference(forward_subsumption_resolution,[],[f15710,f11647]) ).
fof(f16941,plain,
( spl23_113
| spl23_123 ),
inference(avatar_contradiction_clause,[],[f16940]) ).
fof(f16943,plain,
( $false
| ~ spl23_17
| spl23_110
| ~ spl23_123 ),
inference(forward_subsumption_resolution,[],[f14705,f11559]) ).
fof(f16944,plain,
( ~ spl23_17
| spl23_110
| ~ spl23_123 ),
inference(avatar_contradiction_clause,[],[f16943]) ).
cnf(s102,plain,
( ~ spl23_121
| ~ spl23_122
| ~ spl23_123 ),
inference(sat_conversion,[],[f12186]) ).
cnf(s104,plain,
( spl23_110
| ~ spl23_113
| spl23_116
| spl23_123 ),
inference(sat_conversion,[],[f12308]) ).
cnf(s105,plain,
( ~ spl23_13
| spl23_17
| spl23_110
| ~ spl23_123 ),
inference(sat_conversion,[],[f12333]) ).
cnf(s106,plain,
( ~ spl23_13
| spl23_17
| ~ spl23_110
| spl23_123 ),
inference(sat_conversion,[],[f12374]) ).
cnf(s108,plain,
( spl23_110
| ~ spl23_113
| spl23_114
| ~ spl23_116
| spl23_123 ),
inference(sat_conversion,[],[f12506]) ).
cnf(s114,plain,
( spl23_110
| ~ spl23_113
| ~ spl23_115
| ~ spl23_116
| spl23_123 ),
inference(sat_conversion,[],[f13608]) ).
cnf(s119,plain,
( ~ spl23_110
| spl23_121
| spl23_133
| ~ spl23_134 ),
inference(sat_conversion,[],[f14063]) ).
cnf(s120,plain,
( ~ spl23_110
| spl23_134 ),
inference(sat_conversion,[],[f14098]) ).
cnf(s121,plain,
( ~ spl23_110
| spl23_121
| ~ spl23_133
| ~ spl23_134
| spl23_135 ),
inference(sat_conversion,[],[f14137]) ).
cnf(s124,plain,
( ~ spl23_110
| spl23_121
| ~ spl23_133
| ~ spl23_134
| ~ spl23_136 ),
inference(sat_conversion,[],[f14613]) ).
cnf(s125,plain,
( ~ spl23_110
| ~ spl23_135
| spl23_136 ),
inference(sat_conversion,[],[f14653]) ).
cnf(s127,plain,
( ~ spl23_110
| spl23_122 ),
inference(sat_conversion,[],[f15288]) ).
cnf(s128,plain,
( ~ spl23_17
| ~ spl23_110
| spl23_123 ),
inference(sat_conversion,[],[f15433]) ).
cnf(s129,plain,
( spl23_13
| ~ spl23_110
| spl23_123 ),
inference(sat_conversion,[],[f15470]) ).
cnf(s130,plain,
( spl23_13
| spl23_110
| ~ spl23_123 ),
inference(sat_conversion,[],[f15533]) ).
cnf(s135,plain,
( ~ spl23_114
| spl23_115
| spl23_123 ),
inference(sat_conversion,[],[f16180]) ).
cnf(s136,plain,
( spl23_113
| spl23_123 ),
inference(sat_conversion,[],[f16941]) ).
cnf(s137,plain,
( ~ spl23_17
| spl23_110
| ~ spl23_123 ),
inference(sat_conversion,[],[f16944]) ).
cnf(s157,plain,
( ~ spl23_116
| spl23_123
| spl23_110
| ~ spl23_113 ),
inference(rat,[],[s135,s108,s114]) ).
cnf(s158,plain,
( ~ spl23_113
| spl23_123
| spl23_110 ),
inference(rat,[],[s157,s104]) ).
cnf(s159,plain,
( spl23_110
| ~ spl23_17 ),
inference(rat,[],[s158,s136,s137]) ).
cnf(s160,plain,
( ~ spl23_133
| spl23_121
| ~ spl23_110
| ~ spl23_134 ),
inference(rat,[],[s125,s124,s121]) ).
cnf(s161,plain,
( spl23_121
| ~ spl23_134
| ~ spl23_110 ),
inference(rat,[],[s160,s119]) ).
cnf(s162,plain,
~ spl23_17,
inference(rat,[],[s161,s102,s128,s120,s127,s159]) ).
cnf(s163,plain,
( ~ spl23_123
| spl23_110 ),
inference(rat,[],[s105,s130,s162]) ).
cnf(s164,plain,
spl23_110,
inference(rat,[],[s158,s136,s163]) ).
cnf(s165,plain,
spl23_122,
inference(rat,[],[s127,s164]) ).
cnf(s166,plain,
spl23_134,
inference(rat,[],[s120,s164]) ).
cnf(s167,plain,
spl23_121,
inference(rat,[],[s161,s164,s166]) ).
cnf(s168,plain,
~ spl23_123,
inference(rat,[],[s102,s165,s167]) ).
cnf(s170,plain,
spl23_13,
inference(rat,[],[s129,s164,s168]) ).
cnf(s171,plain,
$false,
inference(rat,[],[s106,s162,s164,s170,s168]) ).
fof(f16945,plain,
$false,
inference(avatar_sat_refutation,[],[s171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU329+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 28 04:43:19 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.32 Running first-order model finding
% 0.03/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.40/1.52 % (3021869)Will run a generic schedule for satisfiability detection.
% 7.40/1.52 % (3021875)% WARNING: option uhcvi not known.
% 7.40/1.52 % (3021874)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3504376539_2999 on theBenchmark for (2999ds/0Mi)
% 7.40/1.52 % (3021875)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4021689572:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.40/1.52 % (3021876)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3738792629:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.40/1.52 % (3021877)dis+10_1_sil=32000:sp=arity:random_seed=1848994654:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.40/1.52 % (3021878)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=156305435:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.40/1.52 % (3021879)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2089470284:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.40/1.52 % (3021880)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1546465602:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.40/1.52 % TRYING [1]
% 7.40/1.52 % TRYING [2]
% 7.40/1.52 % TRYING [3]
% 7.40/1.52 % (3021877)Instruction limit reached!
% 7.40/1.52 % (3021877)------------------------------
% 7.40/1.52 % (3021877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021877)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021877)Termination reason: Instruction limit
% 7.40/1.52 % (3021877)Termination phase: Saturation
% 7.40/1.52 % (3021877)Time elapsed: 0.034 s
% 7.40/1.52 % (3021877)Peak memory usage: 12 MB
% 7.40/1.52 % (3021877)Instructions burned: 104 (million)
% 7.40/1.52 % (3021878)Instruction limit reached!
% 7.40/1.52 % (3021878)------------------------------
% 7.40/1.52 % (3021878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021878)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021878)Termination reason: Instruction limit
% 7.40/1.52 % (3021878)Termination phase: Saturation
% 7.40/1.52 % (3021878)Time elapsed: 0.037 s
% 7.40/1.52 % (3021878)Peak memory usage: 13 MB
% 7.40/1.52 % (3021878)Instructions burned: 119 (million)
% 7.40/1.52 % (3021879)Instruction limit reached!
% 7.40/1.52 % (3021879)------------------------------
% 7.40/1.52 % (3021879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021879)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021879)Termination reason: Instruction limit
% 7.40/1.52 % (3021879)Termination phase: Saturation
% 7.40/1.52 % (3021879)Time elapsed: 0.041 s
% 7.40/1.52 % (3021879)Peak memory usage: 13 MB
% 7.40/1.52 % (3021879)Instructions burned: 132 (million)
% 7.40/1.52 % (3021888)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=309537149:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.40/1.52 % (3021889)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1953131283:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.40/1.52 % TRYING [1]
% 7.40/1.52 % TRYING [2]
% 7.40/1.52 % (3021890)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=4251597522:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.40/1.52 % TRYING [3]
% 7.40/1.52 % (3021880)Instruction limit reached!
% 7.40/1.52 % (3021880)------------------------------
% 7.40/1.52 % (3021880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021880)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021880)Termination reason: Instruction limit
% 7.40/1.52 % (3021880)Termination phase: Saturation
% 7.40/1.52 % (3021880)Time elapsed: 0.056 s
% 7.40/1.52 % (3021880)Peak memory usage: 14 MB
% 7.40/1.52 % (3021880)Instructions burned: 160 (million)
% 7.40/1.52 % (3021894)ott-21_1_sil=16000:fs=off:random_seed=4138142161:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.40/1.52 % (3021889)Instruction limit reached!
% 7.40/1.52 % (3021889)------------------------------
% 7.40/1.52 % (3021889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021889)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021889)Termination reason: Instruction limit
% 7.40/1.52 % (3021889)Termination phase: Saturation
% 7.40/1.52 % (3021889)Time elapsed: 0.047 s
% 7.40/1.52 % (3021889)Peak memory usage: 13 MB
% 7.40/1.52 % (3021889)Instructions burned: 134 (million)
% 7.40/1.52 % (3021896)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=487737321:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.40/1.52 % (3021894)Instruction limit reached!
% 7.40/1.52 % (3021894)------------------------------
% 7.40/1.52 % (3021894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021894)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021894)Termination reason: Instruction limit
% 7.40/1.52 % (3021894)Termination phase: Saturation
% 7.40/1.52 % (3021894)Time elapsed: 0.048 s
% 7.40/1.52 % (3021894)Peak memory usage: 12 MB
% 7.40/1.52 % (3021894)Instructions burned: 180 (million)
% 7.40/1.52 % (3021898)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1703806530:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.40/1.52 % TRYING [1]
% 7.40/1.52 % TRYING [2]
% 7.40/1.52 % TRYING [3]
% 7.40/1.52 % TRYING [4]
% 7.40/1.52 % (3021888)Instruction limit reached!
% 7.40/1.52 % (3021888)------------------------------
% 7.40/1.52 % (3021888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021888)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021888)Termination reason: Instruction limit
% 7.40/1.52 % (3021888)Termination phase: Finite model building SAT solving
% 7.40/1.52 % (3021888)Time elapsed: 0.208 s
% 7.40/1.52 % (3021888)Peak memory usage: 16 MB
% 7.40/1.52 % (3021888)Instructions burned: 717 (million)
% 7.40/1.52 % TRYING [4]
% 7.40/1.52 % (3021890)Instruction limit reached!
% 7.40/1.52 % (3021890)------------------------------
% 7.40/1.52 % (3021890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021890)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021890)Termination reason: Instruction limit
% 7.40/1.52 % (3021890)Termination phase: Saturation
% 7.40/1.52 % (3021890)Time elapsed: 0.211 s
% 7.40/1.52 % (3021890)Peak memory usage: 18 MB
% 7.40/1.52 % (3021890)Instructions burned: 685 (million)
% 7.40/1.52 % (3021900)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1837819313:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.40/1.52 % (3021901)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2589506553:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 7.40/1.52 % (3021896)Instruction limit reached!
% 7.40/1.52 % (3021896)------------------------------
% 7.40/1.52 % (3021896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021896)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021896)Termination reason: Instruction limit
% 7.40/1.52 % (3021896)Termination phase: Saturation
% 7.40/1.52 % (3021896)Time elapsed: 0.172 s
% 7.40/1.52 % (3021896)Peak memory usage: 14 MB
% 7.40/1.52 % (3021896)Instructions burned: 477 (million)
% 7.40/1.52 % (3021904)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3967556142:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 7.40/1.52 % (3021898)Instruction limit reached!
% 7.40/1.52 % (3021898)------------------------------
% 7.40/1.52 % (3021898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021898)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021898)Termination reason: Instruction limit
% 7.40/1.52 % (3021898)Termination phase: Finite model building SAT solving
% 7.40/1.52 % (3021898)Time elapsed: 0.263 s
% 7.40/1.52 % (3021898)Peak memory usage: 16 MB
% 7.40/1.52 % (3021898)Instructions burned: 867 (million)
% 7.40/1.52 % (3021906)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1508755026:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 7.40/1.52 % (3021904)Instruction limit reached!
% 7.40/1.52 % (3021904)------------------------------
% 7.40/1.52 % (3021904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021904)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021904)Termination reason: Instruction limit
% 7.40/1.52 % (3021904)Termination phase: Saturation
% 7.40/1.52 % (3021904)Time elapsed: 0.189 s
% 7.40/1.52 % (3021904)Peak memory usage: 16 MB
% 7.40/1.52 % (3021904)Instructions burned: 693 (million)
% 7.40/1.52 % (3021908)fmb+10_1_sil=64000:random_seed=2593910191:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 7.40/1.52 % TRYING [1]
% 7.40/1.52 % TRYING [2]
% 7.40/1.52 % TRYING [3]
% 7.40/1.52 % (3021901)Instruction limit reached!
% 7.40/1.52 % (3021901)------------------------------
% 7.40/1.52 % (3021901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021901)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021901)Termination reason: Instruction limit
% 7.40/1.52 % (3021901)Termination phase: Finite model building constraint generation
% 7.40/1.52 % (3021901)Time elapsed: 0.236 s
% 7.40/1.52 % (3021901)Peak memory usage: 108 MB
% 7.40/1.52 % (3021901)Instructions burned: 893 (million)
% 7.40/1.52 % (3021910)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2839900591:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 7.40/1.52 % TRYING [20]
% 7.40/1.52 % TRYING [4]
% 7.40/1.52 % (3021900)Instruction limit reached!
% 7.40/1.52 % (3021900)------------------------------
% 7.40/1.52 % (3021900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021900)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021900)Termination reason: Instruction limit
% 7.40/1.52 % (3021900)Termination phase: Saturation
% 7.40/1.52 % (3021900)Time elapsed: 0.331 s
% 7.40/1.52 % (3021900)Peak memory usage: 22 MB
% 7.40/1.52 % (3021900)Instructions burned: 1180 (million)
% 7.40/1.52 % (3021912)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=406657489:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 7.40/1.52 % TRYING [8]
% 7.40/1.52 % (3021906)Instruction limit reached!
% 7.40/1.52 % (3021906)------------------------------
% 7.40/1.52 % (3021906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021906)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021906)Termination reason: Instruction limit
% 7.40/1.52 % (3021906)Termination phase: Saturation
% 7.40/1.52 % (3021906)Time elapsed: 0.299 s
% 7.40/1.52 % (3021906)Peak memory usage: 17 MB
% 7.40/1.52 % (3021906)Instructions burned: 880 (million)
% 7.40/1.52 % (3021914)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2552899765:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 7.40/1.52 % (3021912)Instruction limit reached!
% 7.40/1.52 % (3021912)------------------------------
% 7.40/1.52 % (3021912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.52 % (3021912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.52 % (3021912)CaDiCaL version: 2.1.3
% 7.40/1.52 % (3021912)Termination reason: Instruction limit
% 7.40/1.52 % (3021912)Termination phase: Finite model building constraint generation
% 7.40/1.52 % (3021912)Time elapsed: 0.213 s
% 7.40/1.52 % (3021912)Peak memory usage: 94 MB
% 7.40/1.52 % (3021912)Instructions burned: 924 (million)
% 7.40/1.52 % (3021916)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2150219041:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 7.40/1.52 % (3021914) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3021869-3021914"...
% 7.40/1.52 % (3021914)...printing done.
% 7.40/1.52 % (3021914)Refutation found. Thanks to Tanya!
% 7.40/1.52 % SZS status Theorem for theBenchmark
% 7.40/1.52 % SZS output start Proof for theBenchmark
% See solution above
% 7.40/1.53 % (3021914)------------------------------
% 7.40/1.53 % (3021914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.40/1.53 % (3021914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.40/1.53 % (3021914)CaDiCaL version: 2.1.3
% 7.40/1.53 % (3021914)Termination reason: Refutation
% 7.40/1.53 % (3021914)Time elapsed: 0.443 s
% 7.40/1.53 % (3021914)Peak memory usage: 19 MB
% 7.40/1.53 % (3021914)Instructions burned: 1647 (million)
% 7.40/1.53 % (3021869)Success in time 1.203 s
% 7.40/1.53 % Vampire exiting
%------------------------------------------------------------------------------