%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU351+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:29 PM UTC 2026
% Result : Theorem 75.40s 13.25s
% Output : Refutation 88.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 55
% Syntax : Number of formulae : 489 ( 45 unt; 45 def)
% Number of atoms : 2377 ( 101 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 3209 (1321 ~;1632 |; 161 &)
% ( 65 <=>; 28 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 63 ( 61 usr; 46 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 497 ( 0 sgn 462 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f56,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
=> below(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_lattice3) ).
fof(f59,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
=> below(X0,X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d17_lattice3) ).
fof(f83,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( X2 = join_of_latt_set(X0,X1)
<=> ( latt_element_smaller(X0,X2,X1)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( latt_element_smaller(X0,X3,X1)
=> below(X0,X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d21_lattice3) ).
fof(f84,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ! [X1] : meet_of_latt_set(X0,X1) = join_of_latt_set(X0,a_2_2_lattice3(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d22_lattice3) ).
fof(f152,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> element(meet_of_latt_set(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k16_lattice3) ).
fof(f312,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X1)
& latt_str(X1) )
=> ( in(X0,a_2_2_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_2_2_lattice3) ).
fof(f313,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& complete_latt_str(X1)
& latt_str(X1) )
=> ( in(X0,a_2_3_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_2_3_lattice3) ).
fof(f395,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0)
& latt_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f551,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( X1 = meet_of_latt_set(X0,X2)
<=> ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( latt_set_smaller(X0,X3,X2)
=> below_refl(X0,X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_lattice3) ).
fof(f552,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( X1 = meet_of_latt_set(X0,X2)
<=> ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( latt_set_smaller(X0,X3,X2)
=> below_refl(X0,X3,X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f551]) ).
fof(f725,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f726,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f725]) ).
fof(f773,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f774,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f773]) ).
fof(f778,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f779,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f778]) ).
fof(f806,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = join_of_latt_set(X0,X1)
<=> ( latt_element_smaller(X0,X2,X1)
& ! [X3] :
( below(X0,X2,X3)
| ~ latt_element_smaller(X0,X3,X1)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f807,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = join_of_latt_set(X0,X1)
<=> ( latt_element_smaller(X0,X2,X1)
& ! [X3] :
( below(X0,X2,X3)
| ~ latt_element_smaller(X0,X3,X1)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f806]) ).
fof(f808,plain,
! [X0] :
( ! [X1] : meet_of_latt_set(X0,X1) = join_of_latt_set(X0,a_2_2_lattice3(X0,X1))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f809,plain,
! [X0] :
( ! [X1] : meet_of_latt_set(X0,X1) = join_of_latt_set(X0,a_2_2_lattice3(X0,X1))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f808]) ).
fof(f887,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f152]) ).
fof(f888,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f887]) ).
fof(f1047,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_2_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) )
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f312]) ).
fof(f1048,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_2_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) )
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f1047]) ).
fof(f1049,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_3_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f313]) ).
fof(f1050,plain,
! [X0,X1,X2] :
( ( in(X0,a_2_3_lattice3(X1,X2))
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) ) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f1049]) ).
fof(f1119,plain,
! [X0,X1,X2] :
( ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f395]) ).
fof(f1120,plain,
! [X0,X1,X2] :
( ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f1119]) ).
fof(f1355,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( X1 = meet_of_latt_set(X0,X2)
<~> ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( below_refl(X0,X3,X1)
| ~ latt_set_smaller(X0,X3,X2)
| ~ element(X3,the_carrier(X0)) ) ) )
& element(X1,the_carrier(X0)) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(ennf_transformation,[],[f552]) ).
fof(f1356,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( X1 = meet_of_latt_set(X0,X2)
<~> ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( below_refl(X0,X3,X1)
| ~ latt_set_smaller(X0,X3,X2)
| ~ element(X3,the_carrier(X0)) ) ) )
& element(X1,the_carrier(X0)) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(flattening,[],[f1355]) ).
fof(f1540,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X1,X3)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f774]) ).
fof(f1541,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X1,X3)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X1,X4)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f1540]) ).
fof(f1542,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ( ~ below(X0,X1,sK39(X0,X1,X2))
& in(sK39(X0,X1,X2),X2)
& element(sK39(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X1,X4)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X3,sK39(X0,X1,X2))],[f1541]) ).
fof(f1547,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X3,X1)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f779]) ).
fof(f1548,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X3,X1)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X4,X1)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f1547]) ).
fof(f1549,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ( ~ below(X0,sK41(X0,X1,X2),X1)
& in(sK41(X0,X1,X2),X2)
& element(sK41(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X4,X1)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X3,sK41(X0,X1,X2))],[f1548]) ).
fof(f1604,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ? [X3] :
( ~ below(X0,X2,X3)
& latt_element_smaller(X0,X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ( latt_element_smaller(X0,X2,X1)
& ! [X3] :
( below(X0,X2,X3)
| ~ latt_element_smaller(X0,X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| join_of_latt_set(X0,X1) != X2 ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f807]) ).
fof(f1605,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ? [X3] :
( ~ below(X0,X2,X3)
& latt_element_smaller(X0,X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ( latt_element_smaller(X0,X2,X1)
& ! [X3] :
( below(X0,X2,X3)
| ~ latt_element_smaller(X0,X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| join_of_latt_set(X0,X1) != X2 ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f1604]) ).
fof(f1606,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ? [X3] :
( ~ below(X0,X2,X3)
& latt_element_smaller(X0,X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ( latt_element_smaller(X0,X2,X1)
& ! [X4] :
( below(X0,X2,X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0)) ) )
| join_of_latt_set(X0,X1) != X2 ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f1605]) ).
fof(f1607,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ( ~ below(X0,X2,sK68(X0,X1,X2))
& latt_element_smaller(X0,sK68(X0,X1,X2),X1)
& element(sK68(X0,X1,X2),the_carrier(X0)) ) )
& ( ( latt_element_smaller(X0,X2,X1)
& ! [X4] :
( below(X0,X2,X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0)) ) )
| join_of_latt_set(X0,X1) != X2 ) )
| ~ element(X2,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X3,sK68(X0,X1,X2))],[f1606]) ).
fof(f1746,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_2_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) )
| ~ in(X0,a_2_2_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f1048]) ).
fof(f1747,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_2_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ? [X4] :
( element(X4,the_carrier(X1))
& X0 = X4
& latt_set_smaller(X1,X4,X2) )
| ~ in(X0,a_2_2_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(rectify,[],[f1746]) ).
fof(f1748,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_2_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ( element(sK144(X0,X1,X2),the_carrier(X1))
& sK144(X0,X1,X2) = X0
& latt_set_smaller(X1,sK144(X0,X1,X2),X2) )
| ~ in(X0,a_2_2_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK144]),skolemize(X4,sK144(X0,X1,X2))],[f1747]) ).
fof(f1749,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_3_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& X0 = X3
& latt_set_smaller(X1,X3,X2) )
| ~ in(X0,a_2_3_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f1050]) ).
fof(f1750,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_3_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ? [X4] :
( element(X4,the_carrier(X1))
& X0 = X4
& latt_set_smaller(X1,X4,X2) )
| ~ in(X0,a_2_3_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(rectify,[],[f1749]) ).
fof(f1751,plain,
! [X0,X1,X2] :
( ( ( in(X0,a_2_3_lattice3(X1,X2))
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2) ) )
& ( ( element(sK145(X0,X1,X2),the_carrier(X1))
& sK145(X0,X1,X2) = X0
& latt_set_smaller(X1,sK145(X0,X1,X2),X2) )
| ~ in(X0,a_2_3_lattice3(X1,X2)) ) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK145]),skolemize(X4,sK145(X0,X1,X2))],[f1750]) ).
fof(f1813,plain,
! [X0,X1,X2] :
( ( ( below_refl(X0,X1,X2)
| ~ below(X0,X1,X2) )
& ( below(X0,X1,X2)
| ~ below_refl(X0,X1,X2) ) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(nnf_transformation,[],[f1120]) ).
fof(f2038,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below_refl(X0,X3,X1)
& latt_set_smaller(X0,X3,X2)
& element(X3,the_carrier(X0)) )
| meet_of_latt_set(X0,X2) != X1 )
& ( ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( below_refl(X0,X3,X1)
| ~ latt_set_smaller(X0,X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| X1 = meet_of_latt_set(X0,X2) ) )
& element(X1,the_carrier(X0)) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(nnf_transformation,[],[f1356]) ).
fof(f2039,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below_refl(X0,X3,X1)
& latt_set_smaller(X0,X3,X2)
& element(X3,the_carrier(X0)) )
| meet_of_latt_set(X0,X2) != X1 )
& ( ( latt_set_smaller(X0,X1,X2)
& ! [X3] :
( below_refl(X0,X3,X1)
| ~ latt_set_smaller(X0,X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| X1 = meet_of_latt_set(X0,X2) ) )
& element(X1,the_carrier(X0)) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(flattening,[],[f2038]) ).
fof(f2040,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below_refl(X0,X3,X1)
& latt_set_smaller(X0,X3,X2)
& element(X3,the_carrier(X0)) )
| meet_of_latt_set(X0,X2) != X1 )
& ( ( latt_set_smaller(X0,X1,X2)
& ! [X4] :
( below_refl(X0,X4,X1)
| ~ latt_set_smaller(X0,X4,X2)
| ~ element(X4,the_carrier(X0)) ) )
| X1 = meet_of_latt_set(X0,X2) ) )
& element(X1,the_carrier(X0)) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(rectify,[],[f2039]) ).
fof(f2041,plain,
( ( ~ latt_set_smaller(sK449,sK450,sK451)
| ( ~ below_refl(sK449,sK452,sK450)
& latt_set_smaller(sK449,sK452,sK451)
& element(sK452,the_carrier(sK449)) )
| sK450 != meet_of_latt_set(sK449,sK451) )
& ( ( latt_set_smaller(sK449,sK450,sK451)
& ! [X4] :
( below_refl(sK449,X4,sK450)
| ~ latt_set_smaller(sK449,X4,sK451)
| ~ element(X4,the_carrier(sK449)) ) )
| sK450 = meet_of_latt_set(sK449,sK451) )
& element(sK450,the_carrier(sK449))
& ~ empty_carrier(sK449)
& lattice(sK449)
& complete_latt_str(sK449)
& latt_str(sK449) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK449,sK450,sK451,sK452]),skolemize(X0,sK449),skolemize(X1,sK450),skolemize(X2,sK451),skolemize(X3,sK452)],[f2040]) ).
fof(f2115,plain,
! [X0] :
( join_absorbing(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f726]) ).
fof(f2116,plain,
! [X0] :
( meet_absorbing(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f726]) ).
fof(f2118,plain,
! [X0] :
( meet_commutative(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f726]) ).
fof(f2229,plain,
! [X2,X0,X1,X4] :
( below(X0,X1,X4)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0))
| ~ latt_set_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1542]) ).
fof(f2230,plain,
! [X2,X0,X1] :
( latt_set_smaller(X0,X1,X2)
| element(sK39(X0,X1,X2),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1542]) ).
fof(f2231,plain,
! [X2,X0,X1] :
( latt_set_smaller(X0,X1,X2)
| in(sK39(X0,X1,X2),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1542]) ).
fof(f2232,plain,
! [X2,X0,X1] :
( latt_set_smaller(X0,X1,X2)
| ~ below(X0,X1,sK39(X0,X1,X2))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1542]) ).
fof(f2239,plain,
! [X2,X0,X1,X4] :
( below(X0,X4,X1)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0))
| ~ latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1549]) ).
fof(f2240,plain,
! [X2,X0,X1] :
( latt_element_smaller(X0,X1,X2)
| element(sK41(X0,X1,X2),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1549]) ).
fof(f2241,plain,
! [X2,X0,X1] :
( latt_element_smaller(X0,X1,X2)
| in(sK41(X0,X1,X2),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1549]) ).
fof(f2242,plain,
! [X2,X0,X1] :
( latt_element_smaller(X0,X1,X2)
| ~ below(X0,sK41(X0,X1,X2),X1)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1549]) ).
fof(f2344,plain,
! [X2,X0,X1,X4] :
( below(X0,X2,X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0))
| join_of_latt_set(X0,X1) != X2
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1607]) ).
fof(f2345,plain,
! [X2,X0,X1] :
( latt_element_smaller(X0,X2,X1)
| join_of_latt_set(X0,X1) != X2
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1607]) ).
fof(f2346,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| element(sK68(X0,X1,X2),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1607]) ).
fof(f2347,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| latt_element_smaller(X0,sK68(X0,X1,X2),X1)
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1607]) ).
fof(f2348,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| ~ below(X0,X2,sK68(X0,X1,X2))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1607]) ).
fof(f2349,plain,
! [X0,X1] :
( meet_of_latt_set(X0,X1) = join_of_latt_set(X0,a_2_2_lattice3(X0,X1))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f2591,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f888]) ).
fof(f2855,plain,
! [X2,X0,X1] :
( latt_set_smaller(X1,sK144(X0,X1,X2),X2)
| ~ in(X0,a_2_2_lattice3(X1,X2))
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1748]) ).
fof(f2856,plain,
! [X2,X0,X1] :
( sK144(X0,X1,X2) = X0
| ~ in(X0,a_2_2_lattice3(X1,X2))
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1748]) ).
fof(f2857,plain,
! [X2,X0,X1] :
( element(sK144(X0,X1,X2),the_carrier(X1))
| ~ in(X0,a_2_2_lattice3(X1,X2))
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1748]) ).
fof(f2858,plain,
! [X2,X3,X0,X1] :
( in(X0,a_2_2_lattice3(X1,X2))
| ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2)
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1748]) ).
fof(f2859,plain,
! [X2,X0,X1] :
( latt_set_smaller(X1,sK145(X0,X1,X2),X2)
| ~ in(X0,a_2_3_lattice3(X1,X2))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1751]) ).
fof(f2860,plain,
! [X2,X0,X1] :
( sK145(X0,X1,X2) = X0
| ~ in(X0,a_2_3_lattice3(X1,X2))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1751]) ).
fof(f2861,plain,
! [X2,X0,X1] :
( element(sK145(X0,X1,X2),the_carrier(X1))
| ~ in(X0,a_2_3_lattice3(X1,X2))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1751]) ).
fof(f2862,plain,
! [X2,X3,X0,X1] :
( in(X0,a_2_3_lattice3(X1,X2))
| ~ element(X3,the_carrier(X1))
| X0 != X3
| ~ latt_set_smaller(X1,X3,X2)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1751]) ).
fof(f3057,plain,
! [X2,X0,X1] :
( below(X0,X1,X2)
| ~ below_refl(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f1813]) ).
fof(f3058,plain,
! [X2,X0,X1] :
( below_refl(X0,X1,X2)
| ~ below(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f1813]) ).
fof(f3852,plain,
latt_str(sK449),
inference(cnf_transformation,[],[f2041]) ).
fof(f3853,plain,
complete_latt_str(sK449),
inference(cnf_transformation,[],[f2041]) ).
fof(f3854,plain,
lattice(sK449),
inference(cnf_transformation,[],[f2041]) ).
fof(f3855,plain,
~ empty_carrier(sK449),
inference(cnf_transformation,[],[f2041]) ).
fof(f3856,plain,
element(sK450,the_carrier(sK449)),
inference(cnf_transformation,[],[f2041]) ).
fof(f3857,plain,
! [X4] :
( below_refl(sK449,X4,sK450)
| ~ latt_set_smaller(sK449,X4,sK451)
| ~ element(X4,the_carrier(sK449))
| sK450 = meet_of_latt_set(sK449,sK451) ),
inference(cnf_transformation,[],[f2041]) ).
fof(f3858,plain,
( latt_set_smaller(sK449,sK450,sK451)
| sK450 = meet_of_latt_set(sK449,sK451) ),
inference(cnf_transformation,[],[f2041]) ).
fof(f3859,plain,
( ~ latt_set_smaller(sK449,sK450,sK451)
| element(sK452,the_carrier(sK449))
| sK450 != meet_of_latt_set(sK449,sK451) ),
inference(cnf_transformation,[],[f2041]) ).
fof(f3860,plain,
( ~ latt_set_smaller(sK449,sK450,sK451)
| latt_set_smaller(sK449,sK452,sK451)
| sK450 != meet_of_latt_set(sK449,sK451) ),
inference(cnf_transformation,[],[f2041]) ).
fof(f3861,plain,
( ~ latt_set_smaller(sK449,sK450,sK451)
| ~ below_refl(sK449,sK452,sK450)
| sK450 != meet_of_latt_set(sK449,sK451) ),
inference(cnf_transformation,[],[f2041]) ).
fof(f4553,plain,
! [X0,X1] :
( latt_element_smaller(X0,join_of_latt_set(X0,X1),X1)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(equality_resolution,[],[f2345]) ).
fof(f4554,plain,
! [X0,X1,X4] :
( below(X0,join_of_latt_set(X0,X1),X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0))
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(equality_resolution,[],[f2344]) ).
fof(f4609,plain,
! [X2,X3,X1] :
( in(X3,a_2_2_lattice3(X1,X2))
| ~ element(X3,the_carrier(X1))
| ~ latt_set_smaller(X1,X3,X2)
| empty_carrier(X1)
| ~ latt_str(X1) ),
inference(equality_resolution,[],[f2858]) ).
fof(f4610,plain,
! [X2,X3,X1] :
( in(X3,a_2_3_lattice3(X1,X2))
| ~ element(X3,the_carrier(X1))
| ~ latt_set_smaller(X1,X3,X2)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(equality_resolution,[],[f2862]) ).
fof(f5070,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| ~ below(X0,X2,sK68(X0,X1,X2))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f2348]) ).
fof(f5071,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| latt_element_smaller(X0,sK68(X0,X1,X2),X1)
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f2347]) ).
fof(f5072,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| element(sK68(X0,X1,X2),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f2346]) ).
fof(f5073,plain,
! [X0,X1] :
( latt_element_smaller(X0,join_of_latt_set(X0,X1),X1)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f4553]) ).
fof(f5074,plain,
! [X0,X1,X4] :
( below(X0,join_of_latt_set(X0,X1),X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0))
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f4554]) ).
fof(f5313,definition,
( spl588_1
<=> sK450 = meet_of_latt_set(sK449,sK451) ),
introduced(definition,[new_symbols(definition,[spl588_1])],[avatar_definition]) ).
fof(f5314,plain,
( sK450 = meet_of_latt_set(sK449,sK451)
| ~ spl588_1 ),
inference(avatar_component_clause,[],[f5313]) ).
fof(f5315,plain,
( sK450 != meet_of_latt_set(sK449,sK451)
| spl588_1 ),
inference(avatar_component_clause,[],[f5313]) ).
fof(f5317,definition,
( spl588_2
<=> below_refl(sK449,sK452,sK450) ),
introduced(definition,[new_symbols(definition,[spl588_2])],[avatar_definition]) ).
fof(f5319,plain,
( ~ below_refl(sK449,sK452,sK450)
| spl588_2 ),
inference(avatar_component_clause,[],[f5317]) ).
fof(f5321,definition,
( spl588_3
<=> latt_set_smaller(sK449,sK450,sK451) ),
introduced(definition,[new_symbols(definition,[spl588_3])],[avatar_definition]) ).
fof(f5322,plain,
( latt_set_smaller(sK449,sK450,sK451)
| ~ spl588_3 ),
inference(avatar_component_clause,[],[f5321]) ).
fof(f5323,plain,
( ~ latt_set_smaller(sK449,sK450,sK451)
| spl588_3 ),
inference(avatar_component_clause,[],[f5321]) ).
fof(f5324,plain,
( ~ spl588_1
| ~ spl588_2
| ~ spl588_3 ),
inference(avatar_split_clause,[],[f3861,f5321,f5317,f5313]) ).
fof(f5325,plain,
( latt_set_smaller(sK449,sK450,sK451)
| spl588_1 ),
inference(backward_subsumption_resolution,[],[f3858,f5315]) ).
fof(f5326,plain,
( ! [X4] :
( below_refl(sK449,X4,sK450)
| ~ latt_set_smaller(sK449,X4,sK451)
| ~ element(X4,the_carrier(sK449)) )
| spl588_1 ),
inference(backward_subsumption_resolution,[],[f3857,f5315]) ).
fof(f5329,plain,
( spl588_3
| spl588_1 ),
inference(avatar_split_clause,[],[f5325,f5313,f5321]) ).
fof(f5345,definition,
( spl588_4
<=> empty_carrier(sK449) ),
introduced(definition,[new_symbols(definition,[spl588_4])],[avatar_definition]) ).
fof(f5347,plain,
( ~ empty_carrier(sK449)
| spl588_4 ),
inference(avatar_component_clause,[],[f5345]) ).
fof(f5348,plain,
~ spl588_4,
inference(avatar_split_clause,[],[f3855,f5345]) ).
fof(f5349,plain,
( join_absorbing(sK449)
| ~ lattice(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(resolution,[],[f5347,f2115]) ).
fof(f5350,plain,
( meet_absorbing(sK449)
| ~ lattice(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(resolution,[],[f5347,f2116]) ).
fof(f5352,plain,
( meet_commutative(sK449)
| ~ lattice(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(resolution,[],[f5347,f2118]) ).
fof(f5372,plain,
( ! [X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ below(sK449,sK41(sK449,X0,X1),X0)
| ~ element(X0,the_carrier(sK449))
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f2242]) ).
fof(f5377,plain,
( ! [X0] :
( meet_of_latt_set(sK449,X0) = join_of_latt_set(sK449,a_2_2_lattice3(sK449,X0))
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f2349]) ).
fof(f5447,plain,
( ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f2859]) ).
fof(f5448,plain,
( ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f2860]) ).
fof(f5449,plain,
( ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f2861]) ).
fof(f5465,plain,
( ! [X0,X1] :
( in(X0,a_2_2_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f4609]) ).
fof(f5466,plain,
( ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(resolution,[],[f5347,f4610]) ).
fof(f5481,plain,
( ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5466,f3854]) ).
fof(f5482,plain,
( ! [X0,X1] :
( in(X0,a_2_2_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5465,f3852]) ).
fof(f5487,plain,
( ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5449,f3854]) ).
fof(f5488,plain,
( ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5448,f3854]) ).
fof(f5489,plain,
( ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5447,f3854]) ).
fof(f5531,plain,
( ! [X0] : meet_of_latt_set(sK449,X0) = join_of_latt_set(sK449,a_2_2_lattice3(sK449,X0))
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5377,f3852]) ).
fof(f5533,plain,
( ! [X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ below(sK449,sK41(sK449,X0,X1),X0)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5372,f3852]) ).
fof(f5543,plain,
( meet_commutative(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5352,f3854]) ).
fof(f5545,plain,
( meet_absorbing(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5350,f3854]) ).
fof(f5546,plain,
( join_absorbing(sK449)
| ~ latt_str(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5349,f3854]) ).
fof(f5553,plain,
( ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1)
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5481,f3853]) ).
fof(f5556,plain,
( ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5487,f3853]) ).
fof(f5557,plain,
( ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5488,f3853]) ).
fof(f5558,plain,
( ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1))
| ~ latt_str(sK449) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5489,f3853]) ).
fof(f5589,plain,
( meet_commutative(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5543,f3852]) ).
fof(f5591,plain,
( meet_absorbing(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5545,f3852]) ).
fof(f5592,plain,
( join_absorbing(sK449)
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5546,f3852]) ).
fof(f5598,plain,
( ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5553,f3852]) ).
fof(f5599,plain,
( ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5556,f3852]) ).
fof(f5600,plain,
( ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5557,f3852]) ).
fof(f5601,plain,
( ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| spl588_4 ),
inference(forward_subsumption_resolution,[],[f5558,f3852]) ).
fof(f5703,definition,
( spl588_6
<=> latt_str(sK449) ),
introduced(definition,[new_symbols(definition,[spl588_6])],[avatar_definition]) ).
fof(f5705,plain,
( latt_str(sK449)
| ~ spl588_6 ),
inference(avatar_component_clause,[],[f5703]) ).
fof(f5706,plain,
spl588_6,
inference(avatar_split_clause,[],[f3852,f5703]) ).
fof(f5708,definition,
( spl588_7
<=> complete_latt_str(sK449) ),
introduced(definition,[new_symbols(definition,[spl588_7])],[avatar_definition]) ).
fof(f5710,plain,
( complete_latt_str(sK449)
| ~ spl588_7 ),
inference(avatar_component_clause,[],[f5708]) ).
fof(f5711,plain,
spl588_7,
inference(avatar_split_clause,[],[f3853,f5708]) ).
fof(f5713,definition,
( spl588_8
<=> ! [X4] :
( below_refl(sK449,X4,sK450)
| ~ latt_set_smaller(sK449,X4,sK451)
| ~ element(X4,the_carrier(sK449)) ) ),
introduced(definition,[new_symbols(definition,[spl588_8])],[avatar_definition]) ).
fof(f5714,plain,
( ! [X4] :
( ~ latt_set_smaller(sK449,X4,sK451)
| below_refl(sK449,X4,sK450)
| ~ element(X4,the_carrier(sK449)) )
| ~ spl588_8 ),
inference(avatar_component_clause,[],[f5713]) ).
fof(f5715,plain,
( spl588_8
| spl588_1 ),
inference(avatar_split_clause,[],[f5326,f5313,f5713]) ).
fof(f5720,plain,
( ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ element(sK144(X0,sK449,sK451),the_carrier(sK449))
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_8 ),
inference(resolution,[],[f5714,f2855]) ).
fof(f5726,plain,
( ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_8 ),
inference(forward_subsumption_resolution,[],[f5720,f2857]) ).
fof(f5731,plain,
( ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_8 ),
inference(forward_subsumption_resolution,[],[f5726,f5347]) ).
fof(f5736,plain,
( ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451)) )
| spl588_4
| ~ spl588_6
| ~ spl588_8 ),
inference(forward_subsumption_resolution,[],[f5731,f5705]) ).
fof(f5744,definition,
( spl588_10
<=> lattice(sK449) ),
introduced(definition,[new_symbols(definition,[spl588_10])],[avatar_definition]) ).
fof(f5746,plain,
( lattice(sK449)
| ~ spl588_10 ),
inference(avatar_component_clause,[],[f5744]) ).
fof(f5747,plain,
spl588_10,
inference(avatar_split_clause,[],[f3854,f5744]) ).
fof(f5749,definition,
( spl588_11
<=> element(sK450,the_carrier(sK449)) ),
introduced(definition,[new_symbols(definition,[spl588_11])],[avatar_definition]) ).
fof(f5751,plain,
( element(sK450,the_carrier(sK449))
| ~ spl588_11 ),
inference(avatar_component_clause,[],[f5749]) ).
fof(f5752,plain,
spl588_11,
inference(avatar_split_clause,[],[f3856,f5749]) ).
fof(f5769,plain,
( ! [X0,X1] :
( below(sK449,X0,sK450)
| ~ in(X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ latt_element_smaller(sK449,sK450,X1)
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_11 ),
inference(resolution,[],[f5751,f2239]) ).
fof(f5770,plain,
( ! [X0,X1] :
( below(sK449,sK450,X0)
| ~ in(sK450,X1)
| ~ latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_11 ),
inference(resolution,[],[f5751,f2239]) ).
fof(f5772,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| in(sK41(sK449,sK450,X0),X0)
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_11 ),
inference(resolution,[],[f5751,f2241]) ).
fof(f5773,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below(sK449,sK41(sK449,sK450,X0),sK450)
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_11 ),
inference(resolution,[],[f5751,f2242]) ).
fof(f5816,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| empty_carrier(sK449)
| ~ meet_commutative(sK449)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(X0,the_carrier(sK449)) )
| ~ spl588_11 ),
inference(resolution,[],[f5751,f3058]) ).
fof(f5866,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ meet_commutative(sK449)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5816,f5347]) ).
fof(f5899,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below(sK449,sK41(sK449,sK450,X0),sK450)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5773,f5347]) ).
fof(f5900,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| in(sK41(sK449,sK450,X0),X0)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5772,f5347]) ).
fof(f5902,plain,
( ! [X0,X1] :
( below(sK449,sK450,X0)
| ~ in(sK450,X1)
| ~ latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5770,f5347]) ).
fof(f5903,plain,
( ! [X0,X1] :
( below(sK449,X0,sK450)
| ~ in(X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ latt_element_smaller(sK449,sK450,X1)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5769,f5347]) ).
fof(f5931,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5866,f5589]) ).
fof(f5949,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below(sK449,sK41(sK449,sK450,X0),sK450) )
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5899,f5705]) ).
fof(f5950,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| in(sK41(sK449,sK450,X0),X0) )
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5900,f5705]) ).
fof(f5952,plain,
( ! [X0,X1] :
( below(sK449,sK450,X0)
| ~ in(sK450,X1)
| ~ latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5902,f5705]) ).
fof(f5953,plain,
( ! [X0,X1] :
( below(sK449,X0,sK450)
| ~ in(X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ latt_element_smaller(sK449,sK450,X1) )
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5903,f5705]) ).
fof(f5971,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5931,f5591]) ).
fof(f5988,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ latt_str(sK449)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5971,f5592]) ).
fof(f5993,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ element(X0,the_carrier(sK449)) )
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f5988,f5705]) ).
fof(f6302,plain,
( element(sK452,the_carrier(sK449))
| sK450 != meet_of_latt_set(sK449,sK451)
| ~ spl588_3 ),
inference(forward_subsumption_resolution,[],[f3859,f5322]) ).
fof(f6303,plain,
( latt_set_smaller(sK449,sK452,sK451)
| sK450 != meet_of_latt_set(sK449,sK451)
| ~ spl588_3 ),
inference(forward_subsumption_resolution,[],[f3860,f5322]) ).
fof(f6304,plain,
( element(sK452,the_carrier(sK449))
| ~ spl588_1
| ~ spl588_3 ),
inference(forward_subsumption_resolution,[],[f6302,f5314]) ).
fof(f6305,plain,
( latt_set_smaller(sK449,sK452,sK451)
| ~ spl588_1
| ~ spl588_3 ),
inference(forward_subsumption_resolution,[],[f6303,f5314]) ).
fof(f6315,definition,
( spl588_14
<=> latt_set_smaller(sK449,sK452,sK451) ),
introduced(definition,[new_symbols(definition,[spl588_14])],[avatar_definition]) ).
fof(f6317,plain,
( latt_set_smaller(sK449,sK452,sK451)
| ~ spl588_14 ),
inference(avatar_component_clause,[],[f6315]) ).
fof(f6318,plain,
( spl588_14
| ~ spl588_1
| ~ spl588_3 ),
inference(avatar_split_clause,[],[f6305,f5321,f5313,f6315]) ).
fof(f6323,plain,
( in(sK39(sK449,sK450,sK451),sK451)
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3 ),
inference(resolution,[],[f5323,f2231]) ).
fof(f6326,plain,
( in(sK39(sK449,sK450,sK451),sK451)
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6323,f5751]) ).
fof(f6329,plain,
( in(sK39(sK449,sK450,sK451),sK451)
| ~ latt_str(sK449)
| spl588_3
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6326,f5347]) ).
fof(f6332,plain,
( in(sK39(sK449,sK450,sK451),sK451)
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6329,f5705]) ).
fof(f6346,definition,
( spl588_15
<=> in(sK39(sK449,sK450,sK451),sK451) ),
introduced(definition,[new_symbols(definition,[spl588_15])],[avatar_definition]) ).
fof(f6348,plain,
( in(sK39(sK449,sK450,sK451),sK451)
| ~ spl588_15 ),
inference(avatar_component_clause,[],[f6346]) ).
fof(f6349,plain,
( spl588_15
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f6332,f5749,f5703,f5345,f5321,f6346]) ).
fof(f6375,definition,
( spl588_16
<=> element(sK452,the_carrier(sK449)) ),
introduced(definition,[new_symbols(definition,[spl588_16])],[avatar_definition]) ).
fof(f6377,plain,
( element(sK452,the_carrier(sK449))
| ~ spl588_16 ),
inference(avatar_component_clause,[],[f6375]) ).
fof(f6378,plain,
( spl588_16
| ~ spl588_1
| ~ spl588_3 ),
inference(avatar_split_clause,[],[f6304,f5321,f5313,f6375]) ).
fof(f6387,plain,
( element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3 ),
inference(resolution,[],[f5323,f2230]) ).
fof(f6391,plain,
( element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6387,f5751]) ).
fof(f6393,plain,
( element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| ~ latt_str(sK449)
| spl588_3
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6391,f5347]) ).
fof(f6395,plain,
( element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6393,f5705]) ).
fof(f6408,definition,
( spl588_17
<=> element(sK39(sK449,sK450,sK451),the_carrier(sK449)) ),
introduced(definition,[new_symbols(definition,[spl588_17])],[avatar_definition]) ).
fof(f6410,plain,
( element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| ~ spl588_17 ),
inference(avatar_component_clause,[],[f6408]) ).
fof(f6411,plain,
( spl588_17
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f6395,f5749,f5703,f5345,f5321,f6408]) ).
fof(f6417,plain,
( in(sK450,a_2_2_lattice3(sK449,sK451))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| ~ spl588_3 ),
inference(resolution,[],[f5322,f4609]) ).
fof(f6420,plain,
( in(sK450,a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| ~ spl588_3
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6417,f5751]) ).
fof(f6422,plain,
( in(sK450,a_2_2_lattice3(sK449,sK451))
| ~ latt_str(sK449)
| ~ spl588_3
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6420,f5347]) ).
fof(f6424,plain,
( in(sK450,a_2_2_lattice3(sK449,sK451))
| ~ spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f6422,f5705]) ).
fof(f6709,plain,
( below_refl(sK449,sK452,sK450)
| ~ element(sK452,the_carrier(sK449))
| ~ spl588_8
| ~ spl588_14 ),
inference(resolution,[],[f5714,f6317]) ).
fof(f6723,plain,
( ~ element(sK452,the_carrier(sK449))
| spl588_2
| ~ spl588_8
| ~ spl588_14 ),
inference(forward_subsumption_resolution,[],[f6709,f5319]) ).
fof(f6726,plain,
( $false
| spl588_2
| ~ spl588_8
| ~ spl588_14
| ~ spl588_16 ),
inference(forward_subsumption_resolution,[],[f6723,f6377]) ).
fof(f6727,plain,
( spl588_2
| ~ spl588_8
| ~ spl588_14
| ~ spl588_16 ),
inference(avatar_contradiction_clause,[],[f6726]) ).
fof(f7161,definition,
( spl588_20
<=> ! [X0] : meet_of_latt_set(sK449,X0) = join_of_latt_set(sK449,a_2_2_lattice3(sK449,X0)) ),
introduced(definition,[new_symbols(definition,[spl588_20])],[avatar_definition]) ).
fof(f7162,plain,
( ! [X0] : meet_of_latt_set(sK449,X0) = join_of_latt_set(sK449,a_2_2_lattice3(sK449,X0))
| ~ spl588_20 ),
inference(avatar_component_clause,[],[f7161]) ).
fof(f7163,plain,
( spl588_20
| spl588_4 ),
inference(avatar_split_clause,[],[f5531,f5345,f7161]) ).
fof(f7172,plain,
( ! [X0] :
( ~ element(meet_of_latt_set(sK449,X0),the_carrier(sK449))
| latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| ~ spl588_20 ),
inference(superposition,[],[f5073,f7162]) ).
fof(f7174,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449))
| ~ element(meet_of_latt_set(sK449,X0),the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| ~ spl588_20 ),
inference(superposition,[],[f5074,f7162]) ).
fof(f7175,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7174,f2591]) ).
fof(f7177,plain,
( ! [X0] :
( latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7172,f2591]) ).
fof(f7185,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7175,f5347]) ).
fof(f7187,plain,
( ! [X0] :
( latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7177,f5347]) ).
fof(f7195,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7185,f5746]) ).
fof(f7197,plain,
( ! [X0] :
( latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7187,f5746]) ).
fof(f7205,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449))
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7195,f5710]) ).
fof(f7207,plain,
( ! [X0] :
( latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7197,f5710]) ).
fof(f7215,plain,
( ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449)) )
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7205,f5705]) ).
fof(f7217,plain,
( ! [X0] : latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(forward_subsumption_resolution,[],[f7207,f5705]) ).
fof(f7275,definition,
( spl588_23
<=> in(sK450,a_2_2_lattice3(sK449,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_23])],[avatar_definition]) ).
fof(f7277,plain,
( in(sK450,a_2_2_lattice3(sK449,sK451))
| ~ spl588_23 ),
inference(avatar_component_clause,[],[f7275]) ).
fof(f7278,plain,
( spl588_23
| ~ spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f6424,f5749,f5703,f5345,f5321,f7275]) ).
fof(f7356,definition,
( spl588_24
<=> ! [X0] :
( below_refl(sK449,sK145(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) ) ),
introduced(definition,[new_symbols(definition,[spl588_24])],[avatar_definition]) ).
fof(f7357,plain,
( ! [X0] :
( below_refl(sK449,sK145(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_24 ),
inference(avatar_component_clause,[],[f7356]) ).
fof(f7381,definition,
( spl588_25
<=> ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) ) ),
introduced(definition,[new_symbols(definition,[spl588_25])],[avatar_definition]) ).
fof(f7382,plain,
( ! [X0] :
( ~ in(X0,a_2_3_lattice3(sK449,sK451))
| below_refl(sK449,X0,sK450) )
| ~ spl588_25 ),
inference(avatar_component_clause,[],[f7381]) ).
fof(f7647,definition,
( spl588_28
<=> ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ below(sK449,X0,sK450)
| ~ element(X0,the_carrier(sK449)) ) ),
introduced(definition,[new_symbols(definition,[spl588_28])],[avatar_definition]) ).
fof(f7648,plain,
( ! [X0] :
( ~ below(sK449,X0,sK450)
| below_refl(sK449,X0,sK450)
| ~ element(X0,the_carrier(sK449)) )
| ~ spl588_28 ),
inference(avatar_component_clause,[],[f7647]) ).
fof(f7649,plain,
( spl588_28
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f5993,f5749,f5703,f5345,f7647]) ).
fof(f8300,definition,
( spl588_34
<=> ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451)) ) ),
introduced(definition,[new_symbols(definition,[spl588_34])],[avatar_definition]) ).
fof(f8301,plain,
( ! [X0] :
( below_refl(sK449,sK144(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451)) )
| ~ spl588_34 ),
inference(avatar_component_clause,[],[f8300]) ).
fof(f8302,plain,
( spl588_34
| spl588_4
| ~ spl588_6
| ~ spl588_8 ),
inference(avatar_split_clause,[],[f5736,f5713,f5703,f5345,f8300]) ).
fof(f8305,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_34 ),
inference(superposition,[],[f8301,f2856]) ).
fof(f8307,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_34 ),
inference(duplicate_literal_removal,[],[f8305]) ).
fof(f8308,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_34 ),
inference(forward_subsumption_resolution,[],[f8307,f5347]) ).
fof(f8311,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451)) )
| spl588_4
| ~ spl588_6
| ~ spl588_34 ),
inference(forward_subsumption_resolution,[],[f8308,f5705]) ).
fof(f9048,definition,
( spl588_53
<=> ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_2_lattice3(sK449,sK451)) ) ),
introduced(definition,[new_symbols(definition,[spl588_53])],[avatar_definition]) ).
fof(f9049,plain,
( ! [X0] :
( ~ in(X0,a_2_2_lattice3(sK449,sK451))
| below_refl(sK449,X0,sK450) )
| ~ spl588_53 ),
inference(avatar_component_clause,[],[f9048]) ).
fof(f9050,plain,
( spl588_53
| spl588_4
| ~ spl588_6
| ~ spl588_34 ),
inference(avatar_split_clause,[],[f8311,f8300,f5703,f5345,f9048]) ).
fof(f9365,definition,
( spl588_58
<=> ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl588_58])],[avatar_definition]) ).
fof(f9366,plain,
( ! [X0,X1] :
( in(X0,a_2_3_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) )
| ~ spl588_58 ),
inference(avatar_component_clause,[],[f9365]) ).
fof(f9367,plain,
( spl588_58
| spl588_4 ),
inference(avatar_split_clause,[],[f5598,f5345,f9365]) ).
fof(f9368,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,sK451)
| below_refl(sK449,X0,sK450) )
| ~ spl588_25
| ~ spl588_58 ),
inference(resolution,[],[f9366,f7382]) ).
fof(f9886,definition,
( spl588_72
<=> ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below(sK449,sK41(sK449,sK450,X0),sK450) ) ),
introduced(definition,[new_symbols(definition,[spl588_72])],[avatar_definition]) ).
fof(f9887,plain,
( ! [X0] :
( ~ below(sK449,sK41(sK449,sK450,X0),sK450)
| latt_element_smaller(sK449,sK450,X0) )
| ~ spl588_72 ),
inference(avatar_component_clause,[],[f9886]) ).
fof(f9888,plain,
( spl588_72
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f5949,f5749,f5703,f5345,f9886]) ).
fof(f9904,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| empty_carrier(sK449)
| ~ meet_commutative(sK449)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(sK41(sK449,sK450,X0),the_carrier(sK449))
| ~ element(sK450,the_carrier(sK449)) )
| ~ spl588_72 ),
inference(resolution,[],[f9887,f3057]) ).
fof(f9911,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| empty_carrier(sK449)
| ~ meet_commutative(sK449)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(sK450,the_carrier(sK449)) )
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9904,f2240]) ).
fof(f9915,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| ~ meet_commutative(sK449)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(sK450,the_carrier(sK449)) )
| spl588_4
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9911,f5347]) ).
fof(f9919,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| ~ meet_absorbing(sK449)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(sK450,the_carrier(sK449)) )
| spl588_4
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9915,f5589]) ).
fof(f9923,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| ~ join_absorbing(sK449)
| ~ latt_str(sK449)
| ~ element(sK450,the_carrier(sK449)) )
| spl588_4
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9919,f5591]) ).
fof(f9924,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| ~ latt_str(sK449)
| ~ element(sK450,the_carrier(sK449)) )
| spl588_4
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9923,f5592]) ).
fof(f9925,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| ~ element(sK450,the_carrier(sK449)) )
| spl588_4
| ~ spl588_6
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9924,f5705]) ).
fof(f9926,plain,
( ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450) )
| spl588_4
| ~ spl588_6
| ~ spl588_11
| ~ spl588_72 ),
inference(forward_subsumption_resolution,[],[f9925,f5751]) ).
fof(f9928,definition,
( spl588_76
<=> ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450) ) ),
introduced(definition,[new_symbols(definition,[spl588_76])],[avatar_definition]) ).
fof(f9929,plain,
( ! [X0] :
( ~ below_refl(sK449,sK41(sK449,sK450,X0),sK450)
| latt_element_smaller(sK449,sK450,X0) )
| ~ spl588_76 ),
inference(avatar_component_clause,[],[f9928]) ).
fof(f9930,plain,
( spl588_76
| spl588_4
| ~ spl588_6
| ~ spl588_11
| ~ spl588_72 ),
inference(avatar_split_clause,[],[f9926,f9886,f5749,f5703,f5345,f9928]) ).
fof(f10845,definition,
( spl588_87
<=> ! [X0] :
( ~ in(X0,a_2_3_lattice3(sK449,sK451))
| below(sK449,sK145(X0,sK449,sK451),sK450) ) ),
introduced(definition,[new_symbols(definition,[spl588_87])],[avatar_definition]) ).
fof(f10846,plain,
( ! [X0] :
( below(sK449,sK145(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_87 ),
inference(avatar_component_clause,[],[f10845]) ).
fof(f10848,plain,
( ! [X0] :
( ~ in(X0,a_2_3_lattice3(sK449,sK451))
| below_refl(sK449,sK145(X0,sK449,sK451),sK450)
| ~ element(sK145(X0,sK449,sK451),the_carrier(sK449)) )
| ~ spl588_28
| ~ spl588_87 ),
inference(resolution,[],[f10846,f7648]) ).
fof(f10859,plain,
( ! [X0] :
( ~ in(X0,a_2_3_lattice3(sK449,sK451))
| below_refl(sK449,sK145(X0,sK449,sK451),sK450) )
| spl588_4
| ~ spl588_28
| ~ spl588_87 ),
inference(forward_subsumption_resolution,[],[f10848,f5599]) ).
fof(f10915,definition,
( spl588_89
<=> ! [X0] :
( latt_element_smaller(sK449,sK450,X0)
| in(sK41(sK449,sK450,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl588_89])],[avatar_definition]) ).
fof(f10916,plain,
( ! [X0] :
( in(sK41(sK449,sK450,X0),X0)
| latt_element_smaller(sK449,sK450,X0) )
| ~ spl588_89 ),
inference(avatar_component_clause,[],[f10915]) ).
fof(f10917,plain,
( spl588_89
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f5950,f5749,f5703,f5345,f10915]) ).
fof(f11027,plain,
( latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451))
| below_refl(sK449,sK41(sK449,sK450,a_2_2_lattice3(sK449,sK451)),sK450)
| ~ spl588_53
| ~ spl588_89 ),
inference(resolution,[],[f10916,f9049]) ).
fof(f11191,plain,
( latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451))
| ~ spl588_53
| ~ spl588_76
| ~ spl588_89 ),
inference(forward_subsumption_resolution,[],[f11027,f9929]) ).
fof(f11220,definition,
( spl588_91
<=> ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl588_91])],[avatar_definition]) ).
fof(f11221,plain,
( ! [X0,X1] :
( latt_set_smaller(sK449,sK145(X0,sK449,X1),X1)
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| ~ spl588_91 ),
inference(avatar_component_clause,[],[f11220]) ).
fof(f11222,plain,
( spl588_91
| spl588_4 ),
inference(avatar_split_clause,[],[f5601,f5345,f11220]) ).
fof(f11582,definition,
( spl588_96
<=> ! [X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ below(sK449,sK41(sK449,X0,X1),X0)
| ~ element(X0,the_carrier(sK449)) ) ),
introduced(definition,[new_symbols(definition,[spl588_96])],[avatar_definition]) ).
fof(f11583,plain,
( ! [X0,X1] :
( ~ below(sK449,sK41(sK449,X0,X1),X0)
| latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449)) )
| ~ spl588_96 ),
inference(avatar_component_clause,[],[f11582]) ).
fof(f11584,plain,
( spl588_96
| spl588_4 ),
inference(avatar_split_clause,[],[f5533,f5345,f11582]) ).
fof(f11588,plain,
( ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2)
| ~ element(sK41(sK449,X0,X1),the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_96 ),
inference(resolution,[],[f11583,f2229]) ).
fof(f11589,plain,
( ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2)
| ~ element(sK41(sK449,X0,X1),the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_96 ),
inference(duplicate_literal_removal,[],[f11588]) ).
fof(f11593,plain,
( ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2)
| empty_carrier(sK449)
| ~ latt_str(sK449) )
| ~ spl588_96 ),
inference(forward_subsumption_resolution,[],[f11589,f2240]) ).
fof(f11597,plain,
( ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2)
| ~ latt_str(sK449) )
| spl588_4
| ~ spl588_96 ),
inference(forward_subsumption_resolution,[],[f11593,f5347]) ).
fof(f11601,plain,
( ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2) )
| spl588_4
| ~ spl588_6
| ~ spl588_96 ),
inference(forward_subsumption_resolution,[],[f11597,f5705]) ).
fof(f12467,definition,
( spl588_121
<=> ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl588_121])],[avatar_definition]) ).
fof(f12468,plain,
( ! [X0,X1] :
( sK145(X0,sK449,X1) = X0
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| ~ spl588_121 ),
inference(avatar_component_clause,[],[f12467]) ).
fof(f12469,plain,
( spl588_121
| spl588_4 ),
inference(avatar_split_clause,[],[f5600,f5345,f12467]) ).
fof(f12471,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451))
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_24
| ~ spl588_121 ),
inference(superposition,[],[f7357,f12468]) ).
fof(f12478,plain,
( ! [X0] :
( below_refl(sK449,X0,sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_24
| ~ spl588_121 ),
inference(duplicate_literal_removal,[],[f12471]) ).
fof(f14038,definition,
( spl588_154
<=> latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_154])],[avatar_definition]) ).
fof(f14039,plain,
( ~ latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451))
| spl588_154 ),
inference(avatar_component_clause,[],[f14038]) ).
fof(f14040,plain,
( latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451))
| ~ spl588_154 ),
inference(avatar_component_clause,[],[f14038]) ).
fof(f14041,plain,
( spl588_154
| ~ spl588_53
| ~ spl588_76
| ~ spl588_89 ),
inference(avatar_split_clause,[],[f11191,f10915,f9928,f9048,f14038]) ).
fof(f14043,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_154 ),
inference(resolution,[],[f14040,f5072]) ).
fof(f14044,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_154 ),
inference(resolution,[],[f14040,f5071]) ).
fof(f14045,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_154 ),
inference(resolution,[],[f14040,f5070]) ).
fof(f14047,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14045,f5751]) ).
fof(f14048,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14044,f5751]) ).
fof(f14049,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| empty_carrier(sK449)
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14043,f5751]) ).
fof(f14051,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14047,f5347]) ).
fof(f14052,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14048,f5347]) ).
fof(f14053,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ lattice(sK449)
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14049,f5347]) ).
fof(f14055,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14051,f5746]) ).
fof(f14056,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14052,f5746]) ).
fof(f14057,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ complete_latt_str(sK449)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14053,f5746]) ).
fof(f14059,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14055,f5710]) ).
fof(f14060,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14056,f5710]) ).
fof(f14061,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14057,f5710]) ).
fof(f14063,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14059,f5705]) ).
fof(f14064,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14060,f5705]) ).
fof(f14065,plain,
( sK450 = join_of_latt_set(sK449,a_2_2_lattice3(sK449,sK451))
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14061,f5705]) ).
fof(f14067,plain,
( sK450 = meet_of_latt_set(sK449,sK451)
| ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_demodulation,[],[f14063,f7162]) ).
fof(f14068,plain,
( sK450 = meet_of_latt_set(sK449,sK451)
| latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_demodulation,[],[f14064,f7162]) ).
fof(f14069,plain,
( sK450 = meet_of_latt_set(sK449,sK451)
| element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_demodulation,[],[f14065,f7162]) ).
fof(f14071,plain,
( ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14067,f5315]) ).
fof(f14072,plain,
( latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14068,f5315]) ).
fof(f14073,plain,
( element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(forward_subsumption_resolution,[],[f14069,f5315]) ).
fof(f14076,definition,
( spl588_155
<=> element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449)) ),
introduced(definition,[new_symbols(definition,[spl588_155])],[avatar_definition]) ).
fof(f14078,plain,
( element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ spl588_155 ),
inference(avatar_component_clause,[],[f14076]) ).
fof(f14079,plain,
( spl588_155
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(avatar_split_clause,[],[f14073,f14038,f7161,f5749,f5744,f5708,f5703,f5345,f5313,f14076]) ).
fof(f14370,definition,
( spl588_157
<=> below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450)) ),
introduced(definition,[new_symbols(definition,[spl588_157])],[avatar_definition]) ).
fof(f14372,plain,
( ~ below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| spl588_157 ),
inference(avatar_component_clause,[],[f14370]) ).
fof(f14373,plain,
( ~ spl588_157
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(avatar_split_clause,[],[f14071,f14038,f7161,f5749,f5744,f5708,f5703,f5345,f5313,f14370]) ).
fof(f14375,definition,
( spl588_158
<=> latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_158])],[avatar_definition]) ).
fof(f14377,plain,
( latt_element_smaller(sK449,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),a_2_2_lattice3(sK449,sK451))
| ~ spl588_158 ),
inference(avatar_component_clause,[],[f14375]) ).
fof(f14378,plain,
( spl588_158
| spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154 ),
inference(avatar_split_clause,[],[f14072,f14038,f7161,f5749,f5744,f5708,f5703,f5345,f5313,f14375]) ).
fof(f14650,definition,
( spl588_169
<=> ! [X0,X1] :
( below(sK449,sK450,X0)
| ~ in(sK450,X1)
| ~ latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449)) ) ),
introduced(definition,[new_symbols(definition,[spl588_169])],[avatar_definition]) ).
fof(f14651,plain,
( ! [X0,X1] :
( ~ latt_element_smaller(sK449,X0,X1)
| ~ in(sK450,X1)
| below(sK449,sK450,X0)
| ~ element(X0,the_carrier(sK449)) )
| ~ spl588_169 ),
inference(avatar_component_clause,[],[f14650]) ).
fof(f14652,plain,
( spl588_169
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f5952,f5749,f5703,f5345,f14650]) ).
fof(f14655,plain,
( ~ in(sK450,a_2_2_lattice3(sK449,sK451))
| below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ spl588_158
| ~ spl588_169 ),
inference(resolution,[],[f14651,f14377]) ).
fof(f14670,plain,
( below(sK449,sK450,sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450))
| ~ element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ spl588_23
| ~ spl588_158
| ~ spl588_169 ),
inference(forward_subsumption_resolution,[],[f14655,f7277]) ).
fof(f14677,plain,
( ~ element(sK68(sK449,a_2_2_lattice3(sK449,sK451),sK450),the_carrier(sK449))
| ~ spl588_23
| spl588_157
| ~ spl588_158
| ~ spl588_169 ),
inference(forward_subsumption_resolution,[],[f14670,f14372]) ).
fof(f14680,plain,
( $false
| ~ spl588_23
| ~ spl588_155
| spl588_157
| ~ spl588_158
| ~ spl588_169 ),
inference(forward_subsumption_resolution,[],[f14677,f14078]) ).
fof(f14681,plain,
( ~ spl588_23
| ~ spl588_155
| spl588_157
| ~ spl588_158
| ~ spl588_169 ),
inference(avatar_contradiction_clause,[],[f14680]) ).
fof(f17540,plain,
( spl588_24
| spl588_4
| ~ spl588_28
| ~ spl588_87 ),
inference(avatar_split_clause,[],[f10859,f10845,f7647,f5345,f7356]) ).
fof(f21927,definition,
( spl588_301
<=> ! [X2,X0,X1] :
( latt_element_smaller(sK449,X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[spl588_301])],[avatar_definition]) ).
fof(f21928,plain,
( ! [X2,X0,X1] :
( ~ latt_set_smaller(sK449,sK41(sK449,X0,X1),X2)
| ~ element(X0,the_carrier(sK449))
| ~ in(X0,X2)
| latt_element_smaller(sK449,X0,X1) )
| ~ spl588_301 ),
inference(avatar_component_clause,[],[f21927]) ).
fof(f21929,plain,
( spl588_301
| spl588_4
| ~ spl588_6
| ~ spl588_96 ),
inference(avatar_split_clause,[],[f11601,f11582,f5703,f5345,f21927]) ).
fof(f23390,definition,
( spl588_354
<=> ! [X0,X1] :
( in(X0,a_2_2_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl588_354])],[avatar_definition]) ).
fof(f23391,plain,
( ! [X0,X1] :
( in(X0,a_2_2_lattice3(sK449,X1))
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,X1) )
| ~ spl588_354 ),
inference(avatar_component_clause,[],[f23390]) ).
fof(f23392,plain,
( spl588_354
| spl588_4 ),
inference(avatar_split_clause,[],[f5482,f5345,f23390]) ).
fof(f30235,definition,
( spl588_457
<=> ! [X0,X1] :
( below(sK449,X0,sK450)
| ~ in(X0,X1)
| ~ element(X0,the_carrier(sK449))
| ~ latt_element_smaller(sK449,sK450,X1) ) ),
introduced(definition,[new_symbols(definition,[spl588_457])],[avatar_definition]) ).
fof(f30236,plain,
( ! [X0,X1] :
( ~ latt_element_smaller(sK449,sK450,X1)
| ~ in(X0,X1)
| ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450) )
| ~ spl588_457 ),
inference(avatar_component_clause,[],[f30235]) ).
fof(f30237,plain,
( spl588_457
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f5953,f5749,f5703,f5345,f30235]) ).
fof(f34927,definition,
( spl588_527
<=> ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl588_527])],[avatar_definition]) ).
fof(f34928,plain,
( ! [X0,X1] :
( element(sK145(X0,sK449,X1),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,X1)) )
| ~ spl588_527 ),
inference(avatar_component_clause,[],[f34927]) ).
fof(f34929,plain,
( spl588_527
| spl588_4 ),
inference(avatar_split_clause,[],[f5599,f5345,f34927]) ).
fof(f35211,definition,
( spl588_528
<=> ! [X0] : latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0)) ),
introduced(definition,[new_symbols(definition,[spl588_528])],[avatar_definition]) ).
fof(f35212,plain,
( ! [X0] : latt_element_smaller(sK449,meet_of_latt_set(sK449,X0),a_2_2_lattice3(sK449,X0))
| ~ spl588_528 ),
inference(avatar_component_clause,[],[f35211]) ).
fof(f35213,plain,
( spl588_528
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(avatar_split_clause,[],[f7217,f7161,f5744,f5708,f5703,f5345,f35211]) ).
fof(f40246,plain,
( latt_element_smaller(sK449,sK450,a_2_2_lattice3(sK449,sK451))
| ~ spl588_1
| ~ spl588_528 ),
inference(superposition,[],[f35212,f5314]) ).
fof(f40247,plain,
( $false
| ~ spl588_1
| spl588_154
| ~ spl588_528 ),
inference(forward_subsumption_resolution,[],[f40246,f14039]) ).
fof(f40248,plain,
( ~ spl588_1
| spl588_154
| ~ spl588_528 ),
inference(avatar_contradiction_clause,[],[f40247]) ).
fof(f46244,plain,
( ~ below(sK449,sK450,sK39(sK449,sK450,sK451))
| ~ element(sK450,the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3 ),
inference(resolution,[],[f5323,f2232]) ).
fof(f46245,plain,
( ~ below(sK449,sK450,sK39(sK449,sK450,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_3
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f46244,f5751]) ).
fof(f46246,plain,
( ~ below(sK449,sK450,sK39(sK449,sK450,sK451))
| ~ latt_str(sK449)
| spl588_3
| spl588_4
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f46245,f5347]) ).
fof(f46247,plain,
( ~ below(sK449,sK450,sK39(sK449,sK450,sK451))
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(forward_subsumption_resolution,[],[f46246,f5705]) ).
fof(f47241,definition,
( spl588_645
<=> below(sK449,sK450,sK39(sK449,sK450,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_645])],[avatar_definition]) ).
fof(f47243,plain,
( ~ below(sK449,sK450,sK39(sK449,sK450,sK451))
| spl588_645 ),
inference(avatar_component_clause,[],[f47241]) ).
fof(f47244,plain,
( ~ spl588_645
| spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11 ),
inference(avatar_split_clause,[],[f46247,f5749,f5703,f5345,f5321,f47241]) ).
fof(f49407,plain,
( ! [X0] :
( ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450) )
| ~ spl588_154
| ~ spl588_457 ),
inference(resolution,[],[f14040,f30236]) ).
fof(f55773,definition,
( spl588_733
<=> ! [X0] :
( ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450) ) ),
introduced(definition,[new_symbols(definition,[spl588_733])],[avatar_definition]) ).
fof(f55774,plain,
( ! [X0] :
( ~ in(X0,a_2_2_lattice3(sK449,sK451))
| ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450) )
| ~ spl588_733 ),
inference(avatar_component_clause,[],[f55773]) ).
fof(f55775,plain,
( spl588_733
| ~ spl588_154
| ~ spl588_457 ),
inference(avatar_split_clause,[],[f49407,f30235,f14038,f55773]) ).
fof(f55776,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450)
| ~ element(X0,the_carrier(sK449))
| ~ latt_set_smaller(sK449,X0,sK451) )
| ~ spl588_354
| ~ spl588_733 ),
inference(resolution,[],[f55774,f23391]) ).
fof(f55959,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450)
| ~ latt_set_smaller(sK449,X0,sK451) )
| ~ spl588_354
| ~ spl588_733 ),
inference(duplicate_literal_removal,[],[f55776]) ).
fof(f56031,definition,
( spl588_738
<=> ! [X0] :
( ~ element(X0,the_carrier(sK449))
| below(sK449,X0,sK450)
| ~ latt_set_smaller(sK449,X0,sK451) ) ),
introduced(definition,[new_symbols(definition,[spl588_738])],[avatar_definition]) ).
fof(f56032,plain,
( ! [X0] :
( ~ latt_set_smaller(sK449,X0,sK451)
| below(sK449,X0,sK450)
| ~ element(X0,the_carrier(sK449)) )
| ~ spl588_738 ),
inference(avatar_component_clause,[],[f56031]) ).
fof(f56033,plain,
( spl588_738
| ~ spl588_354
| ~ spl588_733 ),
inference(avatar_split_clause,[],[f55959,f55773,f23390,f56031]) ).
fof(f56323,plain,
( ! [X0] :
( below(sK449,sK145(X0,sK449,sK451),sK450)
| ~ element(sK145(X0,sK449,sK451),the_carrier(sK449))
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_91
| ~ spl588_738 ),
inference(resolution,[],[f56032,f11221]) ).
fof(f56341,plain,
( ! [X0] :
( below(sK449,sK145(X0,sK449,sK451),sK450)
| ~ in(X0,a_2_3_lattice3(sK449,sK451)) )
| ~ spl588_91
| ~ spl588_527
| ~ spl588_738 ),
inference(forward_subsumption_resolution,[],[f56323,f34928]) ).
fof(f63687,definition,
( spl588_822
<=> ! [X0,X1] :
( below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| ~ element(X1,the_carrier(sK449)) ) ),
introduced(definition,[new_symbols(definition,[spl588_822])],[avatar_definition]) ).
fof(f63688,plain,
( ! [X0,X1] :
( ~ latt_element_smaller(sK449,X1,a_2_2_lattice3(sK449,X0))
| below(sK449,meet_of_latt_set(sK449,X0),X1)
| ~ element(X1,the_carrier(sK449)) )
| ~ spl588_822 ),
inference(avatar_component_clause,[],[f63687]) ).
fof(f63689,plain,
( spl588_822
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20 ),
inference(avatar_split_clause,[],[f7215,f7161,f5744,f5708,f5703,f5345,f63687]) ).
fof(f79449,plain,
( spl588_87
| ~ spl588_91
| ~ spl588_527
| ~ spl588_738 ),
inference(avatar_split_clause,[],[f56341,f56031,f34927,f11220,f10845]) ).
fof(f79474,plain,
( spl588_25
| ~ spl588_24
| ~ spl588_121 ),
inference(avatar_split_clause,[],[f12478,f12467,f7356,f7381]) ).
fof(f79668,plain,
( spl588_8
| ~ spl588_25
| ~ spl588_58 ),
inference(avatar_split_clause,[],[f9368,f9365,f7381,f5713]) ).
fof(f83416,definition,
( spl588_1125
<=> latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_1125])],[avatar_definition]) ).
fof(f83417,plain,
( ~ latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451))
| spl588_1125 ),
inference(avatar_component_clause,[],[f83416]) ).
fof(f83418,plain,
( latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451))
| ~ spl588_1125 ),
inference(avatar_component_clause,[],[f83416]) ).
fof(f83425,plain,
( below(sK449,meet_of_latt_set(sK449,sK451),sK39(sK449,sK450,sK451))
| ~ element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| ~ spl588_822
| ~ spl588_1125 ),
inference(resolution,[],[f83418,f63688]) ).
fof(f83443,plain,
( below(sK449,meet_of_latt_set(sK449,sK451),sK39(sK449,sK450,sK451))
| ~ spl588_17
| ~ spl588_822
| ~ spl588_1125 ),
inference(forward_subsumption_resolution,[],[f83425,f6410]) ).
fof(f83450,plain,
( below(sK449,sK450,sK39(sK449,sK450,sK451))
| ~ spl588_1
| ~ spl588_17
| ~ spl588_822
| ~ spl588_1125 ),
inference(forward_demodulation,[],[f83443,f5314]) ).
fof(f83458,plain,
( $false
| ~ spl588_1
| ~ spl588_17
| spl588_645
| ~ spl588_822
| ~ spl588_1125 ),
inference(forward_subsumption_resolution,[],[f83450,f47243]) ).
fof(f83459,plain,
( ~ spl588_1
| ~ spl588_17
| spl588_645
| ~ spl588_822
| ~ spl588_1125 ),
inference(avatar_contradiction_clause,[],[f83458]) ).
fof(f83495,plain,
( in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451))
| ~ element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| spl588_1125 ),
inference(resolution,[],[f83417,f2241]) ).
fof(f83498,plain,
( in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451))
| empty_carrier(sK449)
| ~ latt_str(sK449)
| ~ spl588_17
| spl588_1125 ),
inference(forward_subsumption_resolution,[],[f83495,f6410]) ).
fof(f83501,plain,
( in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451))
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_17
| spl588_1125 ),
inference(forward_subsumption_resolution,[],[f83498,f5347]) ).
fof(f83504,plain,
( in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451))
| spl588_4
| ~ spl588_6
| ~ spl588_17
| spl588_1125 ),
inference(forward_subsumption_resolution,[],[f83501,f5705]) ).
fof(f84865,definition,
( spl588_1152
<=> in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451)) ),
introduced(definition,[new_symbols(definition,[spl588_1152])],[avatar_definition]) ).
fof(f84867,plain,
( in(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),a_2_2_lattice3(sK449,sK451))
| ~ spl588_1152 ),
inference(avatar_component_clause,[],[f84865]) ).
fof(f84868,plain,
( spl588_1152
| spl588_4
| ~ spl588_6
| ~ spl588_17
| spl588_1125 ),
inference(avatar_split_clause,[],[f83504,f83416,f6408,f5703,f5345,f84865]) ).
fof(f84873,plain,
( latt_set_smaller(sK449,sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451),sK451)
| empty_carrier(sK449)
| ~ latt_str(sK449)
| ~ spl588_1152 ),
inference(resolution,[],[f84867,f2855]) ).
fof(f84874,plain,
( sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)) = sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451)
| empty_carrier(sK449)
| ~ latt_str(sK449)
| ~ spl588_1152 ),
inference(resolution,[],[f84867,f2856]) ).
fof(f84935,plain,
( sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)) = sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_1152 ),
inference(forward_subsumption_resolution,[],[f84874,f5347]) ).
fof(f84936,plain,
( latt_set_smaller(sK449,sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451),sK451)
| ~ latt_str(sK449)
| spl588_4
| ~ spl588_1152 ),
inference(forward_subsumption_resolution,[],[f84873,f5347]) ).
fof(f84939,plain,
( sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)) = sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451)
| spl588_4
| ~ spl588_6
| ~ spl588_1152 ),
inference(forward_subsumption_resolution,[],[f84935,f5705]) ).
fof(f84940,plain,
( latt_set_smaller(sK449,sK144(sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK449,sK451),sK451)
| spl588_4
| ~ spl588_6
| ~ spl588_1152 ),
inference(forward_subsumption_resolution,[],[f84936,f5705]) ).
fof(f84941,plain,
( latt_set_smaller(sK449,sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK451)
| spl588_4
| ~ spl588_6
| ~ spl588_1152 ),
inference(forward_demodulation,[],[f84940,f84939]) ).
fof(f84943,definition,
( spl588_1153
<=> latt_set_smaller(sK449,sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK451) ),
introduced(definition,[new_symbols(definition,[spl588_1153])],[avatar_definition]) ).
fof(f84945,plain,
( latt_set_smaller(sK449,sK41(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451)),sK451)
| ~ spl588_1153 ),
inference(avatar_component_clause,[],[f84943]) ).
fof(f84946,plain,
( spl588_1153
| spl588_4
| ~ spl588_6
| ~ spl588_1152 ),
inference(avatar_split_clause,[],[f84941,f84865,f5703,f5345,f84943]) ).
fof(f84947,plain,
( ~ element(sK39(sK449,sK450,sK451),the_carrier(sK449))
| ~ in(sK39(sK449,sK450,sK451),sK451)
| latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451))
| ~ spl588_301
| ~ spl588_1153 ),
inference(resolution,[],[f84945,f21928]) ).
fof(f84961,plain,
( ~ in(sK39(sK449,sK450,sK451),sK451)
| latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451))
| ~ spl588_17
| ~ spl588_301
| ~ spl588_1153 ),
inference(forward_subsumption_resolution,[],[f84947,f6410]) ).
fof(f84966,plain,
( latt_element_smaller(sK449,sK39(sK449,sK450,sK451),a_2_2_lattice3(sK449,sK451))
| ~ spl588_15
| ~ spl588_17
| ~ spl588_301
| ~ spl588_1153 ),
inference(forward_subsumption_resolution,[],[f84961,f6348]) ).
fof(f84969,plain,
( $false
| ~ spl588_15
| ~ spl588_17
| ~ spl588_301
| spl588_1125
| ~ spl588_1153 ),
inference(forward_subsumption_resolution,[],[f84966,f83417]) ).
fof(f84970,plain,
( ~ spl588_15
| ~ spl588_17
| ~ spl588_301
| spl588_1125
| ~ spl588_1153 ),
inference(avatar_contradiction_clause,[],[f84969]) ).
cnf(s1,plain,
( ~ spl588_1
| ~ spl588_2
| ~ spl588_3 ),
inference(sat_conversion,[],[f5324]) ).
cnf(s2,plain,
( spl588_1
| spl588_3 ),
inference(sat_conversion,[],[f5329]) ).
cnf(s3,plain,
~ spl588_4,
inference(sat_conversion,[],[f5348]) ).
cnf(s5,plain,
spl588_6,
inference(sat_conversion,[],[f5706]) ).
cnf(s6,plain,
spl588_7,
inference(sat_conversion,[],[f5711]) ).
cnf(s7,plain,
( spl588_1
| spl588_8 ),
inference(sat_conversion,[],[f5715]) ).
cnf(s9,plain,
spl588_10,
inference(sat_conversion,[],[f5747]) ).
cnf(s10,plain,
spl588_11,
inference(sat_conversion,[],[f5752]) ).
cnf(s13,plain,
( ~ spl588_1
| ~ spl588_3
| spl588_14 ),
inference(sat_conversion,[],[f6318]) ).
cnf(s15,plain,
( spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_15 ),
inference(sat_conversion,[],[f6349]) ).
cnf(s17,plain,
( ~ spl588_1
| ~ spl588_3
| spl588_16 ),
inference(sat_conversion,[],[f6378]) ).
cnf(s18,plain,
( spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_17 ),
inference(sat_conversion,[],[f6411]) ).
cnf(s21,plain,
( spl588_2
| ~ spl588_8
| ~ spl588_14
| ~ spl588_16 ),
inference(sat_conversion,[],[f6727]) ).
cnf(s23,plain,
( spl588_4
| spl588_20 ),
inference(sat_conversion,[],[f7163]) ).
cnf(s26,plain,
( ~ spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_23 ),
inference(sat_conversion,[],[f7278]) ).
cnf(s31,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_28 ),
inference(sat_conversion,[],[f7649]) ).
cnf(s37,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_8
| spl588_34 ),
inference(sat_conversion,[],[f8302]) ).
cnf(s56,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_34
| spl588_53 ),
inference(sat_conversion,[],[f9050]) ).
cnf(s61,plain,
( spl588_4
| spl588_58 ),
inference(sat_conversion,[],[f9367]) ).
cnf(s75,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_72 ),
inference(sat_conversion,[],[f9888]) ).
cnf(s79,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| ~ spl588_72
| spl588_76 ),
inference(sat_conversion,[],[f9930]) ).
cnf(s88,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_89 ),
inference(sat_conversion,[],[f10917]) ).
cnf(s90,plain,
( spl588_4
| spl588_91 ),
inference(sat_conversion,[],[f11222]) ).
cnf(s95,plain,
( spl588_4
| spl588_96 ),
inference(sat_conversion,[],[f11584]) ).
cnf(s120,plain,
( spl588_4
| spl588_121 ),
inference(sat_conversion,[],[f12469]) ).
cnf(s153,plain,
( ~ spl588_53
| ~ spl588_76
| ~ spl588_89
| spl588_154 ),
inference(sat_conversion,[],[f14041]) ).
cnf(s154,plain,
( spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154
| spl588_155 ),
inference(sat_conversion,[],[f14079]) ).
cnf(s156,plain,
( spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154
| ~ spl588_157 ),
inference(sat_conversion,[],[f14373]) ).
cnf(s157,plain,
( spl588_1
| spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_11
| ~ spl588_20
| ~ spl588_154
| spl588_158 ),
inference(sat_conversion,[],[f14378]) ).
cnf(s168,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_169 ),
inference(sat_conversion,[],[f14652]) ).
cnf(s169,plain,
( ~ spl588_23
| ~ spl588_155
| spl588_157
| ~ spl588_158
| ~ spl588_169 ),
inference(sat_conversion,[],[f14681]) ).
cnf(s225,plain,
( spl588_4
| spl588_24
| ~ spl588_28
| ~ spl588_87 ),
inference(sat_conversion,[],[f17540]) ).
cnf(s309,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_96
| spl588_301 ),
inference(sat_conversion,[],[f21929]) ).
cnf(s359,plain,
( spl588_4
| spl588_354 ),
inference(sat_conversion,[],[f23392]) ).
cnf(s459,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_11
| spl588_457 ),
inference(sat_conversion,[],[f30237]) ).
cnf(s529,plain,
( spl588_4
| spl588_527 ),
inference(sat_conversion,[],[f34929]) ).
cnf(s530,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20
| spl588_528 ),
inference(sat_conversion,[],[f35213]) ).
cnf(s643,plain,
( ~ spl588_1
| spl588_154
| ~ spl588_528 ),
inference(sat_conversion,[],[f40248]) ).
cnf(s824,plain,
( spl588_3
| spl588_4
| ~ spl588_6
| ~ spl588_11
| ~ spl588_645 ),
inference(sat_conversion,[],[f47244]) ).
cnf(s921,plain,
( ~ spl588_154
| ~ spl588_457
| spl588_733 ),
inference(sat_conversion,[],[f55775]) ).
cnf(s925,plain,
( ~ spl588_354
| ~ spl588_733
| spl588_738 ),
inference(sat_conversion,[],[f56033]) ).
cnf(s1028,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_7
| ~ spl588_10
| ~ spl588_20
| spl588_822 ),
inference(sat_conversion,[],[f63689]) ).
cnf(s1297,plain,
( spl588_87
| ~ spl588_91
| ~ spl588_527
| ~ spl588_738 ),
inference(sat_conversion,[],[f79449]) ).
cnf(s1298,plain,
( ~ spl588_24
| spl588_25
| ~ spl588_121 ),
inference(sat_conversion,[],[f79474]) ).
cnf(s1299,plain,
( spl588_8
| ~ spl588_25
| ~ spl588_58 ),
inference(sat_conversion,[],[f79668]) ).
cnf(s1349,plain,
( ~ spl588_1
| ~ spl588_17
| spl588_645
| ~ spl588_822
| ~ spl588_1125 ),
inference(sat_conversion,[],[f83459]) ).
cnf(s1382,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_17
| spl588_1125
| spl588_1152 ),
inference(sat_conversion,[],[f84868]) ).
cnf(s1383,plain,
( spl588_4
| ~ spl588_6
| ~ spl588_1152
| spl588_1153 ),
inference(sat_conversion,[],[f84946]) ).
cnf(s1385,plain,
( ~ spl588_15
| ~ spl588_17
| ~ spl588_301
| spl588_1125
| ~ spl588_1153 ),
inference(sat_conversion,[],[f84970]) ).
cnf(s1414,plain,
spl588_527,
inference(rat,[],[s529,s3]) ).
cnf(s1421,plain,
spl588_457,
inference(rat,[],[s459,s5,s10,s3]) ).
cnf(s1431,plain,
spl588_354,
inference(rat,[],[s359,s3]) ).
cnf(s1453,plain,
spl588_169,
inference(rat,[],[s168,s5,s10,s3]) ).
cnf(s1467,plain,
spl588_121,
inference(rat,[],[s120,s3]) ).
cnf(s1476,plain,
spl588_96,
inference(rat,[],[s95,s3]) ).
cnf(s1478,plain,
spl588_91,
inference(rat,[],[s90,s3]) ).
cnf(s1479,plain,
spl588_89,
inference(rat,[],[s88,s5,s10,s3]) ).
cnf(s1482,plain,
spl588_72,
inference(rat,[],[s75,s5,s10,s3]) ).
cnf(s1487,plain,
spl588_58,
inference(rat,[],[s61,s3]) ).
cnf(s1499,plain,
spl588_28,
inference(rat,[],[s31,s5,s10,s3]) ).
cnf(s1502,plain,
spl588_20,
inference(rat,[],[s23,s3]) ).
cnf(s1535,plain,
spl588_301,
inference(rat,[],[s309,s3,s5,s1476]) ).
cnf(s1547,plain,
spl588_76,
inference(rat,[],[s79,s3,s5,s10,s1482]) ).
cnf(s1602,plain,
spl588_822,
inference(rat,[],[s1028,s3,s5,s9,s6,s1502]) ).
cnf(s1603,plain,
spl588_528,
inference(rat,[],[s530,s3,s5,s9,s6,s1502]) ).
cnf(s1727,plain,
spl588_1,
inference(rat,[],[s169,s154,s156,s157,s153,s56,s26,s37,s2,s7,s1453,s5,s6,s9,s10,s3,s1502,s1479,s1547]) ).
cnf(s1728,plain,
spl588_154,
inference(rat,[],[s643,s1603,s1727]) ).
cnf(s1729,plain,
spl588_733,
inference(rat,[],[s921,s1421,s1728]) ).
cnf(s1731,plain,
spl588_738,
inference(rat,[],[s925,s1431,s1729]) ).
cnf(s1734,plain,
spl588_87,
inference(rat,[],[s1297,s1478,s1414,s1731]) ).
cnf(s1735,plain,
spl588_24,
inference(rat,[],[s225,s1499,s3,s1734]) ).
cnf(s1736,plain,
spl588_25,
inference(rat,[],[s1298,s1467,s1735]) ).
cnf(s1737,plain,
spl588_8,
inference(rat,[],[s1299,s1487,s1736]) ).
cnf(s1796,plain,
spl588_3,
inference(rat,[],[s1383,s1385,s1382,s1349,s15,s18,s824,s5,s3,s1535,s1727,s1602,s10]) ).
cnf(s1801,plain,
spl588_16,
inference(rat,[],[s17,s1727,s1796]) ).
cnf(s1802,plain,
spl588_14,
inference(rat,[],[s13,s1727,s1796]) ).
cnf(s1804,plain,
~ spl588_2,
inference(rat,[],[s1,s1727,s1796]) ).
cnf(s1876,plain,
$false,
inference(rat,[],[s21,s1804,s1737,s1801,s1802]) ).
fof(f84973,plain,
$false,
inference(avatar_sat_refutation,[],[s1876]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU351+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.12/0.37 % Computer : n014.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 04:50:31 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 15.66/3.08 % (1439631)Detected formulas, will run a generic FOF schedule.
% 15.66/3.08 % (1439636)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=3758256416:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.66/3.08 % (1439639)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2223660509:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.66/3.08 % (1439642)dis-21_1_sil=8000:lcm=predicate:random_seed=2351468385: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)
% 15.66/3.08 % (1439640)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2217285892:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.66/3.08 % (1439638)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=4105483876:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.66/3.08 % (1439637)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=257545493:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.66/3.08 % (1439641)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=551396846:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.66/3.08 % (1439639)Instruction limit reached!
% 15.66/3.08 % (1439639)------------------------------
% 15.66/3.08 % (1439639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.66/3.08 % (1439639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.66/3.08 % (1439639)CaDiCaL version: 2.1.3
% 15.66/3.08 % (1439639)Termination reason: Instruction limit
% 15.66/3.08 % (1439639)Termination phase: Saturation
% 15.66/3.08 % (1439639)Time elapsed: 0.059 s
% 15.66/3.08 % (1439639)Peak memory usage: 91 MB
% 15.66/3.08 % (1439639)Instructions burned: 110 (million)
% 15.66/3.08 % (1439642)Instruction limit reached!
% 15.66/3.08 % (1439642)------------------------------
% 15.66/3.08 % (1439642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.66/3.08 % (1439642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.66/3.08 % (1439642)CaDiCaL version: 2.1.3
% 15.66/3.08 % (1439642)Termination reason: Instruction limit
% 15.66/3.08 % (1439642)Termination phase: Saturation
% 15.66/3.08 % (1439642)Time elapsed: 0.065 s
% 15.66/3.08 % (1439642)Peak memory usage: 91 MB
% 15.66/3.08 % (1439642)Instructions burned: 130 (million)
% 15.66/3.08 % (1439640)Instruction limit reached!
% 15.66/3.08 % (1439640)------------------------------
% 15.66/3.08 % (1439640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.66/3.08 % (1439640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.66/3.08 % (1439640)CaDiCaL version: 2.1.3
% 15.66/3.08 % (1439640)Termination reason: Instruction limit
% 15.66/3.08 % (1439640)Termination phase: Saturation
% 15.66/3.08 % (1439640)Time elapsed: 0.074 s
% 15.66/3.08 % (1439640)Peak memory usage: 91 MB
% 15.66/3.08 % (1439640)Instructions burned: 120 (million)
% 15.66/3.08 % (1439641)Instruction limit reached!
% 15.66/3.08 % (1439641)------------------------------
% 15.66/3.08 % (1439641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.66/3.08 % (1439641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.66/3.08 % (1439641)CaDiCaL version: 2.1.3
% 15.66/3.08 % (1439641)Termination reason: Instruction limit
% 15.66/3.08 % (1439641)Termination phase: Saturation
% 15.66/3.08 % (1439641)Time elapsed: 0.086 s
% 15.66/3.08 % (1439641)Peak memory usage: 91 MB
% 15.66/3.08 % (1439641)Instructions burned: 139 (million)
% 15.66/3.08 % (1439651)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4221507241:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.66/3.08 % (1439650)lrs+10_1_sil=8000:sp=occurrence:random_seed=1582986027:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 15.66/3.08 % (1439652)lrs+1011_1_sil=32000:sp=occurrence:random_seed=312887078:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.66/3.08 % (1439651)Refutation not found, incomplete strategy
% 15.66/3.08 % (1439651)------------------------------
% 15.66/3.08 % (1439651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.66/3.08 % (1439651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439651)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439651)Termination reason: Refutation not found, incomplete strategy
% 21.15/3.97 % (1439651)Time elapsed: 0.013 s
% 21.15/3.97 % (1439651)Peak memory usage: 89 MB
% 21.15/3.97 % (1439651)Instructions burned: 18 (million)
% 21.15/3.97 % (1439653)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=1244752131:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 21.15/3.97 % (1439650)Instruction limit reached!
% 21.15/3.97 % (1439650)------------------------------
% 21.15/3.97 % (1439650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439650)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439650)Termination reason: Instruction limit
% 21.15/3.97 % (1439650)Termination phase: Saturation
% 21.15/3.97 % (1439650)Time elapsed: 0.180 s
% 21.15/3.97 % (1439650)Peak memory usage: 94 MB
% 21.15/3.97 % (1439650)Instructions burned: 286 (million)
% 21.15/3.97 % (1439653)Instruction limit reached!
% 21.15/3.97 % (1439653)------------------------------
% 21.15/3.97 % (1439653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439653)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439653)Termination reason: Instruction limit
% 21.15/3.97 % (1439653)Termination phase: Saturation
% 21.15/3.97 % (1439653)Time elapsed: 0.144 s
% 21.15/3.97 % (1439653)Peak memory usage: 93 MB
% 21.15/3.97 % (1439653)Instructions burned: 248 (million)
% 21.15/3.97 % (1439652)Instruction limit reached!
% 21.15/3.97 % (1439652)------------------------------
% 21.15/3.97 % (1439652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439652)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439652)Termination reason: Instruction limit
% 21.15/3.97 % (1439652)Termination phase: Saturation
% 21.15/3.97 % (1439652)Time elapsed: 0.216 s
% 21.15/3.97 % (1439652)Peak memory usage: 95 MB
% 21.15/3.97 % (1439652)Instructions burned: 325 (million)
% 21.15/3.97 % (1439651)------------------------------
% 21.15/3.97 % (1439651)------------------------------
% 21.15/3.97 % (1439658)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1350518217:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 21.15/3.97 % (1439659)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=654274232:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 21.15/3.97 % (1439660)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=788257615:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 21.15/3.97 % (1439661)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3369419866:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 21.15/3.97 % (1439660)Instruction limit reached!
% 21.15/3.97 % (1439660)------------------------------
% 21.15/3.97 % (1439660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439660)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439660)Termination reason: Instruction limit
% 21.15/3.97 % (1439660)Termination phase: Saturation
% 21.15/3.97 % (1439660)Time elapsed: 0.064 s
% 21.15/3.97 % (1439660)Peak memory usage: 92 MB
% 21.15/3.97 % (1439660)Instructions burned: 113 (million)
% 21.15/3.97 % (1439661)Instruction limit reached!
% 21.15/3.97 % (1439661)------------------------------
% 21.15/3.97 % (1439661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439661)CaDiCaL version: 2.1.3
% 21.15/3.97 % (1439661)Termination reason: Instruction limit
% 21.15/3.97 % (1439661)Termination phase: Saturation
% 21.15/3.97 % (1439661)Time elapsed: 0.072 s
% 21.15/3.97 % (1439661)Peak memory usage: 91 MB
% 21.15/3.97 % (1439661)Instructions burned: 129 (million)
% 21.15/3.97 % (1439658)Instruction limit reached!
% 21.15/3.97 % (1439658)------------------------------
% 21.15/3.97 % (1439658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.15/3.97 % (1439658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.15/3.97 % (1439658)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439658)Termination reason: Instruction limit
% 60.13/9.36 % (1439658)Termination phase: Saturation
% 60.13/9.36 % (1439658)Time elapsed: 0.183 s
% 60.13/9.36 % (1439658)Peak memory usage: 93 MB
% 60.13/9.36 % (1439658)Instructions burned: 294 (million)
% 60.13/9.36 % (1439666)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1230692918:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 60.13/9.36 % (1439667)lrs+10_1_sil=8000:sp=occurrence:random_seed=3104865240:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 60.13/9.36 % (1439668)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2104160556:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 60.13/9.36 % (1439666)Instruction limit reached!
% 60.13/9.36 % (1439666)------------------------------
% 60.13/9.36 % (1439666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.36 % (1439666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.36 % (1439666)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439666)Termination reason: Instruction limit
% 60.13/9.36 % (1439666)Termination phase: Saturation
% 60.13/9.36 % (1439666)Time elapsed: 0.069 s
% 60.13/9.36 % (1439666)Peak memory usage: 89 MB
% 60.13/9.36 % (1439666)Instructions burned: 115 (million)
% 60.13/9.36 % (1439672)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1851322931:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 60.13/9.36 % (1439668)Instruction limit reached!
% 60.13/9.36 % (1439668)------------------------------
% 60.13/9.36 % (1439668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.36 % (1439668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.36 % (1439668)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439668)Termination reason: Instruction limit
% 60.13/9.36 % (1439668)Termination phase: Saturation
% 60.13/9.36 % (1439668)Time elapsed: 0.265 s
% 60.13/9.36 % (1439668)Peak memory usage: 95 MB
% 60.13/9.36 % (1439668)Instructions burned: 438 (million)
% 60.13/9.36 % (1439674)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1040610546:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 60.13/9.36 % (1439674)Instruction limit reached!
% 60.13/9.36 % (1439674)------------------------------
% 60.13/9.36 % (1439674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.36 % (1439674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.36 % (1439674)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439674)Termination reason: Instruction limit
% 60.13/9.36 % (1439674)Termination phase: Saturation
% 60.13/9.36 % (1439674)Time elapsed: 0.069 s
% 60.13/9.36 % (1439674)Peak memory usage: 92 MB
% 60.13/9.36 % (1439674)Instructions burned: 135 (million)
% 60.13/9.36 % (1439667)Instruction limit reached!
% 60.13/9.36 % (1439667)------------------------------
% 60.13/9.36 % (1439667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.36 % (1439667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.36 % (1439667)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439667)Termination reason: Instruction limit
% 60.13/9.36 % (1439667)Termination phase: Saturation
% 60.13/9.36 % (1439667)Time elapsed: 0.570 s
% 60.13/9.36 % (1439667)Peak memory usage: 105 MB
% 60.13/9.36 % (1439667)Instructions burned: 908 (million)
% 60.13/9.36 % (1439676)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=464384236:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 60.13/9.36 % (1439677)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4236601970:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 60.13/9.36 % (1439676)Instruction limit reached!
% 60.13/9.36 % (1439676)------------------------------
% 60.13/9.36 % (1439676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.13/9.36 % (1439676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.13/9.36 % (1439676)CaDiCaL version: 2.1.3
% 60.13/9.36 % (1439676)Termination reason: Instruction limit
% 60.13/9.36 % (1439676)Termination phase: Saturation
% 60.13/9.36 % (1439676)Time elapsed: 0.356 s
% 60.13/9.36 % (1439676)Peak memory usage: 100 MB
% 60.13/9.36 % (1439676)Instructions burned: 592 (million)
% 60.13/9.36 % (1439681)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=4215874306:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 83.11/12.64 % (1439659)Instruction limit reached!
% 83.11/12.64 % (1439659)------------------------------
% 83.11/12.64 % (1439659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439659)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439659)Termination reason: Instruction limit
% 83.11/12.64 % (1439659)Termination phase: Saturation
% 83.11/12.64 % (1439659)Time elapsed: 1.480 s
% 83.11/12.64 % (1439659)Peak memory usage: 154 MB
% 83.11/12.64 % (1439659)Instructions burned: 2351 (million)
% 83.11/12.64 % (1439681)Instruction limit reached!
% 83.11/12.64 % (1439681)------------------------------
% 83.11/12.64 % (1439681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439681)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439681)Termination reason: Instruction limit
% 83.11/12.64 % (1439681)Termination phase: Saturation
% 83.11/12.64 % (1439681)Time elapsed: 0.070 s
% 83.11/12.64 % (1439681)Peak memory usage: 92 MB
% 83.11/12.64 % (1439681)Instructions burned: 125 (million)
% 83.11/12.64 % (1439683)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3992620096:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 83.11/12.64 % (1439684)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3817245958:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 83.11/12.64 % (1439683)Instruction limit reached!
% 83.11/12.64 % (1439683)------------------------------
% 83.11/12.64 % (1439683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439683)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439683)Termination reason: Instruction limit
% 83.11/12.64 % (1439683)Termination phase: Saturation
% 83.11/12.64 % (1439683)Time elapsed: 0.074 s
% 83.11/12.64 % (1439683)Peak memory usage: 92 MB
% 83.11/12.64 % (1439683)Instructions burned: 134 (million)
% 83.11/12.64 % (1439684)Instruction limit reached!
% 83.11/12.64 % (1439684)------------------------------
% 83.11/12.64 % (1439684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439684)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439684)Termination reason: Instruction limit
% 83.11/12.64 % (1439684)Termination phase: Saturation
% 83.11/12.64 % (1439684)Time elapsed: 0.073 s
% 83.11/12.64 % (1439684)Peak memory usage: 92 MB
% 83.11/12.64 % (1439684)Instructions burned: 141 (million)
% 83.11/12.64 % (1439687)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2144668467:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 83.11/12.64 % (1439688)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=2776371489:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 83.11/12.64 % (1439687)Instruction limit reached!
% 83.11/12.64 % (1439687)------------------------------
% 83.11/12.64 % (1439687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439687)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439687)Termination reason: Instruction limit
% 83.11/12.64 % (1439687)Termination phase: Saturation
% 83.11/12.64 % (1439687)Time elapsed: 0.255 s
% 83.11/12.64 % (1439687)Peak memory usage: 96 MB
% 83.11/12.64 % (1439687)Instructions burned: 432 (million)
% 83.11/12.64 % (1439691)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=3885445148:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 83.11/12.64 % (1439691)Instruction limit reached!
% 83.11/12.64 % (1439691)------------------------------
% 83.11/12.64 % (1439691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.11/12.64 % (1439691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.11/12.64 % (1439691)CaDiCaL version: 2.1.3
% 83.11/12.64 % (1439691)Termination reason: Instruction limit
% 75.40/13.25 % (1439691)Termination phase: Saturation
% 75.40/13.25 % (1439691)Time elapsed: 0.083 s
% 75.40/13.25 % (1439691)Peak memory usage: 92 MB
% 75.40/13.25 % (1439691)Instructions burned: 151 (million)
% 75.40/13.25 % (1439693)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=997481584:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 75.40/13.25 % (1439672)Instruction limit reached!
% 75.40/13.25 % (1439672)------------------------------
% 75.40/13.25 % (1439672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439672)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439672)Termination reason: Instruction limit
% 75.40/13.25 % (1439672)Termination phase: Saturation
% 75.40/13.25 % (1439672)Time elapsed: 3.169 s
% 75.40/13.25 % (1439672)Peak memory usage: 157 MB
% 75.40/13.25 % (1439672)Instructions burned: 5203 (million)
% 75.40/13.25 % (1439695)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1927094570:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 75.40/13.25 % (1439695)Instruction limit reached!
% 75.40/13.25 % (1439695)------------------------------
% 75.40/13.25 % (1439695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439695)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439695)Termination reason: Instruction limit
% 75.40/13.25 % (1439695)Termination phase: Saturation
% 75.40/13.25 % (1439695)Time elapsed: 0.320 s
% 75.40/13.25 % (1439695)Peak memory usage: 93 MB
% 75.40/13.25 % (1439695)Instructions burned: 669 (million)
% 75.40/13.25 % (1439697)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=382073800:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 75.40/13.25 % (1439697)Instruction limit reached!
% 75.40/13.25 % (1439697)------------------------------
% 75.40/13.25 % (1439697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439697)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439697)Termination reason: Instruction limit
% 75.40/13.25 % (1439697)Termination phase: Saturation
% 75.40/13.25 % (1439697)Time elapsed: 0.098 s
% 75.40/13.25 % (1439697)Peak memory usage: 93 MB
% 75.40/13.25 % (1439697)Instructions burned: 187 (million)
% 75.40/13.25 % (1439699)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=455161559:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi)
% 75.40/13.25 % (1439699)Instruction limit reached!
% 75.40/13.25 % (1439699)------------------------------
% 75.40/13.25 % (1439699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439699)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439699)Termination reason: Instruction limit
% 75.40/13.25 % (1439699)Termination phase: Saturation
% 75.40/13.25 % (1439699)Time elapsed: 0.111 s
% 75.40/13.25 % (1439699)Peak memory usage: 95 MB
% 75.40/13.25 % (1439699)Instructions burned: 193 (million)
% 75.40/13.25 % (1439701)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3047668715:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2945 on theBenchmark for (2945ds/4850Mi)
% 75.40/13.25 % (1439688)Instruction limit reached!
% 75.40/13.25 % (1439688)------------------------------
% 75.40/13.25 % (1439688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439688)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439688)Termination reason: Instruction limit
% 75.40/13.25 % (1439688)Termination phase: Saturation
% 75.40/13.25 % (1439688)Time elapsed: 3.900 s
% 75.40/13.25 % (1439688)Peak memory usage: 178 MB
% 75.40/13.25 % (1439688)Instructions burned: 6060 (million)
% 75.40/13.25 % (1439703)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1481003122:i=12111:sd=1:ss=included_2933 on theBenchmark for (2933ds/12111Mi)
% 75.40/13.25 % (1439701)Instruction limit reached!
% 75.40/13.25 % (1439701)------------------------------
% 75.40/13.25 % (1439701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439701)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439701)Termination reason: Instruction limit
% 75.40/13.25 % (1439701)Termination phase: Saturation
% 75.40/13.25 % (1439701)Time elapsed: 2.934 s
% 75.40/13.25 % (1439701)Peak memory usage: 146 MB
% 75.40/13.25 % (1439701)Instructions burned: 4851 (million)
% 75.40/13.25 % (1439705)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=450691933:i=319:kws=precedence:fsr=off_2914 on theBenchmark for (2914ds/319Mi)
% 75.40/13.25 % (1439705)Instruction limit reached!
% 75.40/13.25 % (1439705)------------------------------
% 75.40/13.25 % (1439705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439705)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439705)Termination reason: Instruction limit
% 75.40/13.25 % (1439705)Termination phase: Saturation
% 75.40/13.25 % (1439705)Time elapsed: 0.171 s
% 75.40/13.25 % (1439705)Peak memory usage: 96 MB
% 75.40/13.25 % (1439705)Instructions burned: 321 (million)
% 75.40/13.25 % (1439707)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2355731833:i=2064:ep=RST_2911 on theBenchmark for (2911ds/2064Mi)
% 75.40/13.25 % (1439677)Instruction limit reached!
% 75.40/13.25 % (1439677)------------------------------
% 75.40/13.25 % (1439677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439677)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439677)Termination reason: Instruction limit
% 75.40/13.25 % (1439677)Termination phase: Saturation
% 75.40/13.25 % (1439677)Time elapsed: 7.876 s
% 75.40/13.25 % (1439677)Peak memory usage: 229 MB
% 75.40/13.25 % (1439677)Instructions burned: 13195 (million)
% 75.40/13.25 % (1439709)dis-1011_128_sil=32000:random_seed=2113927222:i=3706:ep=RST:av=off_2903 on theBenchmark for (2903ds/3706Mi)
% 75.40/13.25 % (1439707)Instruction limit reached!
% 75.40/13.25 % (1439707)------------------------------
% 75.40/13.25 % (1439707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439707)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439707)Termination reason: Instruction limit
% 75.40/13.25 % (1439707)Termination phase: Saturation
% 75.40/13.25 % (1439707)Time elapsed: 1.140 s
% 75.40/13.25 % (1439707)Peak memory usage: 125 MB
% 75.40/13.25 % (1439707)Instructions burned: 2065 (million)
% 75.40/13.25 % (1439711)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3299953092:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2898 on theBenchmark for (2898ds/757Mi)
% 75.40/13.25 % (1439711)Instruction limit reached!
% 75.40/13.25 % (1439711)------------------------------
% 75.40/13.25 % (1439711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439711)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439711)Termination reason: Instruction limit
% 75.40/13.25 % (1439711)Termination phase: Saturation
% 75.40/13.25 % (1439711)Time elapsed: 0.519 s
% 75.40/13.25 % (1439711)Peak memory usage: 109 MB
% 75.40/13.25 % (1439711)Instructions burned: 758 (million)
% 75.40/13.25 % (1439713)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2978764014:i=13913:ss=axioms:sgt=8_2891 on theBenchmark for (2891ds/13913Mi)
% 75.40/13.25 % (1439693)Instruction limit reached!
% 75.40/13.25 % (1439693)------------------------------
% 75.40/13.25 % (1439693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439693)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439693)Termination reason: Instruction limit
% 75.40/13.25 % (1439693)Termination phase: Saturation
% 75.40/13.25 % (1439693)Time elapsed: 7.992 s
% 75.40/13.25 % (1439693)Peak memory usage: 241 MB
% 75.40/13.25 % (1439693)Instructions burned: 14157 (million)
% 75.40/13.25 % (1439715)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2798703195:i=9925:aac=none_2887 on theBenchmark for (2887ds/9925Mi)
% 75.40/13.25 % (1439709)Instruction limit reached!
% 75.40/13.25 % (1439709)------------------------------
% 75.40/13.25 % (1439709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.40/13.25 % (1439709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.40/13.25 % (1439709)CaDiCaL version: 2.1.3
% 75.40/13.25 % (1439709)Termination reason: Instruction limit
% 75.40/13.25 % (1439709)Termination phase: Saturation
% 75.40/13.25 % (1439709)Time elapsed: 1.951 s
% 75.40/13.25 % (1439709)Peak memory usage: 119 MB
% 75.40/13.25 % (1439709)Instructions burned: 3708 (million)
% 75.40/13.25 % (1439717)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2196083109:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2882 on theBenchmark for (2882ds/2479Mi)
% 75.40/13.25 % (1439638)First to succeed.
% 75.40/13.25 % (1439638)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1439631"
% 75.40/13.25 % (1439638)Refutation found. Thanks to Tanya!
% 75.40/13.25 % SZS status Theorem for theBenchmark
% 75.40/13.25 % SZS output start Proof for theBenchmark
% See solution above
% 88.22/13.44 % (1439638)------------------------------
% 88.22/13.44 % (1439638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.22/13.44 % (1439638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.22/13.44 % (1439638)CaDiCaL version: 2.1.3
% 88.22/13.44 % (1439638)Termination reason: Refutation
% 88.22/13.44 % (1439638)Time elapsed: 11.866 s
% 88.22/13.44 % (1439638)Peak memory usage: 274 MB
% 88.22/13.44 % (1439638)Instructions burned: 18837 (million)
% 88.22/13.44 % (1439638)------------------------------
% 88.22/13.44 % (1439638)------------------------------
% 88.22/13.44 % (1439631)Success in time 12.394 s
% 88.22/13.44 % Vampire exiting
%------------------------------------------------------------------------------