%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU352+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 : n005.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 16.16s 3.62s
% Output : Refutation 19.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 27
% Syntax : Number of formulae : 235 ( 22 unt; 12 def)
% Number of atoms : 1220 ( 159 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 1702 ( 717 ~; 796 |; 134 &)
% ( 23 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 11 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-3 aty)
% Number of variables : 278 ( 0 sgn 260 !; 18 ?)
% 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(f40,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_semilatt_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> meet_commut(X0,X1,X2) = meet_commut(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k4_lattices) ).
fof(f51,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( element(X2,the_carrier(X0))
=> ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_lattices) ).
fof(f57,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> ( lower_bounded_semilattstr(X0)
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_lattices) ).
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(f81,axiom,
! [X0] :
( X0 = empty_set
<=> ! [X1] : ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
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(f151,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> element(join_of_latt_set(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f173,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> element(meet(X0,X1,X2),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_lattices) ).
fof(f196,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> element(bottom_of_semilattstr(X0),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f217,axiom,
! [X0] :
( latt_str(X0)
=> ( meet_semilatt_str(X0)
& join_semilatt_str(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f384,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_semilatt_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> meet_commut(X0,X1,X2) = meet(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f512,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> below(X0,meet_commut(X0,X1,X2),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_lattices) ).
fof(f523,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_semilatt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( ( below(X0,X1,X2)
& below(X0,X2,X1) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_lattices) ).
fof(f593,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ( ~ empty_carrier(X0)
& lattice(X0)
& lower_bounded_semilattstr(X0)
& latt_str(X0)
& bottom_of_semilattstr(X0) = join_of_latt_set(X0,empty_set) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_lattice3) ).
fof(f594,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ( ~ empty_carrier(X0)
& lattice(X0)
& lower_bounded_semilattstr(X0)
& latt_str(X0)
& bottom_of_semilattstr(X0) = join_of_latt_set(X0,empty_set) ) ),
inference(negated_conjecture,[status(cth)],[f593]) ).
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(ennf_transformation,[],[f19]) ).
fof(f727,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,[],[f726]) ).
fof(f751,plain,
! [X0,X1,X2] :
( meet_commut(X0,X1,X2) = meet_commut(X0,X2,X1)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f752,plain,
! [X0,X1,X2] :
( meet_commut(X0,X1,X2) = meet_commut(X0,X2,X1)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f751]) ).
fof(f767,plain,
! [X0] :
( ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f768,plain,
! [X0] :
( ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f767]) ).
fof(f776,plain,
! [X0] :
( ! [X1] :
( ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f777,plain,
! [X0] :
( ! [X1] :
( ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f776]) ).
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(ennf_transformation,[],[f59]) ).
fof(f780,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,[],[f779]) ).
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(ennf_transformation,[],[f83]) ).
fof(f808,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,[],[f807]) ).
fof(f886,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f151]) ).
fof(f887,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f886]) ).
fof(f903,plain,
! [X0,X1,X2] :
( element(meet(X0,X1,X2),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f173]) ).
fof(f904,plain,
! [X0,X1,X2] :
( element(meet(X0,X1,X2),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f903]) ).
fof(f922,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f196]) ).
fof(f923,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f922]) ).
fof(f946,plain,
! [X0] :
( ( meet_semilatt_str(X0)
& join_semilatt_str(X0) )
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f217]) ).
fof(f1106,plain,
! [X0,X1,X2] :
( meet_commut(X0,X1,X2) = meet(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f384]) ).
fof(f1107,plain,
! [X0,X1,X2] :
( meet_commut(X0,X1,X2) = meet(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f1106]) ).
fof(f1297,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( below(X0,meet_commut(X0,X1,X2),X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f512]) ).
fof(f1298,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( below(X0,meet_commut(X0,X1,X2),X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f1297]) ).
fof(f1318,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ below(X0,X1,X2)
| ~ below(X0,X2,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0) ),
inference(ennf_transformation,[],[f523]) ).
fof(f1319,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ below(X0,X1,X2)
| ~ below(X0,X2,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0) ),
inference(flattening,[],[f1318]) ).
fof(f1399,plain,
? [X0] :
( ( empty_carrier(X0)
| ~ lattice(X0)
| ~ lower_bounded_semilattstr(X0)
| ~ latt_str(X0)
| bottom_of_semilattstr(X0) != join_of_latt_set(X0,empty_set) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(ennf_transformation,[],[f594]) ).
fof(f1400,plain,
? [X0] :
( ( empty_carrier(X0)
| ~ lattice(X0)
| ~ lower_bounded_semilattstr(X0)
| ~ latt_str(X0)
| bottom_of_semilattstr(X0) != join_of_latt_set(X0,empty_set) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(flattening,[],[f1399]) ).
fof(f1580,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) ) )
& ( ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(nnf_transformation,[],[f768]) ).
fof(f1581,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& ! [X4] :
( ( meet(X0,X3,X4) = X3
& meet(X0,X4,X3) = X3 )
| ~ element(X4,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(rectify,[],[f1580]) ).
fof(f1582,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ( ( meet(X0,X1,sK65(X0,X1)) != X1
| meet(X0,sK65(X0,X1),X1) != X1 )
& element(sK65(X0,X1),the_carrier(X0)) ) ) )
& ( ( element(sK66(X0),the_carrier(X0))
& ! [X4] :
( ( sK66(X0) = meet(X0,sK66(X0),X4)
& sK66(X0) = meet(X0,X4,sK66(X0)) )
| ~ element(X4,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65,sK66]),skolemize(X2,sK65(X0,X1)),skolemize(X3,sK66(X0))],[f1581]) ).
fof(f1599,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) )
& ( ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(nnf_transformation,[],[f777]) ).
fof(f1600,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) )
& ( ! [X3] :
( ( meet(X0,X1,X3) = X1
& meet(X0,X3,X1) = X1 )
| ~ element(X3,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(rectify,[],[f1599]) ).
fof(f1601,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ( ( meet(X0,X1,sK77(X0,X1)) != X1
| meet(X0,sK77(X0,X1),X1) != X1 )
& element(sK77(X0,X1),the_carrier(X0)) ) )
& ( ! [X3] :
( ( meet(X0,X1,X3) = X1
& meet(X0,X3,X1) = X1 )
| ~ element(X3,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77]),skolemize(X2,sK77(X0,X1))],[f1600]) ).
fof(f1603,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,[],[f780]) ).
fof(f1604,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,[],[f1603]) ).
fof(f1605,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ( ~ below(X0,sK78(X0,X1,X2),X1)
& in(sK78(X0,X1,X2),X2)
& element(sK78(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,[sK78]),skolemize(X3,sK78(X0,X1,X2))],[f1604]) ).
fof(f1657,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X1] : ~ in(X1,X0)
| empty_set != X0 ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f1658,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(rectify,[],[f1657]) ).
fof(f1659,plain,
! [X0] :
( ( X0 = empty_set
| in(sK103(X0),X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103]),skolemize(X1,sK103(X0))],[f1658]) ).
fof(f1663,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,[],[f808]) ).
fof(f1664,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,[],[f1663]) ).
fof(f1665,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,[],[f1664]) ).
fof(f1666,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ( ~ below(X0,X2,sK105(X0,X1,X2))
& latt_element_smaller(X0,sK105(X0,X1,X2),X1)
& element(sK105(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,[sK105]),skolemize(X3,sK105(X0,X1,X2))],[f1665]) ).
fof(f2198,plain,
( ( empty_carrier(sK494)
| ~ lattice(sK494)
| ~ lower_bounded_semilattstr(sK494)
| ~ latt_str(sK494)
| bottom_of_semilattstr(sK494) != join_of_latt_set(sK494,empty_set) )
& ~ empty_carrier(sK494)
& lattice(sK494)
& complete_latt_str(sK494)
& latt_str(sK494) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK494]),skolemize(X0,sK494)],[f1400]) ).
fof(f2253,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f2255,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_commutative(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f2257,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| join_commutative(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f2295,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| meet_commut(X0,X1,X2) = meet_commut(X0,X2,X1) ),
inference(cnf_transformation,[],[f752]) ).
fof(f2339,plain,
! [X0,X1] :
( element(sK65(X0,X1),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1582]) ).
fof(f2340,plain,
! [X0,X1] :
( meet(X0,sK65(X0,X1),X1) != X1
| ~ element(X1,the_carrier(X0))
| meet(X0,X1,sK65(X0,X1)) != X1
| lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1582]) ).
fof(f2373,plain,
! [X3,X0,X1] :
( meet(X0,X3,X1) = X1
| ~ element(X3,the_carrier(X0))
| bottom_of_semilattstr(X0) != X1
| ~ element(X1,the_carrier(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1601]) ).
fof(f2381,plain,
! [X2,X0,X1] :
( in(sK78(X0,X1,X2),X2)
| latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1605]) ).
fof(f2472,plain,
! [X2,X0] :
( ~ in(X2,X0)
| empty_set != X0 ),
inference(cnf_transformation,[],[f1659]) ).
fof(f2478,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,[],[f1666]) ).
fof(f2727,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f887]) ).
fof(f2744,plain,
! [X2,X0,X1] :
( element(meet(X0,X1,X2),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f904]) ).
fof(f2761,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f923]) ).
fof(f2780,plain,
! [X0] :
( ~ latt_str(X0)
| join_semilatt_str(X0) ),
inference(cnf_transformation,[],[f946]) ).
fof(f2781,plain,
! [X0] :
( ~ latt_str(X0)
| meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f946]) ).
fof(f3180,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_semilatt_str(X0)
| ~ element(X1,the_carrier(X0))
| meet_commut(X0,X1,X2) = meet(X0,X1,X2) ),
inference(cnf_transformation,[],[f1107]) ).
fof(f3784,plain,
! [X2,X0,X1] :
( below(X0,meet_commut(X0,X1,X2),X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f3799,plain,
! [X2,X0,X1] :
( ~ below(X0,X2,X1)
| ~ below(X0,X1,X2)
| X1 = X2
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1319]) ).
fof(f3929,plain,
latt_str(sK494),
inference(cnf_transformation,[],[f2198]) ).
fof(f3930,plain,
complete_latt_str(sK494),
inference(cnf_transformation,[],[f2198]) ).
fof(f3931,plain,
lattice(sK494),
inference(cnf_transformation,[],[f2198]) ).
fof(f3932,plain,
~ empty_carrier(sK494),
inference(cnf_transformation,[],[f2198]) ).
fof(f3933,plain,
( empty_carrier(sK494)
| ~ lattice(sK494)
| ~ lower_bounded_semilattstr(sK494)
| ~ latt_str(sK494)
| bottom_of_semilattstr(sK494) != join_of_latt_set(sK494,empty_set) ),
inference(cnf_transformation,[],[f2198]) ).
fof(f4450,plain,
! [X3,X0] :
( bottom_of_semilattstr(X0) = meet(X0,X3,bottom_of_semilattstr(X0))
| ~ element(X3,the_carrier(X0))
| ~ element(bottom_of_semilattstr(X0),the_carrier(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(equality_resolution,[],[f2373]) ).
fof(f4492,plain,
! [X2] : ~ in(X2,empty_set),
inference(equality_resolution,[],[f2472]) ).
fof(f4496,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,[],[f2478]) ).
fof(f4686,definition,
sF503 = bottom_of_semilattstr(sK494),
introduced(definition,[new_symbols(definition,[sF503])],[function_definition]) ).
fof(f4687,plain,
bottom_of_semilattstr(sK494) = sF503,
inference(reorient_equations,[],[f4686]) ).
fof(f4688,definition,
sF504 = join_of_latt_set(sK494,empty_set),
introduced(definition,[new_symbols(definition,[sF504])],[function_definition]) ).
fof(f4689,plain,
join_of_latt_set(sK494,empty_set) = sF504,
inference(reorient_equations,[],[f4688]) ).
fof(f4690,plain,
( empty_carrier(sK494)
| ~ lattice(sK494)
| ~ lower_bounded_semilattstr(sK494)
| ~ latt_str(sK494)
| sF503 != sF504 ),
inference(definition_folding,[],[f3933,f4689,f4687]) ).
fof(f4712,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,[],[f4496]) ).
fof(f4731,plain,
( ~ lattice(sK494)
| ~ lower_bounded_semilattstr(sK494)
| ~ latt_str(sK494)
| sF503 != sF504 ),
inference(forward_subsumption_resolution,[],[f4690,f3932]) ).
fof(f5010,plain,
! [X0,X1,X4] :
( below(X0,join_of_latt_set(X0,X1),X4)
| ~ latt_element_smaller(X0,X4,X1)
| ~ element(X4,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f4712,f2727]) ).
fof(f5022,plain,
! [X3,X0] :
( ~ element(X3,the_carrier(X0))
| bottom_of_semilattstr(X0) = meet(X0,X3,bottom_of_semilattstr(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(forward_subsumption_resolution,[],[f4450,f2761]) ).
fof(f5035,plain,
( ~ lower_bounded_semilattstr(sK494)
| ~ latt_str(sK494)
| sF503 != sF504 ),
inference(forward_subsumption_resolution,[],[f4731,f3931]) ).
fof(f5040,plain,
( ~ lower_bounded_semilattstr(sK494)
| sF503 != sF504 ),
inference(forward_subsumption_resolution,[],[f5035,f3929]) ).
fof(f5042,definition,
( spl505_59
<=> sF503 = sF504 ),
introduced(definition,[new_symbols(definition,[spl505_59])],[avatar_definition]) ).
fof(f5044,plain,
( sF503 != sF504
| spl505_59 ),
inference(avatar_component_clause,[],[f5042]) ).
fof(f5046,definition,
( spl505_60
<=> lower_bounded_semilattstr(sK494) ),
introduced(definition,[new_symbols(definition,[spl505_60])],[avatar_definition]) ).
fof(f5048,plain,
( ~ lower_bounded_semilattstr(sK494)
| spl505_60 ),
inference(avatar_component_clause,[],[f5046]) ).
fof(f5049,plain,
( ~ spl505_59
| ~ spl505_60 ),
inference(avatar_split_clause,[],[f5040,f5046,f5042]) ).
fof(f5050,plain,
( element(sF504,the_carrier(sK494))
| empty_carrier(sK494)
| ~ latt_str(sK494) ),
inference(superposition,[],[f2727,f4689]) ).
fof(f5051,plain,
( element(sF504,the_carrier(sK494))
| ~ latt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f5050,f3932]) ).
fof(f5052,plain,
element(sF504,the_carrier(sK494)),
inference(forward_subsumption_resolution,[],[f5051,f3929]) ).
fof(f5053,plain,
( element(sF503,the_carrier(sK494))
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494) ),
inference(superposition,[],[f2761,f4687]) ).
fof(f5054,plain,
( element(sF503,the_carrier(sK494))
| ~ meet_semilatt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f5053,f3932]) ).
fof(f5056,definition,
( spl505_61
<=> meet_semilatt_str(sK494) ),
introduced(definition,[new_symbols(definition,[spl505_61])],[avatar_definition]) ).
fof(f5057,plain,
( meet_semilatt_str(sK494)
| ~ spl505_61 ),
inference(avatar_component_clause,[],[f5056]) ).
fof(f5058,plain,
( ~ meet_semilatt_str(sK494)
| spl505_61 ),
inference(avatar_component_clause,[],[f5056]) ).
fof(f5060,definition,
( spl505_62
<=> element(sF503,the_carrier(sK494)) ),
introduced(definition,[new_symbols(definition,[spl505_62])],[avatar_definition]) ).
fof(f5062,plain,
( element(sF503,the_carrier(sK494))
| ~ spl505_62 ),
inference(avatar_component_clause,[],[f5060]) ).
fof(f5063,plain,
( ~ spl505_61
| spl505_62 ),
inference(avatar_split_clause,[],[f5054,f5060,f5056]) ).
fof(f5074,plain,
meet_semilatt_str(sK494),
inference(resolution,[],[f2781,f3929]) ).
fof(f5075,plain,
( $false
| spl505_61 ),
inference(forward_subsumption_resolution,[],[f5074,f5058]) ).
fof(f5076,plain,
spl505_61,
inference(avatar_contradiction_clause,[],[f5075]) ).
fof(f5121,definition,
( spl505_65
<=> meet_commutative(sK494) ),
introduced(definition,[new_symbols(definition,[spl505_65])],[avatar_definition]) ).
fof(f5122,plain,
( meet_commutative(sK494)
| ~ spl505_65 ),
inference(avatar_component_clause,[],[f5121]) ).
fof(f5153,plain,
( bottom_of_semilattstr(sK494) = meet(sK494,sF504,bottom_of_semilattstr(sK494))
| ~ lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494) ),
inference(resolution,[],[f5022,f5052]) ).
fof(f5157,plain,
( bottom_of_semilattstr(sK494) = meet(sK494,sF504,bottom_of_semilattstr(sK494))
| ~ lower_bounded_semilattstr(sK494)
| ~ meet_semilatt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f5153,f3932]) ).
fof(f5161,plain,
( bottom_of_semilattstr(sK494) = meet(sK494,sF504,bottom_of_semilattstr(sK494))
| ~ lower_bounded_semilattstr(sK494)
| ~ spl505_61 ),
inference(forward_subsumption_resolution,[],[f5157,f5057]) ).
fof(f5163,plain,
( sF503 = meet(sK494,sF504,sF503)
| ~ lower_bounded_semilattstr(sK494)
| ~ spl505_61 ),
inference(forward_demodulation,[],[f5161,f4687]) ).
fof(f5166,definition,
( spl505_67
<=> sF503 = meet(sK494,sF504,sF503) ),
introduced(definition,[new_symbols(definition,[spl505_67])],[avatar_definition]) ).
fof(f5168,plain,
( sF503 = meet(sK494,sF504,sF503)
| ~ spl505_67 ),
inference(avatar_component_clause,[],[f5166]) ).
fof(f5169,plain,
( ~ spl505_60
| spl505_67
| ~ spl505_61 ),
inference(avatar_split_clause,[],[f5163,f5056,f5166,f5046]) ).
fof(f5280,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,join_of_latt_set(X0,X2))
| join_of_latt_set(X0,X2) = X1
| ~ element(join_of_latt_set(X0,X2),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0)
| ~ latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(resolution,[],[f3799,f5010]) ).
fof(f5284,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,join_of_latt_set(X0,X2))
| join_of_latt_set(X0,X2) = X1
| ~ element(join_of_latt_set(X0,X2),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0)
| ~ latt_element_smaller(X0,X1,X2)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(duplicate_literal_removal,[],[f5280]) ).
fof(f5286,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,join_of_latt_set(X0,X2))
| join_of_latt_set(X0,X2) = X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_commutative(X0)
| ~ join_semilatt_str(X0)
| ~ latt_element_smaller(X0,X1,X2)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f5284,f2727]) ).
fof(f5288,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,join_of_latt_set(X0,X2))
| join_of_latt_set(X0,X2) = X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ join_semilatt_str(X0)
| ~ latt_element_smaller(X0,X1,X2)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f5286,f2257]) ).
fof(f5290,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,join_of_latt_set(X0,X2))
| join_of_latt_set(X0,X2) = X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_element_smaller(X0,X1,X2)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f5288,f2780]) ).
fof(f5333,plain,
( empty_carrier(sK494)
| meet_commutative(sK494)
| ~ latt_str(sK494) ),
inference(resolution,[],[f2255,f3931]) ).
fof(f5334,plain,
( meet_commutative(sK494)
| ~ latt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f5333,f3932]) ).
fof(f5335,plain,
meet_commutative(sK494),
inference(forward_subsumption_resolution,[],[f5334,f3929]) ).
fof(f5336,plain,
spl505_65,
inference(avatar_split_clause,[],[f5335,f5121]) ).
fof(f5718,plain,
( ! [X0] :
( empty_carrier(sK494)
| ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF503) = meet(sK494,X0,sF503) )
| ~ spl505_62 ),
inference(resolution,[],[f3180,f5062]) ).
fof(f5719,plain,
! [X0] :
( empty_carrier(sK494)
| ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet(sK494,X0,sF504) ),
inference(resolution,[],[f3180,f5052]) ).
fof(f5726,plain,
! [X0] :
( ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet(sK494,X0,sF504) ),
inference(forward_subsumption_resolution,[],[f5719,f3932]) ).
fof(f5727,plain,
( ! [X0] :
( ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF503) = meet(sK494,X0,sF503) )
| ~ spl505_62 ),
inference(forward_subsumption_resolution,[],[f5718,f3932]) ).
fof(f5731,plain,
( ! [X0] :
( ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet(sK494,X0,sF504) )
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f5726,f5122]) ).
fof(f5732,plain,
( ! [X0] :
( ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF503) = meet(sK494,X0,sF503) )
| ~ spl505_62
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f5727,f5122]) ).
fof(f5734,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet(sK494,X0,sF504) )
| ~ spl505_61
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f5731,f5057]) ).
fof(f5735,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF503) = meet(sK494,X0,sF503) )
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f5732,f5057]) ).
fof(f5766,plain,
( meet(sK494,sF504,sF503) = meet_commut(sK494,sF504,sF503)
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65 ),
inference(resolution,[],[f5735,f5052]) ).
fof(f6175,plain,
! [X2,X0,X1] :
( ~ element(X0,the_carrier(X1))
| ~ element(join_of_latt_set(X1,X2),the_carrier(X1))
| empty_carrier(X1)
| ~ meet_commutative(X1)
| ~ meet_absorbing(X1)
| ~ latt_str(X1)
| join_of_latt_set(X1,X2) = meet_commut(X1,join_of_latt_set(X1,X2),X0)
| ~ element(meet_commut(X1,join_of_latt_set(X1,X2),X0),the_carrier(X1))
| empty_carrier(X1)
| ~ latt_element_smaller(X1,meet_commut(X1,join_of_latt_set(X1,X2),X0),X2)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1) ),
inference(resolution,[],[f3784,f5290]) ).
fof(f6184,plain,
! [X2,X0,X1] :
( ~ element(X0,the_carrier(X1))
| ~ element(join_of_latt_set(X1,X2),the_carrier(X1))
| empty_carrier(X1)
| ~ meet_commutative(X1)
| ~ meet_absorbing(X1)
| ~ latt_str(X1)
| join_of_latt_set(X1,X2) = meet_commut(X1,join_of_latt_set(X1,X2),X0)
| ~ element(meet_commut(X1,join_of_latt_set(X1,X2),X0),the_carrier(X1))
| ~ latt_element_smaller(X1,meet_commut(X1,join_of_latt_set(X1,X2),X0),X2)
| ~ lattice(X1)
| ~ complete_latt_str(X1) ),
inference(duplicate_literal_removal,[],[f6175]) ).
fof(f6192,plain,
! [X2,X0,X1] :
( ~ element(X0,the_carrier(X1))
| empty_carrier(X1)
| ~ meet_commutative(X1)
| ~ meet_absorbing(X1)
| ~ latt_str(X1)
| join_of_latt_set(X1,X2) = meet_commut(X1,join_of_latt_set(X1,X2),X0)
| ~ element(meet_commut(X1,join_of_latt_set(X1,X2),X0),the_carrier(X1))
| ~ latt_element_smaller(X1,meet_commut(X1,join_of_latt_set(X1,X2),X0),X2)
| ~ lattice(X1)
| ~ complete_latt_str(X1) ),
inference(forward_subsumption_resolution,[],[f6184,f2727]) ).
fof(f6199,plain,
! [X2,X0,X1] :
( ~ element(X0,the_carrier(X1))
| empty_carrier(X1)
| ~ meet_absorbing(X1)
| ~ latt_str(X1)
| join_of_latt_set(X1,X2) = meet_commut(X1,join_of_latt_set(X1,X2),X0)
| ~ element(meet_commut(X1,join_of_latt_set(X1,X2),X0),the_carrier(X1))
| ~ latt_element_smaller(X1,meet_commut(X1,join_of_latt_set(X1,X2),X0),X2)
| ~ lattice(X1)
| ~ complete_latt_str(X1) ),
inference(forward_subsumption_resolution,[],[f6192,f2255]) ).
fof(f6204,plain,
! [X2,X0,X1] :
( ~ latt_element_smaller(X1,meet_commut(X1,join_of_latt_set(X1,X2),X0),X2)
| empty_carrier(X1)
| ~ latt_str(X1)
| join_of_latt_set(X1,X2) = meet_commut(X1,join_of_latt_set(X1,X2),X0)
| ~ element(meet_commut(X1,join_of_latt_set(X1,X2),X0),the_carrier(X1))
| ~ element(X0,the_carrier(X1))
| ~ lattice(X1)
| ~ complete_latt_str(X1) ),
inference(forward_subsumption_resolution,[],[f6199,f2253]) ).
fof(f6325,definition,
( spl505_88
<=> element(sK65(sK494,sF504),the_carrier(sK494)) ),
introduced(definition,[new_symbols(definition,[spl505_88])],[avatar_definition]) ).
fof(f6326,plain,
( element(sK65(sK494,sF504),the_carrier(sK494))
| ~ spl505_88 ),
inference(avatar_component_clause,[],[f6325]) ).
fof(f6327,plain,
( ~ element(sK65(sK494,sF504),the_carrier(sK494))
| spl505_88 ),
inference(avatar_component_clause,[],[f6325]) ).
fof(f6370,plain,
( ~ element(sF504,the_carrier(sK494))
| lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| spl505_88 ),
inference(resolution,[],[f6327,f2339]) ).
fof(f6371,plain,
( lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| spl505_88 ),
inference(forward_subsumption_resolution,[],[f6370,f5052]) ).
fof(f6372,plain,
( empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| spl505_60
| spl505_88 ),
inference(forward_subsumption_resolution,[],[f6371,f5048]) ).
fof(f6373,plain,
( ~ meet_semilatt_str(sK494)
| spl505_60
| spl505_88 ),
inference(forward_subsumption_resolution,[],[f6372,f3932]) ).
fof(f6374,plain,
( $false
| spl505_60
| ~ spl505_61
| spl505_88 ),
inference(forward_subsumption_resolution,[],[f6373,f5057]) ).
fof(f6375,plain,
( spl505_60
| ~ spl505_61
| spl505_88 ),
inference(avatar_contradiction_clause,[],[f6374]) ).
fof(f6644,plain,
! [X0] :
( ~ latt_element_smaller(sK494,meet_commut(sK494,sF504,X0),empty_set)
| empty_carrier(sK494)
| ~ latt_str(sK494)
| sF504 = meet_commut(sK494,sF504,X0)
| ~ element(meet_commut(sK494,sF504,X0),the_carrier(sK494))
| ~ element(X0,the_carrier(sK494))
| ~ lattice(sK494)
| ~ complete_latt_str(sK494) ),
inference(superposition,[],[f6204,f4689]) ).
fof(f6647,plain,
! [X0] :
( ~ latt_element_smaller(sK494,meet_commut(sK494,sF504,X0),empty_set)
| ~ latt_str(sK494)
| sF504 = meet_commut(sK494,sF504,X0)
| ~ element(meet_commut(sK494,sF504,X0),the_carrier(sK494))
| ~ element(X0,the_carrier(sK494))
| ~ lattice(sK494)
| ~ complete_latt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f6644,f3932]) ).
fof(f6649,plain,
! [X0] :
( ~ latt_element_smaller(sK494,meet_commut(sK494,sF504,X0),empty_set)
| sF504 = meet_commut(sK494,sF504,X0)
| ~ element(meet_commut(sK494,sF504,X0),the_carrier(sK494))
| ~ element(X0,the_carrier(sK494))
| ~ lattice(sK494)
| ~ complete_latt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f6647,f3929]) ).
fof(f6651,plain,
! [X0] :
( ~ latt_element_smaller(sK494,meet_commut(sK494,sF504,X0),empty_set)
| sF504 = meet_commut(sK494,sF504,X0)
| ~ element(meet_commut(sK494,sF504,X0),the_carrier(sK494))
| ~ element(X0,the_carrier(sK494))
| ~ complete_latt_str(sK494) ),
inference(forward_subsumption_resolution,[],[f6649,f3931]) ).
fof(f6653,plain,
! [X0] :
( ~ latt_element_smaller(sK494,meet_commut(sK494,sF504,X0),empty_set)
| sF504 = meet_commut(sK494,sF504,X0)
| ~ element(meet_commut(sK494,sF504,X0),the_carrier(sK494))
| ~ element(X0,the_carrier(sK494)) ),
inference(forward_subsumption_resolution,[],[f6651,f3930]) ).
fof(f6655,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sF504,sF503),empty_set)
| sF504 = meet(sK494,sF504,sF503)
| ~ element(meet(sK494,sF504,sF503),the_carrier(sK494))
| ~ element(sF503,the_carrier(sK494))
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65 ),
inference(superposition,[],[f6653,f5766]) ).
fof(f6656,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sF504,sF503),empty_set)
| sF504 = meet(sK494,sF504,sF503)
| ~ element(meet(sK494,sF504,sF503),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f6655,f5062]) ).
fof(f6657,plain,
( ~ latt_element_smaller(sK494,sF503,empty_set)
| sF504 = meet(sK494,sF504,sF503)
| ~ element(meet(sK494,sF504,sF503),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_demodulation,[],[f6656,f5168]) ).
fof(f6658,plain,
( sF503 = sF504
| ~ latt_element_smaller(sK494,sF503,empty_set)
| ~ element(meet(sK494,sF504,sF503),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_demodulation,[],[f6657,f5168]) ).
fof(f6659,plain,
( ~ latt_element_smaller(sK494,sF503,empty_set)
| ~ element(meet(sK494,sF504,sF503),the_carrier(sK494))
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_subsumption_resolution,[],[f6658,f5044]) ).
fof(f6660,plain,
( ~ element(sF503,the_carrier(sK494))
| ~ latt_element_smaller(sK494,sF503,empty_set)
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_demodulation,[],[f6659,f5168]) ).
fof(f6661,plain,
( ~ latt_element_smaller(sK494,sF503,empty_set)
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_subsumption_resolution,[],[f6660,f5062]) ).
fof(f7108,plain,
! [X0] :
( empty_carrier(sK494)
| ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet_commut(sK494,sF504,X0) ),
inference(resolution,[],[f2295,f5052]) ).
fof(f7119,plain,
! [X0] :
( ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet_commut(sK494,sF504,X0) ),
inference(forward_subsumption_resolution,[],[f7108,f3932]) ).
fof(f7127,plain,
( ! [X0] :
( ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet_commut(sK494,sF504,X0) )
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f7119,f5122]) ).
fof(f7133,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sF504) = meet_commut(sK494,sF504,X0) )
| ~ spl505_61
| ~ spl505_65 ),
inference(forward_subsumption_resolution,[],[f7127,f5057]) ).
fof(f8783,plain,
( meet_commut(sK494,sK65(sK494,sF504),sF504) = meet(sK494,sK65(sK494,sF504),sF504)
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(resolution,[],[f6326,f5734]) ).
fof(f8787,plain,
( meet_commut(sK494,sK65(sK494,sF504),sF504) = meet_commut(sK494,sF504,sK65(sK494,sF504))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(resolution,[],[f6326,f7133]) ).
fof(f8792,plain,
( ! [X0] :
( empty_carrier(sK494)
| ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sK65(sK494,sF504)) = meet(sK494,X0,sK65(sK494,sF504)) )
| ~ spl505_88 ),
inference(resolution,[],[f6326,f3180]) ).
fof(f8812,plain,
( ! [X0] :
( ~ meet_commutative(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sK65(sK494,sF504)) = meet(sK494,X0,sK65(sK494,sF504)) )
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f8792,f3932]) ).
fof(f8816,plain,
( meet(sK494,sK65(sK494,sF504),sF504) = meet_commut(sK494,sF504,sK65(sK494,sF504))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_demodulation,[],[f8783,f8787]) ).
fof(f8824,plain,
( ! [X0] :
( ~ meet_semilatt_str(sK494)
| ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sK65(sK494,sF504)) = meet(sK494,X0,sK65(sK494,sF504)) )
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f8812,f5122]) ).
fof(f8834,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK494))
| meet_commut(sK494,X0,sK65(sK494,sF504)) = meet(sK494,X0,sK65(sK494,sF504)) )
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f8824,f5057]) ).
fof(f9009,plain,
( meet_commut(sK494,sF504,sK65(sK494,sF504)) = meet(sK494,sF504,sK65(sK494,sF504))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(resolution,[],[f8834,f5052]) ).
fof(f9010,plain,
( meet(sK494,sK65(sK494,sF504),sF504) = meet(sK494,sF504,sK65(sK494,sF504))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_demodulation,[],[f9009,f8816]) ).
fof(f9250,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sK65(sK494,sF504),sF504),empty_set)
| sF504 = meet(sK494,sK65(sK494,sF504),sF504)
| ~ element(meet(sK494,sK65(sK494,sF504),sF504),the_carrier(sK494))
| ~ element(sK65(sK494,sF504),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(superposition,[],[f6653,f8816]) ).
fof(f9253,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sK65(sK494,sF504),sF504),empty_set)
| sF504 = meet(sK494,sK65(sK494,sF504),sF504)
| ~ element(meet(sK494,sK65(sK494,sF504),sF504),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f9250,f6326]) ).
fof(f9255,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set)
| sF504 = meet(sK494,sK65(sK494,sF504),sF504)
| ~ element(meet(sK494,sK65(sK494,sF504),sF504),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_demodulation,[],[f9253,f9010]) ).
fof(f9257,plain,
( sF504 = meet(sK494,sF504,sK65(sK494,sF504))
| ~ latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set)
| ~ element(meet(sK494,sK65(sK494,sF504),sF504),the_carrier(sK494))
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_demodulation,[],[f9255,f9010]) ).
fof(f9259,plain,
( ~ element(meet(sK494,sF504,sK65(sK494,sF504)),the_carrier(sK494))
| sF504 = meet(sK494,sF504,sK65(sK494,sF504))
| ~ latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set)
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_demodulation,[],[f9257,f9010]) ).
fof(f9262,definition,
( spl505_167
<=> latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set) ),
introduced(definition,[new_symbols(definition,[spl505_167])],[avatar_definition]) ).
fof(f9264,plain,
( ~ latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set)
| spl505_167 ),
inference(avatar_component_clause,[],[f9262]) ).
fof(f9266,definition,
( spl505_168
<=> sF504 = meet(sK494,sF504,sK65(sK494,sF504)) ),
introduced(definition,[new_symbols(definition,[spl505_168])],[avatar_definition]) ).
fof(f9270,definition,
( spl505_169
<=> element(meet(sK494,sF504,sK65(sK494,sF504)),the_carrier(sK494)) ),
introduced(definition,[new_symbols(definition,[spl505_169])],[avatar_definition]) ).
fof(f9271,plain,
( element(meet(sK494,sF504,sK65(sK494,sF504)),the_carrier(sK494))
| ~ spl505_169 ),
inference(avatar_component_clause,[],[f9270]) ).
fof(f9272,plain,
( ~ element(meet(sK494,sF504,sK65(sK494,sF504)),the_carrier(sK494))
| spl505_169 ),
inference(avatar_component_clause,[],[f9270]) ).
fof(f9273,plain,
( ~ spl505_167
| spl505_168
| ~ spl505_169
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(avatar_split_clause,[],[f9259,f6325,f5121,f5056,f9270,f9266,f9262]) ).
fof(f9276,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| ~ element(sF504,the_carrier(sK494))
| sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(superposition,[],[f2340,f9010]) ).
fof(f9278,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| ~ element(sF504,the_carrier(sK494))
| lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(duplicate_literal_removal,[],[f9276]) ).
fof(f9279,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| lower_bounded_semilattstr(sK494)
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f9278,f5052]) ).
fof(f9280,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| spl505_60
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f9279,f5048]) ).
fof(f9281,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| ~ meet_semilatt_str(sK494)
| spl505_60
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f9280,f3932]) ).
fof(f9282,plain,
( sF504 != meet(sK494,sF504,sK65(sK494,sF504))
| spl505_60
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(forward_subsumption_resolution,[],[f9281,f5057]) ).
fof(f9283,plain,
( ~ spl505_168
| spl505_60
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88 ),
inference(avatar_split_clause,[],[f9282,f6325,f5121,f5056,f5046,f9266]) ).
fof(f9883,plain,
( empty_carrier(sK494)
| ~ meet_semilatt_str(sK494)
| ~ element(sF504,the_carrier(sK494))
| ~ element(sK65(sK494,sF504),the_carrier(sK494))
| spl505_169 ),
inference(resolution,[],[f9272,f2744]) ).
fof(f9884,plain,
( ~ meet_semilatt_str(sK494)
| ~ element(sF504,the_carrier(sK494))
| ~ element(sK65(sK494,sF504),the_carrier(sK494))
| spl505_169 ),
inference(forward_subsumption_resolution,[],[f9883,f3932]) ).
fof(f9885,plain,
( ~ element(sF504,the_carrier(sK494))
| ~ element(sK65(sK494,sF504),the_carrier(sK494))
| ~ spl505_61
| spl505_169 ),
inference(forward_subsumption_resolution,[],[f9884,f5057]) ).
fof(f9886,plain,
( ~ element(sK65(sK494,sF504),the_carrier(sK494))
| ~ spl505_61
| spl505_169 ),
inference(forward_subsumption_resolution,[],[f9885,f5052]) ).
fof(f9887,plain,
( $false
| ~ spl505_61
| ~ spl505_88
| spl505_169 ),
inference(forward_subsumption_resolution,[],[f9886,f6326]) ).
fof(f9888,plain,
( ~ spl505_61
| ~ spl505_88
| spl505_169 ),
inference(avatar_contradiction_clause,[],[f9887]) ).
fof(f15501,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| latt_element_smaller(X0,X1,empty_set)
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(resolution,[],[f2381,f4492]) ).
fof(f16012,plain,
( latt_element_smaller(sK494,meet(sK494,sF504,sK65(sK494,sF504)),empty_set)
| empty_carrier(sK494)
| ~ latt_str(sK494)
| ~ spl505_169 ),
inference(resolution,[],[f15501,f9271]) ).
fof(f16044,plain,
( latt_element_smaller(sK494,sF503,empty_set)
| empty_carrier(sK494)
| ~ latt_str(sK494)
| ~ spl505_62 ),
inference(resolution,[],[f15501,f5062]) ).
fof(f16063,plain,
( empty_carrier(sK494)
| ~ latt_str(sK494)
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_subsumption_resolution,[],[f16044,f6661]) ).
fof(f16077,plain,
( empty_carrier(sK494)
| ~ latt_str(sK494)
| spl505_167
| ~ spl505_169 ),
inference(forward_subsumption_resolution,[],[f16012,f9264]) ).
fof(f16094,plain,
( ~ latt_str(sK494)
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_subsumption_resolution,[],[f16063,f3932]) ).
fof(f16103,plain,
( ~ latt_str(sK494)
| spl505_167
| ~ spl505_169 ),
inference(forward_subsumption_resolution,[],[f16077,f3932]) ).
fof(f16118,plain,
( $false
| spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(forward_subsumption_resolution,[],[f16094,f3929]) ).
fof(f16119,plain,
( spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(avatar_contradiction_clause,[],[f16118]) ).
fof(f16122,plain,
( $false
| spl505_167
| ~ spl505_169 ),
inference(forward_subsumption_resolution,[],[f16103,f3929]) ).
fof(f16123,plain,
( spl505_167
| ~ spl505_169 ),
inference(avatar_contradiction_clause,[],[f16122]) ).
cnf(s49,plain,
( ~ spl505_59
| ~ spl505_60 ),
inference(sat_conversion,[],[f5049]) ).
cnf(s50,plain,
( ~ spl505_61
| spl505_62 ),
inference(sat_conversion,[],[f5063]) ).
cnf(s51,plain,
spl505_61,
inference(sat_conversion,[],[f5076]) ).
cnf(s55,plain,
( ~ spl505_60
| ~ spl505_61
| spl505_67 ),
inference(sat_conversion,[],[f5169]) ).
cnf(s58,plain,
spl505_65,
inference(sat_conversion,[],[f5336]) ).
cnf(s81,plain,
( spl505_60
| ~ spl505_61
| spl505_88 ),
inference(sat_conversion,[],[f6375]) ).
cnf(s126,plain,
( ~ spl505_61
| ~ spl505_65
| ~ spl505_88
| ~ spl505_167
| spl505_168
| ~ spl505_169 ),
inference(sat_conversion,[],[f9273]) ).
cnf(s127,plain,
( spl505_60
| ~ spl505_61
| ~ spl505_65
| ~ spl505_88
| ~ spl505_168 ),
inference(sat_conversion,[],[f9283]) ).
cnf(s156,plain,
( ~ spl505_61
| ~ spl505_88
| spl505_169 ),
inference(sat_conversion,[],[f9888]) ).
cnf(s311,plain,
( spl505_59
| ~ spl505_61
| ~ spl505_62
| ~ spl505_65
| ~ spl505_67 ),
inference(sat_conversion,[],[f16119]) ).
cnf(s313,plain,
( spl505_167
| ~ spl505_169 ),
inference(sat_conversion,[],[f16123]) ).
cnf(s325,plain,
spl505_62,
inference(rat,[],[s50,s51]) ).
cnf(s327,plain,
spl505_60,
inference(rat,[],[s126,s313,s127,s156,s81,s58,s51]) ).
cnf(s329,plain,
spl505_67,
inference(rat,[],[s55,s51,s327]) ).
cnf(s330,plain,
~ spl505_59,
inference(rat,[],[s49,s327]) ).
cnf(s334,plain,
$false,
inference(rat,[],[s311,s325,s58,s51,s329,s330]) ).
fof(f16131,plain,
$false,
inference(avatar_sat_refutation,[],[s334]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU352+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n005.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 04:51:17 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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.36/3.04 % (440814)Detected formulas, will run a generic FOF schedule.
% 15.36/3.04 % (440821)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=3011374251:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 15.36/3.04 % (440822)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2194898682:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 15.36/3.04 % (440819)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=1380773947:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 15.36/3.04 % (440823)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1362276414:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 15.36/3.04 % (440824)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4137219069:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 15.36/3.04 % (440825)dis-21_1_sil=8000:lcm=predicate:random_seed=307807235: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.36/3.04 % (440820)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=2622143777:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 15.36/3.04 % (440822)Instruction limit reached!
% 15.36/3.04 % (440822)------------------------------
% 15.36/3.04 % (440822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.36/3.04 % (440822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.36/3.04 % (440822)CaDiCaL version: 2.1.3
% 15.36/3.04 % (440822)Termination reason: Instruction limit
% 15.36/3.04 % (440822)Termination phase: Saturation
% 15.36/3.04 % (440822)Time elapsed: 0.059 s
% 15.36/3.04 % (440822)Peak memory usage: 91 MB
% 15.36/3.04 % (440822)Instructions burned: 110 (million)
% 15.36/3.04 % (440825)Instruction limit reached!
% 15.36/3.04 % (440825)------------------------------
% 15.36/3.04 % (440825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.36/3.04 % (440825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.36/3.04 % (440825)CaDiCaL version: 2.1.3
% 15.36/3.04 % (440825)Termination reason: Instruction limit
% 15.36/3.04 % (440825)Termination phase: Saturation
% 15.36/3.04 % (440825)Time elapsed: 0.065 s
% 15.36/3.04 % (440825)Peak memory usage: 91 MB
% 15.36/3.04 % (440825)Instructions burned: 129 (million)
% 15.36/3.04 % (440823)Instruction limit reached!
% 15.36/3.04 % (440823)------------------------------
% 15.36/3.04 % (440823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.36/3.04 % (440823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.36/3.04 % (440823)CaDiCaL version: 2.1.3
% 15.36/3.04 % (440823)Termination reason: Instruction limit
% 15.36/3.04 % (440823)Termination phase: Saturation
% 15.36/3.04 % (440823)Time elapsed: 0.075 s
% 15.36/3.04 % (440823)Peak memory usage: 91 MB
% 15.36/3.04 % (440823)Instructions burned: 120 (million)
% 15.36/3.04 % (440824)Instruction limit reached!
% 15.36/3.04 % (440824)------------------------------
% 15.36/3.04 % (440824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.36/3.04 % (440824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.36/3.04 % (440824)CaDiCaL version: 2.1.3
% 15.36/3.04 % (440824)Termination reason: Instruction limit
% 15.36/3.04 % (440824)Termination phase: Saturation
% 15.36/3.04 % (440824)Time elapsed: 0.088 s
% 15.36/3.04 % (440824)Peak memory usage: 92 MB
% 15.36/3.04 % (440824)Instructions burned: 140 (million)
% 15.36/3.04 % (440833)lrs+10_1_sil=8000:sp=occurrence:random_seed=3768784480:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 15.36/3.04 % (440835)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1097197194:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.36/3.04 % (440834)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2425532817:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 15.36/3.04 % (440834)Refutation not found, incomplete strategy
% 15.36/3.04 % (440834)------------------------------
% 15.36/3.04 % (440834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.36/3.04 % (440834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440834)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440834)Termination reason: Refutation not found, incomplete strategy
% 16.16/3.62 % (440834)Time elapsed: 0.009 s
% 16.16/3.62 % (440834)Peak memory usage: 89 MB
% 16.16/3.62 % (440834)Instructions burned: 13 (million)
% 16.16/3.62 % (440836)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=2691467544:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 16.16/3.62 % (440833)Instruction limit reached!
% 16.16/3.62 % (440833)------------------------------
% 16.16/3.62 % (440833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440833)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440833)Termination reason: Instruction limit
% 16.16/3.62 % (440833)Termination phase: Saturation
% 16.16/3.62 % (440833)Time elapsed: 0.181 s
% 16.16/3.62 % (440833)Peak memory usage: 95 MB
% 16.16/3.62 % (440833)Instructions burned: 285 (million)
% 16.16/3.62 % (440836)Instruction limit reached!
% 16.16/3.62 % (440836)------------------------------
% 16.16/3.62 % (440836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440836)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440836)Termination reason: Instruction limit
% 16.16/3.62 % (440836)Termination phase: Saturation
% 16.16/3.62 % (440836)Time elapsed: 0.152 s
% 16.16/3.62 % (440836)Peak memory usage: 93 MB
% 16.16/3.62 % (440836)Instructions burned: 249 (million)
% 16.16/3.62 % (440835)Instruction limit reached!
% 16.16/3.62 % (440835)------------------------------
% 16.16/3.62 % (440835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440835)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440835)Termination reason: Instruction limit
% 16.16/3.62 % (440835)Termination phase: Saturation
% 16.16/3.62 % (440835)Time elapsed: 0.222 s
% 16.16/3.62 % (440835)Peak memory usage: 95 MB
% 16.16/3.62 % (440835)Instructions burned: 325 (million)
% 16.16/3.62 % (440834)------------------------------
% 16.16/3.62 % (440834)------------------------------
% 16.16/3.62 % (440841)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3874942954:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 16.16/3.62 % (440842)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2170311280:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 16.16/3.62 % (440843)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2803369254:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 16.16/3.62 % (440844)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=64085911:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 16.16/3.62 % (440843)Instruction limit reached!
% 16.16/3.62 % (440843)------------------------------
% 16.16/3.62 % (440843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440843)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440843)Termination reason: Instruction limit
% 16.16/3.62 % (440843)Termination phase: Saturation
% 16.16/3.62 % (440843)Time elapsed: 0.065 s
% 16.16/3.62 % (440843)Peak memory usage: 92 MB
% 16.16/3.62 % (440843)Instructions burned: 113 (million)
% 16.16/3.62 % (440844)Instruction limit reached!
% 16.16/3.62 % (440844)------------------------------
% 16.16/3.62 % (440844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440844)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440844)Termination reason: Instruction limit
% 16.16/3.62 % (440844)Termination phase: Saturation
% 16.16/3.62 % (440844)Time elapsed: 0.070 s
% 16.16/3.62 % (440844)Peak memory usage: 91 MB
% 16.16/3.62 % (440844)Instructions burned: 127 (million)
% 16.16/3.62 % (440841)Instruction limit reached!
% 16.16/3.62 % (440841)------------------------------
% 16.16/3.62 % (440841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440841)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440841)Termination reason: Instruction limit
% 16.16/3.62 % (440841)Termination phase: Saturation
% 16.16/3.62 % (440841)Time elapsed: 0.184 s
% 16.16/3.62 % (440841)Peak memory usage: 93 MB
% 16.16/3.62 % (440841)Instructions burned: 294 (million)
% 16.16/3.62 % (440849)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1933095905:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 16.16/3.62 % (440850)lrs+10_1_sil=8000:sp=occurrence:random_seed=768423488:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 16.16/3.62 % (440851)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2788251335:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 16.16/3.62 % (440849)Instruction limit reached!
% 16.16/3.62 % (440849)------------------------------
% 16.16/3.62 % (440849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440849)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440849)Termination reason: Instruction limit
% 16.16/3.62 % (440849)Termination phase: Saturation
% 16.16/3.62 % (440849)Time elapsed: 0.071 s
% 16.16/3.62 % (440849)Peak memory usage: 89 MB
% 16.16/3.62 % (440849)Instructions burned: 115 (million)
% 16.16/3.62 % (440855)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2570928669:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 16.16/3.62 % (440851)Instruction limit reached!
% 16.16/3.62 % (440851)------------------------------
% 16.16/3.62 % (440851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440851)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440851)Termination reason: Instruction limit
% 16.16/3.62 % (440851)Termination phase: Saturation
% 16.16/3.62 % (440851)Time elapsed: 0.264 s
% 16.16/3.62 % (440851)Peak memory usage: 95 MB
% 16.16/3.62 % (440851)Instructions burned: 438 (million)
% 16.16/3.62 % (440857)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3149645838:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 16.16/3.62 % (440857)Instruction limit reached!
% 16.16/3.62 % (440857)------------------------------
% 16.16/3.62 % (440857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440857)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440857)Termination reason: Instruction limit
% 16.16/3.62 % (440857)Termination phase: Saturation
% 16.16/3.62 % (440857)Time elapsed: 0.069 s
% 16.16/3.62 % (440857)Peak memory usage: 92 MB
% 16.16/3.62 % (440857)Instructions burned: 135 (million)
% 16.16/3.62 % (440850)Instruction limit reached!
% 16.16/3.62 % (440850)------------------------------
% 16.16/3.62 % (440850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440850)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440850)Termination reason: Instruction limit
% 16.16/3.62 % (440850)Termination phase: Saturation
% 16.16/3.62 % (440850)Time elapsed: 0.568 s
% 16.16/3.62 % (440850)Peak memory usage: 104 MB
% 16.16/3.62 % (440850)Instructions burned: 908 (million)
% 16.16/3.62 % (440859)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1436317873:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 16.16/3.62 % (440860)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=733633946:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 16.16/3.62 % (440859)Instruction limit reached!
% 16.16/3.62 % (440859)------------------------------
% 16.16/3.62 % (440859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440859)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440859)Termination reason: Instruction limit
% 16.16/3.62 % (440859)Termination phase: Saturation
% 16.16/3.62 % (440859)Time elapsed: 0.370 s
% 16.16/3.62 % (440859)Peak memory usage: 101 MB
% 16.16/3.62 % (440859)Instructions burned: 592 (million)
% 16.16/3.62 % (440863)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=1301660857:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 16.16/3.62 % (440863)Instruction limit reached!
% 16.16/3.62 % (440863)------------------------------
% 16.16/3.62 % (440863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440863)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440863)Termination reason: Instruction limit
% 16.16/3.62 % (440863)Termination phase: Saturation
% 16.16/3.62 % (440863)Time elapsed: 0.071 s
% 16.16/3.62 % (440863)Peak memory usage: 92 MB
% 16.16/3.62 % (440863)Instructions burned: 126 (million)
% 16.16/3.62 % (440842)Instruction limit reached!
% 16.16/3.62 % (440842)------------------------------
% 16.16/3.62 % (440842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440842)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440842)Termination reason: Instruction limit
% 16.16/3.62 % (440842)Termination phase: Saturation
% 16.16/3.62 % (440842)Time elapsed: 1.481 s
% 16.16/3.62 % (440842)Peak memory usage: 146 MB
% 16.16/3.62 % (440842)Instructions burned: 2351 (million)
% 16.16/3.62 % (440865)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=699920451:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 16.16/3.62 % (440866)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1447245674:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 16.16/3.62 % (440865)Instruction limit reached!
% 16.16/3.62 % (440865)------------------------------
% 16.16/3.62 % (440865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440865)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440865)Termination reason: Instruction limit
% 16.16/3.62 % (440865)Termination phase: Saturation
% 16.16/3.62 % (440865)Time elapsed: 0.073 s
% 16.16/3.62 % (440865)Peak memory usage: 92 MB
% 16.16/3.62 % (440865)Instructions burned: 135 (million)
% 16.16/3.62 % (440866)Instruction limit reached!
% 16.16/3.62 % (440866)------------------------------
% 16.16/3.62 % (440866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.16/3.62 % (440866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.16/3.62 % (440866)CaDiCaL version: 2.1.3
% 16.16/3.62 % (440866)Termination reason: Instruction limit
% 16.16/3.62 % (440866)Termination phase: Saturation
% 16.16/3.62 % (440866)Time elapsed: 0.074 s
% 16.16/3.62 % (440866)Peak memory usage: 92 MB
% 16.16/3.62 % (440866)Instructions burned: 142 (million)
% 16.16/3.62 % (440819)First to succeed.
% 16.16/3.62 % (440819)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-440814"
% 16.16/3.62 % (440869)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=336024560:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 16.16/3.62 % (440870)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=3076041728:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 16.16/3.62 % (440819)Refutation found. Thanks to Tanya!
% 16.16/3.62 % SZS status Theorem for theBenchmark
% 16.16/3.62 % SZS output start Proof for theBenchmark
% See solution above
% 19.80/3.88 % (440819)------------------------------
% 19.80/3.88 % (440819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.80/3.88 % (440819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.88 % (440819)CaDiCaL version: 2.1.3
% 19.80/3.88 % (440819)Termination reason: Refutation
% 19.80/3.88 % (440819)Time elapsed: 2.297 s
% 19.80/3.88 % (440819)Peak memory usage: 158 MB
% 19.80/3.88 % (440819)Instructions burned: 3603 (million)
% 19.80/3.88 % (440819)------------------------------
% 19.80/3.88 % (440819)------------------------------
% 19.80/3.88 % (440814)Success in time 2.804 s
% 19.80/3.88 % Vampire exiting
%------------------------------------------------------------------------------