%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU332+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:23 PM UTC 2026
% Result : Theorem 140.66s 20.98s
% Output : Refutation 142.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 5
% Syntax : Number of formulae : 110 ( 7 unt; 1 def)
% Number of atoms : 772 ( 217 equ)
% Maximal formula atoms : 23 ( 7 avg)
% Number of connectives : 1099 ( 437 ~; 467 |; 160 &)
% ( 8 <=>; 25 =>; 0 <=; 2 <~>)
% Maximal formula depth : 20 ( 11 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 3 con; 0-4 aty)
% Number of variables : 515 ( 403 !; 112 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f100,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f277,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l55_zfmisc_1) ).
fof(f339,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/sandbox2/benchmark/theBenchmark.p',s1_tarski__e4_7_2__tops_2__2) ).
fof(f351,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/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e4_7_2__tops_2__1) ).
fof(f352,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)],[f351]) ).
fof(f555,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,[],[f339]) ).
fof(f563,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,[],[f352]) ).
fof(f564,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,[],[f563]) ).
fof(f605,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,[],[f555]) ).
fof(f606,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,[],[f605]) ).
fof(f609,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f100]) ).
fof(f683,definition,
! [X1,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))) ) ) )
| ~ sP5(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f684,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))) ) ) ) )
| sP5(X1,X0) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(definition_folding,[],[f606,f683]) ).
fof(f694,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X1,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X1)
| ? [X7] :
( subset_complement(the_carrier(X0),X7) != X6
& X5 = X7
& element(X7,powerset(the_carrier(X0))) ) )
| ~ 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))) ) ) )
| in(X4,X3) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(nnf_transformation,[],[f564]) ).
fof(f695,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X1,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X1)
| ? [X7] :
( subset_complement(the_carrier(X0),X7) != X6
& X5 = X7
& element(X7,powerset(the_carrier(X0))) ) )
| ~ 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))) ) ) )
| in(X4,X3) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(flattening,[],[f694]) ).
fof(f696,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X1,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X1)
| ? [X7] :
( subset_complement(the_carrier(X0),X7) != X6
& X5 = X7
& element(X7,powerset(the_carrier(X0))) ) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X1,X2))
& ? [X8,X9] :
( ordered_pair(X8,X9) = X4
& in(X8,X1)
& ! [X10] :
( subset_complement(the_carrier(X0),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(X0))) ) ) )
| in(X4,X3) ) )
& one_sorted_str(X0)
& element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(rectify,[],[f695]) ).
fof(f697,plain,
( ! [X3] :
( ( ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ! [X5,X6] :
( ordered_pair(X5,X6) != sK14(X3)
| ~ in(X5,sK12)
| ( subset_complement(the_carrier(sK11),sK15(X5,X6)) != X6
& sK15(X5,X6) = X5
& element(sK15(X5,X6),powerset(the_carrier(sK11))) ) )
| ~ in(sK14(X3),X3) )
& ( ( in(sK14(X3),cartesian_product2(sK12,sK13))
& sK14(X3) = ordered_pair(sK16(X3),sK17(X3))
& in(sK16(X3),sK12)
& ! [X10] :
( sK17(X3) = subset_complement(the_carrier(sK11),X10)
| sK16(X3) != X10
| ~ element(X10,powerset(the_carrier(sK11))) ) )
| in(sK14(X3),X3) ) )
& one_sorted_str(sK11)
& element(sK12,powerset(powerset(the_carrier(sK11)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14,sK15,sK16,sK17]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X4,sK14(X3)),skolemize(X7,sK15(X5,X6)),skolemize(X8,sK16(X3)),skolemize(X9,sK17(X3))],[f696]) ).
fof(f734,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f277]) ).
fof(f735,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f734]) ).
fof(f763,plain,
! [X1,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))) ) ) )
| ~ sP5(X1,X0) ),
inference(nnf_transformation,[],[f683]) ).
fof(f764,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5,X6] :
( ordered_pair(X5,X6) = X3
& in(X5,X0)
& ! [X7] :
( subset_complement(the_carrier(X1),X7) = X6
| X5 != X7
| ~ element(X7,powerset(the_carrier(X1))) ) )
& X2 = X4
& ? [X8,X9] :
( ordered_pair(X8,X9) = X4
& in(X8,X0)
& ! [X10] :
( subset_complement(the_carrier(X1),X10) = X9
| X8 != X10
| ~ element(X10,powerset(the_carrier(X1))) ) ) )
| ~ sP5(X0,X1) ),
inference(rectify,[],[f763]) ).
fof(f765,plain,
! [X0,X1] :
( ( sK103(X0,X1) != sK104(X0,X1)
& sK102(X0,X1) = sK103(X0,X1)
& sK103(X0,X1) = ordered_pair(sK105(X0,X1),sK106(X0,X1))
& in(sK105(X0,X1),X0)
& ! [X7] :
( subset_complement(the_carrier(X1),X7) = sK106(X0,X1)
| sK105(X0,X1) != X7
| ~ element(X7,powerset(the_carrier(X1))) )
& sK102(X0,X1) = sK104(X0,X1)
& sK104(X0,X1) = ordered_pair(sK107(X0,X1),sK108(X0,X1))
& in(sK107(X0,X1),X0)
& ! [X10] :
( subset_complement(the_carrier(X1),X10) = sK108(X0,X1)
| sK107(X0,X1) != X10
| ~ element(X10,powerset(the_carrier(X1))) ) )
| ~ sP5(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK102,sK103,sK104,sK105,sK106,sK107,sK108]),skolemize(X2,sK102(X0,X1)),skolemize(X3,sK103(X0,X1)),skolemize(X4,sK104(X0,X1)),skolemize(X5,sK105(X0,X1)),skolemize(X6,sK106(X0,X1)),skolemize(X8,sK107(X0,X1)),skolemize(X9,sK108(X0,X1))],[f764]) ).
fof(f766,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))) ) ) ) )
& ( ? [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))) ) ) )
| ~ in(X13,X12) ) )
| sP5(X1,X0) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(nnf_transformation,[],[f684]) ).
fof(f767,plain,
! [X0,X1] :
( ! [X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ! [X5] :
( ~ in(X5,cartesian_product2(X1,X2))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(X6,X1)
| ? [X8] :
( subset_complement(the_carrier(X0),X8) != X7
& X6 = X8
& element(X8,powerset(the_carrier(X0))) ) ) ) )
& ( ? [X9] :
( in(X9,cartesian_product2(X1,X2))
& X4 = X9
& ? [X10,X11] :
( ordered_pair(X10,X11) = X4
& in(X10,X1)
& ! [X12] :
( subset_complement(the_carrier(X0),X12) = X11
| X10 != X12
| ~ element(X12,powerset(the_carrier(X0))) ) ) )
| ~ in(X4,X3) ) )
| sP5(X1,X0) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(rectify,[],[f766]) ).
fof(f768,plain,
! [X0,X1] :
( ! [X2] :
( ! [X4] :
( ( in(X4,sK109(X0,X1,X2))
| ! [X5] :
( ~ in(X5,cartesian_product2(X1,X2))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(X6,X1)
| ( subset_complement(the_carrier(X0),sK110(X0,X6,X7)) != X7
& sK110(X0,X6,X7) = X6
& element(sK110(X0,X6,X7),powerset(the_carrier(X0))) ) ) ) )
& ( ( in(sK111(X0,X1,X2,X4),cartesian_product2(X1,X2))
& sK111(X0,X1,X2,X4) = X4
& ordered_pair(sK112(X0,X1,X4),sK113(X0,X1,X4)) = X4
& in(sK112(X0,X1,X4),X1)
& ! [X12] :
( subset_complement(the_carrier(X0),X12) = sK113(X0,X1,X4)
| sK112(X0,X1,X4) != X12
| ~ element(X12,powerset(the_carrier(X0))) ) )
| ~ in(X4,sK109(X0,X1,X2)) ) )
| sP5(X1,X0) )
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109,sK110,sK111,sK112,sK113]),skolemize(X3,sK109(X0,X1,X2)),skolemize(X8,sK110(X0,X6,X7)),skolemize(X9,sK111(X0,X1,X2,X4)),skolemize(X10,sK112(X0,X1,X4)),skolemize(X11,sK113(X0,X1,X4))],[f767]) ).
fof(f852,plain,
element(sK12,powerset(powerset(the_carrier(sK11)))),
inference(cnf_transformation,[],[f697]) ).
fof(f853,plain,
one_sorted_str(sK11),
inference(cnf_transformation,[],[f697]) ).
fof(f854,plain,
! [X3,X10] :
( sK17(X3) = subset_complement(the_carrier(sK11),X10)
| sK16(X3) != X10
| ~ element(X10,powerset(the_carrier(sK11)))
| in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f856,plain,
! [X3] :
( sK14(X3) = ordered_pair(sK16(X3),sK17(X3))
| in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f857,plain,
! [X3] :
( in(sK14(X3),cartesian_product2(sK12,sK13))
| in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f858,plain,
! [X3,X6,X5] :
( ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ordered_pair(X5,X6) != sK14(X3)
| ~ in(X5,sK12)
| element(sK15(X5,X6),powerset(the_carrier(sK11)))
| ~ in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f859,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK14(X3)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(X5,sK12)
| sK15(X5,X6) = X5
| ~ in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f860,plain,
! [X3,X6,X5] :
( ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ordered_pair(X5,X6) != sK14(X3)
| ~ in(X5,sK12)
| subset_complement(the_carrier(sK11),sK15(X5,X6)) != X6
| ~ in(sK14(X3),X3) ),
inference(cnf_transformation,[],[f697]) ).
fof(f945,plain,
! [X2,X3,X0,X1] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f735]) ).
fof(f1015,plain,
! [X0,X1] :
( sK102(X0,X1) = sK104(X0,X1)
| ~ sP5(X0,X1) ),
inference(cnf_transformation,[],[f765]) ).
fof(f1019,plain,
! [X0,X1] :
( sK102(X0,X1) = sK103(X0,X1)
| ~ sP5(X0,X1) ),
inference(cnf_transformation,[],[f765]) ).
fof(f1020,plain,
! [X0,X1] :
( sK103(X0,X1) != sK104(X0,X1)
| ~ sP5(X0,X1) ),
inference(cnf_transformation,[],[f765]) ).
fof(f1021,plain,
! [X2,X0,X1,X4,X12] :
( subset_complement(the_carrier(X0),X12) = sK113(X0,X1,X4)
| sK112(X0,X1,X4) != X12
| ~ element(X12,powerset(the_carrier(X0)))
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1022,plain,
! [X2,X0,X1,X4] :
( in(sK112(X0,X1,X4),X1)
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1023,plain,
! [X2,X0,X1,X4] :
( ordered_pair(sK112(X0,X1,X4),sK113(X0,X1,X4)) = X4
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1024,plain,
! [X2,X0,X1,X4] :
( sK111(X0,X1,X2,X4) = X4
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1025,plain,
! [X2,X0,X1,X4] :
( in(sK111(X0,X1,X2,X4),cartesian_product2(X1,X2))
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1026,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| X4 != X5
| ordered_pair(X6,X7) != X4
| ~ in(X6,X1)
| element(sK110(X0,X6,X7),powerset(the_carrier(X0)))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1027,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| X4 != X5
| ordered_pair(X6,X7) != X4
| ~ in(X6,X1)
| sK110(X0,X6,X7) = X6
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1028,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| X4 != X5
| ordered_pair(X6,X7) != X4
| ~ in(X6,X1)
| subset_complement(the_carrier(X0),sK110(X0,X6,X7)) != X7
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(cnf_transformation,[],[f768]) ).
fof(f1031,plain,
! [X0,X1] :
( set_difference(X0,X1) = subset_complement(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f609]) ).
fof(f1252,plain,
! [X3] :
( sK17(X3) = subset_complement(the_carrier(sK11),sK16(X3))
| ~ element(sK16(X3),powerset(the_carrier(sK11)))
| in(sK14(X3),X3) ),
inference(equality_resolution,[],[f854]) ).
fof(f1284,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| ordered_pair(X6,X7) != X5
| ~ in(X6,X1)
| subset_complement(the_carrier(X0),sK110(X0,X6,X7)) != X7
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1028]) ).
fof(f1285,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| ~ in(X6,X1)
| subset_complement(the_carrier(X0),sK110(X0,X6,X7)) != X7
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1284]) ).
fof(f1286,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| ordered_pair(X6,X7) != X5
| ~ in(X6,X1)
| sK110(X0,X6,X7) = X6
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1027]) ).
fof(f1287,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| ~ in(X6,X1)
| sK110(X0,X6,X7) = X6
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1286]) ).
fof(f1288,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK109(X0,X1,X2))
| ~ in(X5,cartesian_product2(X1,X2))
| ordered_pair(X6,X7) != X5
| ~ in(X6,X1)
| element(sK110(X0,X6,X7),powerset(the_carrier(X0)))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1026]) ).
fof(f1289,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| ~ in(X6,X1)
| element(sK110(X0,X6,X7),powerset(the_carrier(X0)))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1288]) ).
fof(f1290,plain,
! [X2,X0,X1,X4] :
( sK113(X0,X1,X4) = subset_complement(the_carrier(X0),sK112(X0,X1,X4))
| ~ element(sK112(X0,X1,X4),powerset(the_carrier(X0)))
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(equality_resolution,[],[f1021]) ).
fof(f1354,plain,
! [X2,X0,X1,X4] :
( sK113(X0,X1,X4) = set_difference(the_carrier(X0),sK112(X0,X1,X4))
| ~ element(sK112(X0,X1,X4),powerset(the_carrier(X0)))
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_demodulation,[],[f1290,f1031]) ).
fof(f1355,plain,
! [X2,X0,X1,X4] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ in(X4,sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| in(X4,cartesian_product2(X1,X2)) ),
inference(forward_subsumption_demodulation,[],[f1025,f1024]) ).
fof(f1356,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| ~ in(X6,X1)
| element(X6,powerset(the_carrier(X0)))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(backward_subsumption_demodulation,[],[f1289,f1287]) ).
fof(f1357,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| ~ in(X6,X1)
| subset_complement(the_carrier(X0),X6) != X7
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_demodulation,[],[f1285,f1287]) ).
fof(f1360,plain,
! [X0,X1] :
( sK103(X0,X1) = sK104(X0,X1)
| ~ sP5(X0,X1) ),
inference(backward_subsumption_demodulation,[],[f1015,f1019]) ).
fof(f1399,plain,
! [X3] :
( sK17(X3) = set_difference(the_carrier(sK11),sK16(X3))
| ~ element(sK16(X3),powerset(the_carrier(sK11)))
| in(sK14(X3),X3) ),
inference(forward_subsumption_demodulation,[],[f1252,f1031]) ).
fof(f1400,plain,
! [X3,X6,X5] :
( ordered_pair(X5,X6) != sK14(X3)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(X5,sK12)
| element(X5,powerset(the_carrier(sK11)))
| ~ in(sK14(X3),X3) ),
inference(backward_subsumption_demodulation,[],[f858,f859]) ).
fof(f1401,plain,
! [X3,X6,X5] :
( subset_complement(the_carrier(sK11),X5) != X6
| ordered_pair(X5,X6) != sK14(X3)
| ~ in(X5,sK12)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(sK14(X3),X3) ),
inference(forward_subsumption_demodulation,[],[f860,f859]) ).
fof(f1406,plain,
! [X2,X0,X1,X6,X7] :
( in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| element(X6,powerset(the_carrier(X0)))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f1356,f945]) ).
fof(f1407,plain,
! [X2,X0,X1,X6,X7] :
( subset_complement(the_carrier(X0),X6) != X7
| ~ in(ordered_pair(X6,X7),cartesian_product2(X1,X2))
| in(ordered_pair(X6,X7),sK109(X0,X1,X2))
| sP5(X1,X0)
| ~ one_sorted_str(X0)
| ~ element(X1,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f1357,f945]) ).
fof(f1408,plain,
! [X0,X1] : ~ sP5(X0,X1),
inference(forward_subsumption_resolution,[],[f1360,f1020]) ).
fof(f1416,plain,
! [X2,X0,X1] :
( set_difference(the_carrier(sK11),X0) != X1
| ordered_pair(X0,X1) != sK14(X2)
| ~ in(X0,sK12)
| ~ in(sK14(X2),cartesian_product2(sK12,sK13))
| ~ in(sK14(X2),X2)
| ~ element(X0,powerset(the_carrier(sK11))) ),
inference(superposition,[],[f1401,f1031]) ).
fof(f1418,plain,
! [X2,X3,X0,X1,X4] :
( set_difference(the_carrier(X0),X1) != X2
| ~ in(ordered_pair(X1,X2),cartesian_product2(X3,X4))
| in(ordered_pair(X1,X2),sK109(X0,X3,X4))
| sP5(X3,X0)
| ~ one_sorted_str(X0)
| ~ element(X3,powerset(powerset(the_carrier(X0))))
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(superposition,[],[f1407,f1031]) ).
fof(f1419,plain,
! [X2,X3,X0,X1,X4] :
( set_difference(the_carrier(X0),X1) != X2
| ~ in(ordered_pair(X1,X2),cartesian_product2(X3,X4))
| in(ordered_pair(X1,X2),sK109(X0,X3,X4))
| sP5(X3,X0)
| ~ one_sorted_str(X0)
| ~ element(X3,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f1418,f1406]) ).
fof(f1420,plain,
! [X2,X0,X1] :
( set_difference(the_carrier(sK11),X0) != X1
| ordered_pair(X0,X1) != sK14(X2)
| ~ in(X0,sK12)
| ~ in(sK14(X2),cartesian_product2(sK12,sK13))
| ~ in(sK14(X2),X2) ),
inference(forward_subsumption_resolution,[],[f1416,f1400]) ).
fof(f1422,plain,
! [X2,X3,X0,X1,X4] :
( set_difference(the_carrier(X0),X1) != X2
| ~ in(ordered_pair(X1,X2),cartesian_product2(X3,X4))
| in(ordered_pair(X1,X2),sK109(X0,X3,X4))
| ~ one_sorted_str(X0)
| ~ element(X3,powerset(powerset(the_carrier(X0)))) ),
inference(forward_subsumption_resolution,[],[f1419,f1408]) ).
fof(f1424,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,set_difference(the_carrier(X1),X0)),sK109(X1,X2,X3))
| ~ in(ordered_pair(X0,set_difference(the_carrier(X1),X0)),cartesian_product2(X2,X3))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1)))) ),
inference(equality_resolution,[],[f1422]) ).
fof(f1432,plain,
! [X2,X0,X1] :
( in(ordered_pair(sK16(X0),sK17(X0)),sK109(sK11,X1,X2))
| ~ in(ordered_pair(sK16(X0),sK17(X0)),cartesian_product2(X1,X2))
| ~ one_sorted_str(sK11)
| ~ element(X1,powerset(powerset(the_carrier(sK11))))
| ~ element(sK16(X0),powerset(the_carrier(sK11)))
| in(sK14(X0),X0) ),
inference(superposition,[],[f1424,f1399]) ).
fof(f1436,plain,
! [X2,X0,X1] :
( in(ordered_pair(sK16(X0),sK17(X0)),sK109(sK11,X1,X2))
| ~ in(ordered_pair(sK16(X0),sK17(X0)),cartesian_product2(X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(sK11))))
| ~ element(sK16(X0),powerset(the_carrier(sK11)))
| in(sK14(X0),X0) ),
inference(forward_subsumption_resolution,[],[f1432,f853]) ).
fof(f1440,plain,
! [X2,X0,X1] :
( in(sK14(X0),sK109(sK11,X1,X2))
| ~ in(ordered_pair(sK16(X0),sK17(X0)),cartesian_product2(X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(sK11))))
| ~ element(sK16(X0),powerset(the_carrier(sK11)))
| in(sK14(X0),X0) ),
inference(forward_subsumption_demodulation,[],[f1436,f856]) ).
fof(f1444,plain,
! [X2,X0,X1] :
( in(sK14(X0),sK109(sK11,X1,X2))
| ~ in(sK14(X0),cartesian_product2(X1,X2))
| ~ element(X1,powerset(powerset(the_carrier(sK11))))
| ~ element(sK16(X0),powerset(the_carrier(sK11)))
| in(sK14(X0),X0) ),
inference(forward_subsumption_demodulation,[],[f1440,f856]) ).
fof(f1455,plain,
! [X0,X1] :
( ~ in(X0,sK109(sK11,sK12,X1))
| sP5(sK12,sK11)
| ~ one_sorted_str(sK11)
| in(X0,cartesian_product2(sK12,X1)) ),
inference(resolution,[],[f1355,f852]) ).
fof(f1456,plain,
! [X0,X1] :
( ~ in(X0,sK109(sK11,sK12,X1))
| ~ one_sorted_str(sK11)
| in(X0,cartesian_product2(sK12,X1)) ),
inference(forward_subsumption_resolution,[],[f1455,f1408]) ).
fof(f1457,plain,
! [X0,X1] :
( ~ in(X0,sK109(sK11,sK12,X1))
| in(X0,cartesian_product2(sK12,X1)) ),
inference(forward_subsumption_resolution,[],[f1456,f853]) ).
fof(f1504,plain,
! [X2,X3,X0,X1,X4] :
( sK113(sK11,X0,X1) != X2
| sK14(X3) != ordered_pair(sK112(sK11,X0,X1),X2)
| ~ in(sK112(sK11,X0,X1),sK12)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(sK14(X3),X3)
| ~ element(sK112(sK11,X0,X1),powerset(the_carrier(sK11)))
| ~ in(X1,sK109(sK11,X0,X4))
| sP5(X0,sK11)
| ~ one_sorted_str(sK11)
| ~ element(X0,powerset(powerset(the_carrier(sK11)))) ),
inference(superposition,[],[f1420,f1354]) ).
fof(f1519,plain,
! [X2,X3,X0,X1,X4] :
( sK113(sK11,X0,X1) != X2
| sK14(X3) != ordered_pair(sK112(sK11,X0,X1),X2)
| ~ in(sK112(sK11,X0,X1),sK12)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(sK14(X3),X3)
| ~ in(X1,sK109(sK11,X0,X4))
| sP5(X0,sK11)
| ~ one_sorted_str(sK11)
| ~ element(X0,powerset(powerset(the_carrier(sK11)))) ),
inference(forward_subsumption_resolution,[],[f1504,f1400]) ).
fof(f1523,plain,
! [X2,X3,X0,X1,X4] :
( sK113(sK11,X0,X1) != X2
| sK14(X3) != ordered_pair(sK112(sK11,X0,X1),X2)
| ~ in(sK112(sK11,X0,X1),sK12)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(sK14(X3),X3)
| ~ in(X1,sK109(sK11,X0,X4))
| sP5(X0,sK11)
| ~ element(X0,powerset(powerset(the_carrier(sK11)))) ),
inference(forward_subsumption_resolution,[],[f1519,f853]) ).
fof(f1527,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X3) != ordered_pair(sK112(sK11,X0,X1),X2)
| sK113(sK11,X0,X1) != X2
| ~ in(sK112(sK11,X0,X1),sK12)
| ~ in(sK14(X3),cartesian_product2(sK12,sK13))
| ~ in(sK14(X3),X3)
| ~ in(X1,sK109(sK11,X0,X4))
| ~ element(X0,powerset(powerset(the_carrier(sK11)))) ),
inference(forward_subsumption_resolution,[],[f1523,f1408]) ).
fof(f1529,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X1) != X0
| sK113(sK11,X2,X0) != sK113(sK11,X2,X0)
| ~ in(sK112(sK11,X2,X0),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(X0,sK109(sK11,X2,X3))
| ~ element(X2,powerset(powerset(the_carrier(sK11))))
| ~ in(X0,sK109(sK11,X2,X4))
| sP5(X2,sK11)
| ~ one_sorted_str(sK11)
| ~ element(X2,powerset(powerset(the_carrier(sK11)))) ),
inference(superposition,[],[f1527,f1023]) ).
fof(f1530,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X1) != X0
| sK113(sK11,X2,X0) != sK113(sK11,X2,X0)
| ~ in(sK112(sK11,X2,X0),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(X0,sK109(sK11,X2,X3))
| ~ element(X2,powerset(powerset(the_carrier(sK11))))
| ~ in(X0,sK109(sK11,X2,X4))
| sP5(X2,sK11)
| ~ one_sorted_str(sK11) ),
inference(duplicate_literal_removal,[],[f1529]) ).
fof(f1531,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X1) != X0
| ~ in(sK112(sK11,X2,X0),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(X0,sK109(sK11,X2,X3))
| ~ element(X2,powerset(powerset(the_carrier(sK11))))
| ~ in(X0,sK109(sK11,X2,X4))
| sP5(X2,sK11)
| ~ one_sorted_str(sK11) ),
inference(trivial_inequality_removal,[],[f1530]) ).
fof(f1532,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X1) != X0
| ~ in(sK112(sK11,X2,X0),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(X0,sK109(sK11,X2,X3))
| ~ element(X2,powerset(powerset(the_carrier(sK11))))
| ~ in(X0,sK109(sK11,X2,X4))
| sP5(X2,sK11) ),
inference(forward_subsumption_resolution,[],[f1531,f853]) ).
fof(f1533,plain,
! [X2,X3,X0,X1,X4] :
( sK14(X1) != X0
| ~ in(sK112(sK11,X2,X0),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(X0,sK109(sK11,X2,X3))
| ~ element(X2,powerset(powerset(the_carrier(sK11))))
| ~ in(X0,sK109(sK11,X2,X4)) ),
inference(forward_subsumption_resolution,[],[f1532,f1408]) ).
fof(f1534,plain,
! [X2,X3,X0,X1] :
( ~ in(sK112(sK11,X0,sK14(X1)),sK12)
| ~ in(sK14(X1),cartesian_product2(sK12,sK13))
| ~ in(sK14(X1),X1)
| ~ in(sK14(X1),sK109(sK11,X0,X2))
| ~ element(X0,powerset(powerset(the_carrier(sK11))))
| ~ in(sK14(X1),sK109(sK11,X0,X3)) ),
inference(equality_resolution,[],[f1533]) ).
fof(f1535,plain,
! [X2,X3,X0,X1] :
( ~ in(sK14(X0),cartesian_product2(sK12,sK13))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),sK109(sK11,sK12,X3))
| sP5(sK12,sK11)
| ~ one_sorted_str(sK11)
| ~ element(sK12,powerset(powerset(the_carrier(sK11)))) ),
inference(resolution,[],[f1534,f1022]) ).
fof(f1536,plain,
! [X2,X3,X0,X1] :
( ~ in(sK14(X0),cartesian_product2(sK12,sK13))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),sK109(sK11,sK12,X3))
| sP5(sK12,sK11)
| ~ one_sorted_str(sK11) ),
inference(duplicate_literal_removal,[],[f1535]) ).
fof(f1537,plain,
! [X2,X3,X0,X1] :
( ~ in(sK14(X0),cartesian_product2(sK12,sK13))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),sK109(sK11,sK12,X3))
| sP5(sK12,sK11)
| ~ one_sorted_str(sK11) ),
inference(forward_subsumption_resolution,[],[f1536,f852]) ).
fof(f1538,plain,
! [X2,X3,X0,X1] :
( ~ in(sK14(X0),cartesian_product2(sK12,sK13))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),sK109(sK11,sK12,X3))
| ~ one_sorted_str(sK11) ),
inference(forward_subsumption_resolution,[],[f1537,f1408]) ).
fof(f1539,plain,
! [X2,X3,X0,X1] :
( ~ in(sK14(X0),sK109(sK11,sK12,X3))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),cartesian_product2(sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f1538,f853]) ).
fof(f1543,plain,
! [X2,X0,X1] :
( ~ in(sK14(X0),sK109(sK11,sK12,X2))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ in(sK14(X0),cartesian_product2(sK12,sK13)) ),
inference(factoring,[],[f1539]) ).
fof(f1546,plain,
! [X0,X1] :
( ~ in(sK14(X0),sK109(sK11,sK12,X1))
| ~ in(sK14(X0),X0)
| ~ in(sK14(X0),cartesian_product2(sK12,sK13)) ),
inference(factoring,[],[f1543]) ).
fof(f1548,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13)) ),
inference(factoring,[],[f1546]) ).
fof(f1549,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| ~ element(sK16(sK109(sK11,sK12,X0)),powerset(the_carrier(sK11)))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0)) ),
inference(resolution,[],[f1548,f1444]) ).
fof(f1550,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| ~ element(sK16(sK109(sK11,sK12,X0)),powerset(the_carrier(sK11)))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0)) ),
inference(forward_subsumption_resolution,[],[f1549,f852]) ).
fof(f1551,plain,
! [X0] :
( in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ element(sK16(sK109(sK11,sK12,X0)),powerset(the_carrier(sK11)))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0)) ),
inference(forward_subsumption_resolution,[],[f1550,f857]) ).
fof(f1576,plain,
! [X2,X3,X0,X1] :
( in(sK14(X0),sK109(X1,X2,X3))
| ~ in(sK14(X0),cartesian_product2(X2,X3))
| element(sK16(X0),powerset(the_carrier(X1)))
| sP5(X2,X1)
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| in(sK14(X0),X0) ),
inference(superposition,[],[f1406,f856]) ).
fof(f1581,plain,
! [X2,X3,X0,X1] :
( in(sK14(X0),sK109(X1,X2,X3))
| ~ in(sK14(X0),cartesian_product2(X2,X3))
| element(sK16(X0),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(powerset(the_carrier(X1))))
| in(sK14(X0),X0) ),
inference(forward_subsumption_resolution,[],[f1576,f1408]) ).
fof(f1586,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| element(sK16(sK109(sK11,sK12,X0)),powerset(the_carrier(sK11)))
| ~ one_sorted_str(sK11)
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13)) ),
inference(resolution,[],[f1581,f1548]) ).
fof(f1588,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| ~ one_sorted_str(sK11)
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f1586,f1551]) ).
fof(f1589,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| ~ element(sK12,powerset(powerset(the_carrier(sK11))))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f1588,f853]) ).
fof(f1590,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0))
| in(sK14(sK109(sK11,sK12,X0)),sK109(sK11,sK12,X0))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13)) ),
inference(forward_subsumption_resolution,[],[f1589,f852]) ).
fof(f1591,plain,
! [X0] :
( ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,sK13))
| ~ in(sK14(sK109(sK11,sK12,X0)),cartesian_product2(sK12,X0)) ),
inference(forward_subsumption_resolution,[],[f1590,f1548]) ).
fof(f1593,plain,
~ in(sK14(sK109(sK11,sK12,sK13)),cartesian_product2(sK12,sK13)),
inference(factoring,[],[f1591]) ).
fof(f1594,plain,
in(sK14(sK109(sK11,sK12,sK13)),sK109(sK11,sK12,sK13)),
inference(resolution,[],[f1593,f857]) ).
fof(f1599,plain,
in(sK14(sK109(sK11,sK12,sK13)),cartesian_product2(sK12,sK13)),
inference(resolution,[],[f1594,f1457]) ).
fof(f1600,plain,
$false,
inference(forward_subsumption_resolution,[],[f1599,f1593]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU332+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.43 % Computer : n014.cluster.edu
% 0.09/0.43 % Model : x86_64 x86_64
% 0.09/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.43 % Memory : 8046.5625MB
% 0.09/0.43 % OS : Linux 6.8.0-71-generic
% 0.09/0.43 % CPULimit : 300
% 0.09/0.43 % WCLimit : 300
% 0.09/0.43 % DateTime : Mon Sep 28 04:47:06 UTC 2026
% 0.09/0.43 % CPUTime :
% 0.09/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.68/2.69 % (1436057)Detected formulas, will run a generic FOF schedule.
% 11.68/2.69 % (1436065)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2617866891:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.68/2.69 % (1436065)Instruction limit reached!
% 11.68/2.69 % (1436065)------------------------------
% 11.68/2.69 % (1436065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.69 % (1436065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.69 % (1436065)CaDiCaL version: 2.1.3
% 11.68/2.69 % (1436065)Termination reason: Instruction limit
% 11.68/2.69 % (1436065)Termination phase: Saturation
% 11.68/2.69 % (1436065)Time elapsed: 0.035 s
% 11.68/2.69 % (1436065)Peak memory usage: 91 MB
% 11.68/2.69 % (1436065)Instructions burned: 113 (million)
% 11.68/2.69 % (1436066)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1916135974:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.68/2.69 % (1436068)dis-21_1_sil=8000:lcm=predicate:random_seed=3887227510:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.68/2.69 % (1436064)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2543108253:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.68/2.69 % (1436062)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1734021072:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.68/2.69 % (1436067)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3429890014:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.68/2.69 % (1436063)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3890286090:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.68/2.69 % (1436068)Instruction limit reached!
% 11.68/2.69 % (1436068)------------------------------
% 11.68/2.69 % (1436068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.69 % (1436068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.69 % (1436068)CaDiCaL version: 2.1.3
% 11.68/2.69 % (1436068)Termination reason: Instruction limit
% 11.68/2.69 % (1436068)Termination phase: Saturation
% 11.68/2.69 % (1436068)Time elapsed: 0.067 s
% 11.68/2.69 % (1436068)Peak memory usage: 90 MB
% 11.68/2.69 % (1436068)Instructions burned: 130 (million)
% 11.68/2.69 % (1436066)Instruction limit reached!
% 11.68/2.69 % (1436066)------------------------------
% 11.68/2.69 % (1436066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.69 % (1436066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.69 % (1436066)CaDiCaL version: 2.1.3
% 11.68/2.69 % (1436066)Termination reason: Instruction limit
% 11.68/2.69 % (1436066)Termination phase: Saturation
% 11.68/2.69 % (1436066)Time elapsed: 0.073 s
% 11.68/2.69 % (1436066)Peak memory usage: 90 MB
% 11.68/2.69 % (1436066)Instructions burned: 119 (million)
% 11.68/2.69 % (1436070)lrs+10_1_sil=8000:sp=occurrence:random_seed=2151066979:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.68/2.69 % (1436067)Instruction limit reached!
% 11.68/2.69 % (1436067)------------------------------
% 11.68/2.69 % (1436067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.69 % (1436067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.69 % (1436067)CaDiCaL version: 2.1.3
% 11.68/2.69 % (1436067)Termination reason: Instruction limit
% 11.68/2.69 % (1436067)Termination phase: Saturation
% 11.68/2.69 % (1436067)Time elapsed: 0.092 s
% 11.68/2.69 % (1436067)Peak memory usage: 91 MB
% 11.68/2.69 % (1436067)Instructions burned: 140 (million)
% 11.68/2.69 % (1436070)Instruction limit reached!
% 11.68/2.69 % (1436070)------------------------------
% 11.68/2.69 % (1436070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.69 % (1436070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.69 % (1436070)CaDiCaL version: 2.1.3
% 11.68/2.69 % (1436070)Termination reason: Instruction limit
% 11.68/2.69 % (1436070)Termination phase: Saturation
% 11.68/2.69 % (1436070)Time elapsed: 0.100 s
% 11.68/2.69 % (1436070)Peak memory usage: 95 MB
% 11.68/2.69 % (1436070)Instructions burned: 287 (million)
% 18.20/3.59 % (1436077)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2877932733:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.20/3.59 % (1436079)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2120411412:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.20/3.59 % (1436080)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3374256344:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 18.20/3.59 % (1436081)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1175871436:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 18.20/3.59 % (1436077)Instruction limit reached!
% 18.20/3.59 % (1436077)------------------------------
% 18.20/3.59 % (1436077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.20/3.59 % (1436077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.20/3.59 % (1436077)CaDiCaL version: 2.1.3
% 18.20/3.59 % (1436077)Termination reason: Instruction limit
% 18.20/3.59 % (1436077)Termination phase: Saturation
% 18.20/3.59 % (1436077)Time elapsed: 0.093 s
% 18.20/3.59 % (1436077)Peak memory usage: 91 MB
% 18.20/3.59 % (1436077)Instructions burned: 158 (million)
% 18.20/3.59 % (1436081)Instruction limit reached!
% 18.20/3.59 % (1436081)------------------------------
% 18.20/3.59 % (1436081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.20/3.59 % (1436081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.20/3.59 % (1436081)CaDiCaL version: 2.1.3
% 18.20/3.59 % (1436081)Termination reason: Instruction limit
% 18.20/3.59 % (1436081)Termination phase: Saturation
% 18.20/3.59 % (1436081)Time elapsed: 0.100 s
% 18.20/3.59 % (1436081)Peak memory usage: 93 MB
% 18.20/3.59 % (1436081)Instructions burned: 296 (million)
% 18.20/3.59 % (1436080)Instruction limit reached!
% 18.20/3.59 % (1436080)------------------------------
% 18.20/3.59 % (1436080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.20/3.59 % (1436080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.20/3.59 % (1436080)CaDiCaL version: 2.1.3
% 18.20/3.59 % (1436080)Termination reason: Instruction limit
% 18.20/3.59 % (1436080)Termination phase: Saturation
% 18.20/3.59 % (1436080)Time elapsed: 0.156 s
% 18.20/3.59 % (1436080)Peak memory usage: 94 MB
% 18.20/3.59 % (1436080)Instructions burned: 248 (million)
% 18.20/3.59 % (1436079)Instruction limit reached!
% 18.20/3.59 % (1436079)------------------------------
% 18.20/3.59 % (1436079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.20/3.59 % (1436079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.20/3.59 % (1436079)CaDiCaL version: 2.1.3
% 18.20/3.59 % (1436079)Termination reason: Instruction limit
% 18.20/3.59 % (1436079)Termination phase: Saturation
% 18.20/3.59 % (1436079)Time elapsed: 0.222 s
% 18.20/3.59 % (1436079)Peak memory usage: 94 MB
% 18.20/3.59 % (1436079)Instructions burned: 326 (million)
% 18.20/3.59 % (1436086)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=328343214:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 18.20/3.59 % (1436087)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2428057670:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.20/3.59 % (1436087)Instruction limit reached!
% 18.20/3.59 % (1436087)------------------------------
% 18.20/3.59 % (1436087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.20/3.59 % (1436087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.20/3.59 % (1436087)CaDiCaL version: 2.1.3
% 18.20/3.59 % (1436087)Termination reason: Instruction limit
% 18.20/3.59 % (1436087)Termination phase: Saturation
% 18.20/3.59 % (1436087)Time elapsed: 0.037 s
% 18.20/3.59 % (1436087)Peak memory usage: 91 MB
% 18.20/3.59 % (1436087)Instructions burned: 116 (million)
% 18.20/3.59 % (1436088)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1063691334:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 18.20/3.59 % (1436089)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2104297280:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 18.20/3.59 % (1436092)lrs+10_1_sil=8000:sp=occurrence:random_seed=2173963034:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 18.20/3.59 % (1436088)Instruction limit reached!
% 18.20/3.59 % (1436088)------------------------------
% 43.66/7.11 % (1436088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436088)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436088)Termination reason: Instruction limit
% 43.66/7.11 % (1436088)Termination phase: Saturation
% 43.66/7.11 % (1436088)Time elapsed: 0.070 s
% 43.66/7.11 % (1436088)Peak memory usage: 91 MB
% 43.66/7.11 % (1436088)Instructions burned: 127 (million)
% 43.66/7.11 % (1436089)Instruction limit reached!
% 43.66/7.11 % (1436089)------------------------------
% 43.66/7.11 % (1436089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436089)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436089)Termination reason: Instruction limit
% 43.66/7.11 % (1436089)Termination phase: Saturation
% 43.66/7.11 % (1436089)Time elapsed: 0.055 s
% 43.66/7.11 % (1436089)Peak memory usage: 89 MB
% 43.66/7.11 % (1436089)Instructions burned: 114 (million)
% 43.66/7.11 % (1436096)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3095821595:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 43.66/7.11 % (1436097)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3427484470:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 43.66/7.11 % (1436092)Instruction limit reached!
% 43.66/7.11 % (1436092)------------------------------
% 43.66/7.11 % (1436092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436092)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436092)Termination reason: Instruction limit
% 43.66/7.11 % (1436092)Termination phase: Saturation
% 43.66/7.11 % (1436092)Time elapsed: 0.316 s
% 43.66/7.11 % (1436092)Peak memory usage: 104 MB
% 43.66/7.11 % (1436092)Instructions burned: 909 (million)
% 43.66/7.11 % (1436100)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2988062244:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 43.66/7.11 % (1436096)Instruction limit reached!
% 43.66/7.11 % (1436096)------------------------------
% 43.66/7.11 % (1436096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436096)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436096)Termination reason: Instruction limit
% 43.66/7.11 % (1436096)Termination phase: Saturation
% 43.66/7.11 % (1436096)Time elapsed: 0.272 s
% 43.66/7.11 % (1436096)Peak memory usage: 95 MB
% 43.66/7.11 % (1436096)Instructions burned: 438 (million)
% 43.66/7.11 % (1436100)Instruction limit reached!
% 43.66/7.11 % (1436100)------------------------------
% 43.66/7.11 % (1436100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436100)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436100)Termination reason: Instruction limit
% 43.66/7.11 % (1436100)Termination phase: Saturation
% 43.66/7.11 % (1436100)Time elapsed: 0.040 s
% 43.66/7.11 % (1436100)Peak memory usage: 92 MB
% 43.66/7.11 % (1436100)Instructions burned: 135 (million)
% 43.66/7.11 % (1436103)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2960808798:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi)
% 43.66/7.11 % (1436102)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4090157391:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 43.66/7.11 % (1436102)Instruction limit reached!
% 43.66/7.11 % (1436102)------------------------------
% 43.66/7.11 % (1436102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.66/7.11 % (1436102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.66/7.11 % (1436102)CaDiCaL version: 2.1.3
% 43.66/7.11 % (1436102)Termination reason: Instruction limit
% 43.66/7.11 % (1436102)Termination phase: Saturation
% 43.66/7.11 % (1436102)Time elapsed: 0.362 s
% 43.66/7.11 % (1436102)Peak memory usage: 99 MB
% 43.66/7.11 % (1436102)Instructions burned: 593 (million)
% 43.66/7.11 % (1436106)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=313381687:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 69.64/10.75 % (1436106)Instruction limit reached!
% 69.64/10.75 % (1436106)------------------------------
% 69.64/10.75 % (1436106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436106)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436106)Termination reason: Instruction limit
% 69.64/10.75 % (1436106)Termination phase: Saturation
% 69.64/10.75 % (1436106)Time elapsed: 0.081 s
% 69.64/10.75 % (1436106)Peak memory usage: 92 MB
% 69.64/10.75 % (1436106)Instructions burned: 125 (million)
% 69.64/10.75 % (1436108)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=930922037:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 69.64/10.75 % (1436086)Instruction limit reached!
% 69.64/10.75 % (1436086)------------------------------
% 69.64/10.75 % (1436086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436086)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436086)Termination reason: Instruction limit
% 69.64/10.75 % (1436086)Termination phase: Saturation
% 69.64/10.75 % (1436086)Time elapsed: 1.488 s
% 69.64/10.75 % (1436086)Peak memory usage: 146 MB
% 69.64/10.75 % (1436086)Instructions burned: 2351 (million)
% 69.64/10.75 % (1436108)Instruction limit reached!
% 69.64/10.75 % (1436108)------------------------------
% 69.64/10.75 % (1436108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436108)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436108)Termination reason: Instruction limit
% 69.64/10.75 % (1436108)Termination phase: Saturation
% 69.64/10.75 % (1436108)Time elapsed: 0.074 s
% 69.64/10.75 % (1436108)Peak memory usage: 92 MB
% 69.64/10.75 % (1436108)Instructions burned: 134 (million)
% 69.64/10.75 % (1436111)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2521734968:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 69.64/10.75 % (1436110)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=84310794:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 69.64/10.75 % (1436110)Instruction limit reached!
% 69.64/10.75 % (1436110)------------------------------
% 69.64/10.75 % (1436110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436110)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436110)Termination reason: Instruction limit
% 69.64/10.75 % (1436110)Termination phase: Saturation
% 69.64/10.75 % (1436110)Time elapsed: 0.073 s
% 69.64/10.75 % (1436110)Peak memory usage: 91 MB
% 69.64/10.75 % (1436110)Instructions burned: 141 (million)
% 69.64/10.75 % (1436114)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2362779723:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 69.64/10.75 % (1436111)Instruction limit reached!
% 69.64/10.75 % (1436111)------------------------------
% 69.64/10.75 % (1436111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436111)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436111)Termination reason: Instruction limit
% 69.64/10.75 % (1436111)Termination phase: Saturation
% 69.64/10.75 % (1436111)Time elapsed: 0.250 s
% 69.64/10.75 % (1436111)Peak memory usage: 95 MB
% 69.64/10.75 % (1436111)Instructions burned: 433 (million)
% 69.64/10.75 % (1436116)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2550835399:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi)
% 69.64/10.75 % (1436116)Instruction limit reached!
% 69.64/10.75 % (1436116)------------------------------
% 69.64/10.75 % (1436116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.64/10.75 % (1436116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.64/10.75 % (1436116)CaDiCaL version: 2.1.3
% 69.64/10.75 % (1436116)Termination reason: Instruction limit
% 69.64/10.75 % (1436116)Termination phase: Saturation
% 69.64/10.75 % (1436116)Time elapsed: 0.083 s
% 69.64/10.75 % (1436116)Peak memory usage: 92 MB
% 95.63/14.50 % (1436116)Instructions burned: 150 (million)
% 95.63/14.50 % (1436118)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1336836053:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi)
% 95.63/14.50 % (1436097)Instruction limit reached!
% 95.63/14.50 % (1436097)------------------------------
% 95.63/14.50 % (1436097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436097)CaDiCaL version: 2.1.3
% 95.63/14.50 % (1436097)Termination reason: Instruction limit
% 95.63/14.50 % (1436097)Termination phase: Saturation
% 95.63/14.50 % (1436097)Time elapsed: 3.159 s
% 95.63/14.50 % (1436097)Peak memory usage: 158 MB
% 95.63/14.50 % (1436097)Instructions burned: 5203 (million)
% 95.63/14.50 % (1436120)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3941038694:i=667:av=off:fsr=off_2959 on theBenchmark for (2959ds/667Mi)
% 95.63/14.50 % (1436120)Instruction limit reached!
% 95.63/14.50 % (1436120)------------------------------
% 95.63/14.50 % (1436120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436120)CaDiCaL version: 2.1.3
% 95.63/14.50 % (1436120)Termination reason: Instruction limit
% 95.63/14.50 % (1436120)Termination phase: Saturation
% 95.63/14.50 % (1436120)Time elapsed: 0.305 s
% 95.63/14.50 % (1436120)Peak memory usage: 92 MB
% 95.63/14.50 % (1436120)Instructions burned: 667 (million)
% 95.63/14.50 % (1436122)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1829910828:s2a=on:i=185:s2at=1.8:fdi=4_2954 on theBenchmark for (2954ds/185Mi)
% 95.63/14.50 % (1436122)Instruction limit reached!
% 95.63/14.50 % (1436122)------------------------------
% 95.63/14.50 % (1436122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436122)CaDiCaL version: 2.1.3
% 95.63/14.50 % (1436122)Termination reason: Instruction limit
% 95.63/14.50 % (1436122)Termination phase: Saturation
% 95.63/14.50 % (1436122)Time elapsed: 0.097 s
% 95.63/14.50 % (1436122)Peak memory usage: 92 MB
% 95.63/14.50 % (1436122)Instructions burned: 187 (million)
% 95.63/14.50 % (1436124)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3147198387:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2952 on theBenchmark for (2952ds/193Mi)
% 95.63/14.50 % (1436124)Instruction limit reached!
% 95.63/14.50 % (1436124)------------------------------
% 95.63/14.50 % (1436124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436124)CaDiCaL version: 2.1.3
% 95.63/14.50 % (1436124)Termination reason: Instruction limit
% 95.63/14.50 % (1436124)Termination phase: Saturation
% 95.63/14.50 % (1436124)Time elapsed: 0.106 s
% 95.63/14.50 % (1436124)Peak memory usage: 94 MB
% 95.63/14.50 % (1436124)Instructions burned: 194 (million)
% 95.63/14.50 % (1436126)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1312038038:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2950 on theBenchmark for (2950ds/4850Mi)
% 95.63/14.50 % (1436103)Instruction limit reached!
% 95.63/14.50 % (1436103)------------------------------
% 95.63/14.50 % (1436103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436103)CaDiCaL version: 2.1.3
% 95.63/14.50 % (1436103)Termination reason: Instruction limit
% 95.63/14.50 % (1436103)Termination phase: Saturation
% 95.63/14.50 % (1436103)Time elapsed: 4.309 s
% 95.63/14.50 % (1436103)Peak memory usage: 236 MB
% 95.63/14.50 % (1436103)Instructions burned: 13197 (million)
% 95.63/14.50 % (1436128)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2139164046:i=12111:sd=1:ss=included_2943 on theBenchmark for (2943ds/12111Mi)
% 95.63/14.50 % (1436114)Instruction limit reached!
% 95.63/14.50 % (1436114)------------------------------
% 95.63/14.50 % (1436114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.63/14.50 % (1436114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.63/14.50 % (1436114)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436114)Termination reason: Instruction limit
% 134.67/19.92 % (1436114)Termination phase: Saturation
% 134.67/19.92 % (1436114)Time elapsed: 3.782 s
% 134.67/19.92 % (1436114)Peak memory usage: 175 MB
% 134.67/19.92 % (1436114)Instructions burned: 6062 (million)
% 134.67/19.92 % (1436130)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=122663410:i=319:kws=precedence:fsr=off_2937 on theBenchmark for (2937ds/319Mi)
% 134.67/19.92 % (1436130)Instruction limit reached!
% 134.67/19.92 % (1436130)------------------------------
% 134.67/19.92 % (1436130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436130)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436130)Termination reason: Instruction limit
% 134.67/19.92 % (1436130)Termination phase: Saturation
% 134.67/19.92 % (1436130)Time elapsed: 0.177 s
% 134.67/19.92 % (1436130)Peak memory usage: 95 MB
% 134.67/19.92 % (1436130)Instructions burned: 319 (million)
% 134.67/19.92 % (1436132)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4091292345:i=2064:ep=RST_2934 on theBenchmark for (2934ds/2064Mi)
% 134.67/19.92 % (1436132)Instruction limit reached!
% 134.67/19.92 % (1436132)------------------------------
% 134.67/19.92 % (1436132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436132)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436132)Termination reason: Instruction limit
% 134.67/19.92 % (1436132)Termination phase: Saturation
% 134.67/19.92 % (1436132)Time elapsed: 1.106 s
% 134.67/19.92 % (1436132)Peak memory usage: 120 MB
% 134.67/19.92 % (1436132)Instructions burned: 2065 (million)
% 134.67/19.92 % (1436134)dis-1011_128_sil=32000:random_seed=1383370313:i=3706:ep=RST:av=off_2922 on theBenchmark for (2922ds/3706Mi)
% 134.67/19.92 % (1436126)Instruction limit reached!
% 134.67/19.92 % (1436126)------------------------------
% 134.67/19.92 % (1436126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436126)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436126)Termination reason: Instruction limit
% 134.67/19.92 % (1436126)Termination phase: Saturation
% 134.67/19.92 % (1436126)Time elapsed: 2.978 s
% 134.67/19.92 % (1436126)Peak memory usage: 145 MB
% 134.67/19.92 % (1436126)Instructions burned: 4850 (million)
% 134.67/19.92 % (1436136)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1683936838:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2918 on theBenchmark for (2918ds/757Mi)
% 134.67/19.92 % (1436136)Instruction limit reached!
% 134.67/19.92 % (1436136)------------------------------
% 134.67/19.92 % (1436136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436136)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436136)Termination reason: Instruction limit
% 134.67/19.92 % (1436136)Termination phase: Saturation
% 134.67/19.92 % (1436136)Time elapsed: 0.508 s
% 134.67/19.92 % (1436136)Peak memory usage: 109 MB
% 134.67/19.92 % (1436136)Instructions burned: 758 (million)
% 134.67/19.92 % (1436138)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3758891318:i=13913:ss=axioms:sgt=8_2912 on theBenchmark for (2912ds/13913Mi)
% 134.67/19.92 % (1436128)Instruction limit reached!
% 134.67/19.92 % (1436128)------------------------------
% 134.67/19.92 % (1436128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436128)CaDiCaL version: 2.1.3
% 134.67/19.92 % (1436128)Termination reason: Instruction limit
% 134.67/19.92 % (1436128)Termination phase: Saturation
% 134.67/19.92 % (1436128)Time elapsed: 4.035 s
% 134.67/19.92 % (1436128)Peak memory usage: 234 MB
% 134.67/19.92 % (1436128)Instructions burned: 12111 (million)
% 134.67/19.92 % (1436140)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3075291060:i=9925:aac=none_2902 on theBenchmark for (2902ds/9925Mi)
% 134.67/19.92 % (1436134)Instruction limit reached!
% 134.67/19.92 % (1436134)------------------------------
% 134.67/19.92 % (1436134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.67/19.92 % (1436134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.92 % (1436134)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436134)Termination reason: Instruction limit
% 140.66/20.98 % (1436134)Termination phase: Saturation
% 140.66/20.98 % (1436134)Time elapsed: 1.963 s
% 140.66/20.98 % (1436134)Peak memory usage: 121 MB
% 140.66/20.98 % (1436134)Instructions burned: 3707 (million)
% 140.66/20.98 % (1436142)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=98821657:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2901 on theBenchmark for (2901ds/2479Mi)
% 140.66/20.98 % (1436142)Instruction limit reached!
% 140.66/20.98 % (1436142)------------------------------
% 140.66/20.98 % (1436142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436142)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436142)Termination reason: Instruction limit
% 140.66/20.98 % (1436142)Termination phase: Saturation
% 140.66/20.98 % (1436142)Time elapsed: 1.508 s
% 140.66/20.98 % (1436142)Peak memory usage: 109 MB
% 140.66/20.98 % (1436142)Instructions burned: 2479 (million)
% 140.66/20.98 % (1436144)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2146018546:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2885 on theBenchmark for (2885ds/440Mi)
% 140.66/20.98 % (1436118)Instruction limit reached!
% 140.66/20.98 % (1436118)------------------------------
% 140.66/20.98 % (1436118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436118)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436118)Termination reason: Instruction limit
% 140.66/20.98 % (1436118)Termination phase: Saturation
% 140.66/20.98 % (1436118)Time elapsed: 8.919 s
% 140.66/20.98 % (1436118)Peak memory usage: 235 MB
% 140.66/20.98 % (1436118)Instructions burned: 14155 (million)
% 140.66/20.98 % (1436146)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=335502810:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2882 on theBenchmark for (2882ds/11145Mi)
% 140.66/20.98 % (1436144)Instruction limit reached!
% 140.66/20.98 % (1436144)------------------------------
% 140.66/20.98 % (1436144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436144)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436144)Termination reason: Instruction limit
% 140.66/20.98 % (1436144)Termination phase: Saturation
% 140.66/20.98 % (1436144)Time elapsed: 0.249 s
% 140.66/20.98 % (1436144)Peak memory usage: 96 MB
% 140.66/20.98 % (1436144)Instructions burned: 441 (million)
% 140.66/20.98 % (1436148)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4075447460:cts=off:i=3034:av=off:er=known:fsd=on_2881 on theBenchmark for (2881ds/3034Mi)
% 140.66/20.98 % (1436140)Instruction limit reached!
% 140.66/20.98 % (1436140)------------------------------
% 140.66/20.98 % (1436140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436140)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436140)Termination reason: Instruction limit
% 140.66/20.98 % (1436140)Termination phase: Saturation
% 140.66/20.98 % (1436140)Time elapsed: 3.080 s
% 140.66/20.98 % (1436140)Peak memory usage: 209 MB
% 140.66/20.98 % (1436140)Instructions burned: 9928 (million)
% 140.66/20.98 % (1436150)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1316264153:st=2:s2a=on:i=524:s2at=2:ss=axioms_2870 on theBenchmark for (2870ds/524Mi)
% 140.66/20.98 % (1436150)Instruction limit reached!
% 140.66/20.98 % (1436150)------------------------------
% 140.66/20.98 % (1436150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436150)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436150)Termination reason: Instruction limit
% 140.66/20.98 % (1436150)Termination phase: Saturation
% 140.66/20.98 % (1436150)Time elapsed: 0.159 s
% 140.66/20.98 % (1436150)Peak memory usage: 97 MB
% 140.66/20.98 % (1436150)Instructions burned: 525 (million)
% 140.66/20.98 % (1436152)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=740386540:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2868 on theBenchmark for (2868ds/1016Mi)
% 140.66/20.98 % (1436152)Instruction limit reached!
% 140.66/20.98 % (1436152)------------------------------
% 140.66/20.98 % (1436152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436152)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436152)Termination reason: Instruction limit
% 140.66/20.98 % (1436152)Termination phase: Saturation
% 140.66/20.98 % (1436152)Time elapsed: 0.337 s
% 140.66/20.98 % (1436152)Peak memory usage: 120 MB
% 140.66/20.98 % (1436152)Instructions burned: 1019 (million)
% 140.66/20.98 % (1436154)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4260043214:i=14123:bd=preordered:ins=4_2864 on theBenchmark for (2864ds/14123Mi)
% 140.66/20.98 % (1436148)Instruction limit reached!
% 140.66/20.98 % (1436148)------------------------------
% 140.66/20.98 % (1436148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436148)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436148)Termination reason: Instruction limit
% 140.66/20.98 % (1436148)Termination phase: Saturation
% 140.66/20.98 % (1436148)Time elapsed: 1.854 s
% 140.66/20.98 % (1436148)Peak memory usage: 149 MB
% 140.66/20.98 % (1436148)Instructions burned: 3034 (million)
% 140.66/20.98 % (1436156)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1828245669:i=5781:kws=precedence:bd=all:rawr=on_2861 on theBenchmark for (2861ds/5781Mi)
% 140.66/20.98 % (1436156)Instruction limit reached!
% 140.66/20.98 % (1436156)------------------------------
% 140.66/20.98 % (1436156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436156)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436156)Termination reason: Instruction limit
% 140.66/20.98 % (1436156)Termination phase: Saturation
% 140.66/20.98 % (1436156)Time elapsed: 3.298 s
% 140.66/20.98 % (1436156)Peak memory usage: 148 MB
% 140.66/20.98 % (1436156)Instructions burned: 5782 (million)
% 140.66/20.98 % (1436158)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1304972441:i=2448:gtgl=5:bd=preordered:gtg=all_2826 on theBenchmark for (2826ds/2448Mi)
% 140.66/20.98 % (1436138)Instruction limit reached!
% 140.66/20.98 % (1436138)------------------------------
% 140.66/20.98 % (1436138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436138)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436138)Termination reason: Instruction limit
% 140.66/20.98 % (1436138)Termination phase: Saturation
% 140.66/20.98 % (1436138)Time elapsed: 8.622 s
% 140.66/20.98 % (1436138)Peak memory usage: 248 MB
% 140.66/20.98 % (1436138)Instructions burned: 13913 (million)
% 140.66/20.98 % (1436160)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1625243634:i=3223:kws=precedence:fgj=on:av=off_2824 on theBenchmark for (2824ds/3223Mi)
% 140.66/20.98 % (1436154)Instruction limit reached!
% 140.66/20.98 % (1436154)------------------------------
% 140.66/20.98 % (1436154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436154)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436154)Termination reason: Instruction limit
% 140.66/20.98 % (1436154)Termination phase: Saturation
% 140.66/20.98 % (1436154)Time elapsed: 5.045 s
% 140.66/20.98 % (1436154)Peak memory usage: 245 MB
% 140.66/20.98 % (1436154)Instructions burned: 14126 (million)
% 140.66/20.98 % (1436162)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3775073745:st=5.6:i=2033:sd=3:ss=axioms_2812 on theBenchmark for (2812ds/2033Mi)
% 140.66/20.98 % (1436158)Instruction limit reached!
% 140.66/20.98 % (1436158)------------------------------
% 140.66/20.98 % (1436158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436158)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436158)Termination reason: Instruction limit
% 140.66/20.98 % (1436158)Termination phase: Saturation
% 140.66/20.98 % (1436158)Time elapsed: 1.425 s
% 140.66/20.98 % (1436158)Peak memory usage: 147 MB
% 140.66/20.98 % (1436158)Instructions burned: 2448 (million)
% 140.66/20.98 % (1436164)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3243427417:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2811 on theBenchmark for (2811ds/2055Mi)
% 140.66/20.98 % (1436146)Instruction limit reached!
% 140.66/20.98 % (1436146)------------------------------
% 140.66/20.98 % (1436146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436146)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436146)Termination reason: Instruction limit
% 140.66/20.98 % (1436146)Termination phase: Saturation
% 140.66/20.98 % (1436146)Time elapsed: 7.355 s
% 140.66/20.98 % (1436146)Peak memory usage: 212 MB
% 140.66/20.98 % (1436146)Instructions burned: 11146 (million)
% 140.66/20.98 % (1436166)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2596043543:i=21611:sd=3:ss=axioms_2807 on theBenchmark for (2807ds/21611Mi)
% 140.66/20.98 % (1436162)Instruction limit reached!
% 140.66/20.98 % (1436162)------------------------------
% 140.66/20.98 % (1436162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436162)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436162)Termination reason: Instruction limit
% 140.66/20.98 % (1436162)Termination phase: Saturation
% 140.66/20.98 % (1436162)Time elapsed: 0.708 s
% 140.66/20.98 % (1436162)Peak memory usage: 149 MB
% 140.66/20.98 % (1436162)Instructions burned: 2035 (million)
% 140.66/20.98 % (1436168)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4015566199:i=4835:sd=13:ss=axioms:sgt=23_2804 on theBenchmark for (2804ds/4835Mi)
% 140.66/20.98 % (1436160)Instruction limit reached!
% 140.66/20.98 % (1436160)------------------------------
% 140.66/20.98 % (1436160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.98 % (1436160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.98 % (1436160)CaDiCaL version: 2.1.3
% 140.66/20.98 % (1436160)Termination reason: Instruction limit
% 140.66/20.98 % (1436160)Termination phase: Saturation
% 140.66/20.98 % (1436160)Time elapsed: 2.071 s
% 140.66/20.98 % (1436160)Peak memory usage: 152 MB
% 140.66/20.98 % (1436160)Instructions burned: 3224 (million)
% 140.66/20.98 % (1436164)First to succeed.
% 140.66/20.98 % (1436164)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1436057"
% 140.66/20.98 % (1436170)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3776972148:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2802 on theBenchmark for (2802ds/797Mi)
% 140.66/20.98 % (1436164)Refutation found. Thanks to Tanya!
% 140.66/20.98 % SZS status Theorem for theBenchmark
% 140.66/20.98 % SZS output start Proof for theBenchmark
% See solution above
% 142.59/21.07 % (1436164)------------------------------
% 142.59/21.07 % (1436164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.59/21.07 % (1436164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.59/21.07 % (1436164)CaDiCaL version: 2.1.3
% 142.59/21.07 % (1436164)Termination reason: Refutation
% 142.59/21.07 % (1436164)Time elapsed: 0.759 s
% 142.59/21.07 % (1436164)Peak memory usage: 135 MB
% 142.59/21.07 % (1436164)Instructions burned: 1165 (million)
% 142.59/21.07 % (1436164)------------------------------
% 142.59/21.07 % (1436164)------------------------------
% 142.59/21.07 % (1436057)Success in time 20.072 s
% 142.59/21.07 % Vampire exiting
%------------------------------------------------------------------------------