%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU358+1 : 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 : n016.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:31 PM UTC 2026
% Result : Theorem 17.73s 3.59s
% Output : Refutation 18.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 65
% Syntax : Number of formulae : 748 ( 61 unt; 42 def)
% Number of atoms : 3794 ( 220 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 5395 (2349 ~;2677 |; 239 &)
% ( 73 <=>; 57 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 65 ( 63 usr; 38 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-3 aty)
% Number of variables : 651 ( 0 sgn 621 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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(f7,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( ex_inf_of_relstr_set(X0,X1)
=> ( X2 = meet_on_relstr(X0,X1)
<=> ( relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_element_smaller(X0,X1,X3)
=> related(X0,X3,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_yellow_0) ).
fof(f8,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(f11,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> cast_to_el_of_LattPOSet(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f12,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(poset_of_lattice(X0)))
=> cast_to_el_of_lattice(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f13,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( ex_sup_of_relstr_set(X0,X1)
=> ( X2 = join_on_relstr(X0,X1)
<=> ( relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X1,X3)
=> related(X0,X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_yellow_0) ).
fof(f15,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(f16,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(f18,axiom,
! [X0,X1] :
( rel_str(X0)
=> element(join_on_relstr(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f23,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ( strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0))
& rel_str(poset_of_lattice(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_lattice3) ).
fof(f24,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0)
& element(X1,the_carrier(X0)) )
=> element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_lattice3) ).
fof(f25,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0)
& element(X1,the_carrier(poset_of_lattice(X0))) )
=> element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f51,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ( ~ empty_carrier(poset_of_lattice(X0))
& strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_lattice3) ).
fof(f65,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(f66,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& reflexive_relstr(X0)
& rel_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f70,axiom,
! [X0] :
( ( antisymmetric_relstr(X0)
& rel_str(X0) )
=> ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_set_smaller(X0,X1,X3)
=> related(X0,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow_0) ).
fof(f71,axiom,
! [X0] :
( ( antisymmetric_relstr(X0)
& rel_str(X0) )
=> ! [X1] :
( ex_inf_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( element(X3,the_carrier(X0))
=> ( relstr_element_smaller(X0,X1,X3)
=> related(X0,X3,X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_yellow_0) ).
fof(f74,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_lattice3) ).
fof(f75,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ! [X1] :
( join_of_latt_set(X0,X1) = join_on_relstr(poset_of_lattice(X0),X1)
& meet_of_latt_set(X0,X1) = meet_on_relstr(poset_of_lattice(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_yellow_0) ).
fof(f76,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) )
=> ! [X1] :
( join_of_latt_set(X0,X1) = join_on_relstr(poset_of_lattice(X0),X1)
& meet_of_latt_set(X0,X1) = meet_on_relstr(poset_of_lattice(X0),X1) ) ),
inference(negated_conjecture,[status(cth)],[f75]) ).
fof(f79,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_lattice3) ).
fof(f80,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_lattice3) ).
fof(f81,axiom,
! [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(f87,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_lattice3) ).
fof(f94,plain,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
inference(pure_predicate_removal,[],[f1]) ).
fof(f95,plain,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& join_commutative(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
inference(pure_predicate_removal,[],[f94]) ).
fof(f96,plain,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
inference(pure_predicate_removal,[],[f95]) ).
fof(f97,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f97]) ).
fof(f104,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = meet_on_relstr(X0,X1)
<=> ( relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f105,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = meet_on_relstr(X0,X1)
<=> ( relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f104]) ).
fof(f106,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,[],[f8]) ).
fof(f107,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,[],[f106]) ).
fof(f112,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f115,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = join_on_relstr(X0,X1)
<=> ( relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f117,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = join_on_relstr(X0,X1)
<=> ( relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f116]) ).
fof(f119,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f120,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f119]) ).
fof(f121,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f122,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f127,plain,
! [X0] :
( ( strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0))
& rel_str(poset_of_lattice(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f128,plain,
! [X0] :
( ( strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0))
& rel_str(poset_of_lattice(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0)) ),
inference(ennf_transformation,[],[f24]) ).
fof(f130,plain,
! [X0,X1] :
( element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0)) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(ennf_transformation,[],[f25]) ).
fof(f132,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(flattening,[],[f131]) ).
fof(f149,plain,
! [X0] :
( ( ~ empty_carrier(poset_of_lattice(X0))
& strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f150,plain,
! [X0] :
( ( ~ empty_carrier(poset_of_lattice(X0))
& strict_rel_str(poset_of_lattice(X0))
& reflexive_relstr(poset_of_lattice(X0))
& transitive_relstr(poset_of_lattice(X0))
& antisymmetric_relstr(poset_of_lattice(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f149]) ).
fof(f160,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,[],[f65]) ).
fof(f161,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,[],[f160]) ).
fof(f162,plain,
! [X0,X1,X2] :
( ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f66]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ( related_reflexive(X0,X1,X2)
<=> related(X0,X1,X2) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f162]) ).
fof(f168,plain,
! [X0] :
( ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f70]) ).
fof(f169,plain,
! [X0] :
( ! [X1] :
( ex_sup_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f168]) ).
fof(f170,plain,
! [X0] :
( ! [X1] :
( ex_inf_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f171,plain,
! [X0] :
( ! [X1] :
( ex_inf_of_relstr_set(X0,X1)
<=> ? [X2] :
( element(X2,the_carrier(X0))
& relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f170]) ).
fof(f175,plain,
! [X0,X1] :
( ! [X2] :
( ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f74]) ).
fof(f176,plain,
! [X0,X1] :
( ! [X2] :
( ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f175]) ).
fof(f177,plain,
? [X0] :
( ? [X1] :
( join_of_latt_set(X0,X1) != join_on_relstr(poset_of_lattice(X0),X1)
| meet_of_latt_set(X0,X1) != meet_on_relstr(poset_of_lattice(X0),X1) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(ennf_transformation,[],[f76]) ).
fof(f178,plain,
? [X0] :
( ? [X1] :
( join_of_latt_set(X0,X1) != join_on_relstr(poset_of_lattice(X0),X1)
| meet_of_latt_set(X0,X1) != meet_on_relstr(poset_of_lattice(X0),X1) )
& ~ empty_carrier(X0)
& lattice(X0)
& complete_latt_str(X0)
& latt_str(X0) ),
inference(flattening,[],[f177]) ).
fof(f182,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f79]) ).
fof(f183,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f182]) ).
fof(f184,plain,
! [X0,X1] :
( ! [X2] :
( ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f80]) ).
fof(f185,plain,
! [X0,X1] :
( ! [X2] :
( ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f184]) ).
fof(f186,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,[],[f81]) ).
fof(f187,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,[],[f186]) ).
fof(f194,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f87]) ).
fof(f195,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f194]) ).
fof(f197,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = meet_on_relstr(X0,X1)
| ~ relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& relstr_element_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| meet_on_relstr(X0,X1) != X2 ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f105]) ).
fof(f198,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = meet_on_relstr(X0,X1)
| ~ relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& relstr_element_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| meet_on_relstr(X0,X1) != X2 ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = meet_on_relstr(X0,X1)
| ~ relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& relstr_element_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_element_smaller(X0,X1,X2)
& ! [X4] :
( related(X0,X4,X2)
| ~ relstr_element_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0)) ) )
| meet_on_relstr(X0,X1) != X2 ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(rectify,[],[f198]) ).
fof(f200,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = meet_on_relstr(X0,X1)
| ~ relstr_element_smaller(X0,X1,X2)
| ( ~ related(X0,sK0(X0,X1,X2),X2)
& relstr_element_smaller(X0,X1,sK0(X0,X1,X2))
& element(sK0(X0,X1,X2),the_carrier(X0)) ) )
& ( ( relstr_element_smaller(X0,X1,X2)
& ! [X4] :
( related(X0,X4,X2)
| ~ relstr_element_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0)) ) )
| meet_on_relstr(X0,X1) != X2 ) )
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f199]) ).
fof(f201,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,[],[f107]) ).
fof(f202,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,[],[f201]) ).
fof(f203,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,[],[f202]) ).
fof(f204,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_of_latt_set(X0,X1)
| ~ latt_element_smaller(X0,X2,X1)
| ( ~ below(X0,X2,sK1(X0,X1,X2))
& latt_element_smaller(X0,sK1(X0,X1,X2),X1)
& element(sK1(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,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f203]) ).
fof(f205,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_on_relstr(X0,X1)
| ~ relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& relstr_set_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| join_on_relstr(X0,X1) != X2 ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f117]) ).
fof(f206,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_on_relstr(X0,X1)
| ~ relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& relstr_set_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| join_on_relstr(X0,X1) != X2 ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_on_relstr(X0,X1)
| ~ relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& relstr_set_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) )
& ( ( relstr_set_smaller(X0,X1,X2)
& ! [X4] :
( related(X0,X2,X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0)) ) )
| join_on_relstr(X0,X1) != X2 ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(rectify,[],[f206]) ).
fof(f208,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = join_on_relstr(X0,X1)
| ~ relstr_set_smaller(X0,X1,X2)
| ( ~ related(X0,X2,sK2(X0,X1,X2))
& relstr_set_smaller(X0,X1,sK2(X0,X1,X2))
& element(sK2(X0,X1,X2),the_carrier(X0)) ) )
& ( ( relstr_set_smaller(X0,X1,X2)
& ! [X4] :
( related(X0,X2,X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0)) ) )
| join_on_relstr(X0,X1) != X2 ) )
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f207]) ).
fof(f230,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,[],[f161]) ).
fof(f231,plain,
! [X0,X1,X2] :
( ( ( related_reflexive(X0,X1,X2)
| ~ related(X0,X1,X2) )
& ( related(X0,X1,X2)
| ~ related_reflexive(X0,X1,X2) ) )
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(nnf_transformation,[],[f163]) ).
fof(f232,plain,
! [X0] :
( ! [X1] :
( ( ex_sup_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& relstr_set_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) ) )
& ( ? [X2] :
( element(X2,the_carrier(X0))
& relstr_set_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X2,X3)
| ~ relstr_set_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| ~ ex_sup_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f169]) ).
fof(f233,plain,
! [X0] :
( ! [X1] :
( ( ex_sup_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& relstr_set_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) ) )
& ( ? [X4] :
( element(X4,the_carrier(X0))
& relstr_set_smaller(X0,X1,X4)
& ! [X5] :
( related(X0,X4,X5)
| ~ relstr_set_smaller(X0,X1,X5)
| ~ element(X5,the_carrier(X0)) ) )
| ~ ex_sup_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(rectify,[],[f232]) ).
fof(f234,plain,
! [X0] :
( ! [X1] :
( ( ex_sup_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ( ~ related(X0,X2,sK21(X0,X1,X2))
& relstr_set_smaller(X0,X1,sK21(X0,X1,X2))
& element(sK21(X0,X1,X2),the_carrier(X0)) ) ) )
& ( ( element(sK22(X0,X1),the_carrier(X0))
& relstr_set_smaller(X0,X1,sK22(X0,X1))
& ! [X5] :
( related(X0,sK22(X0,X1),X5)
| ~ relstr_set_smaller(X0,X1,X5)
| ~ element(X5,the_carrier(X0)) ) )
| ~ ex_sup_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22]),skolemize(X3,sK21(X0,X1,X2)),skolemize(X4,sK22(X0,X1))],[f233]) ).
fof(f235,plain,
! [X0] :
( ! [X1] :
( ( ex_inf_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& relstr_element_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) ) )
& ( ? [X2] :
( element(X2,the_carrier(X0))
& relstr_element_smaller(X0,X1,X2)
& ! [X3] :
( related(X0,X3,X2)
| ~ relstr_element_smaller(X0,X1,X3)
| ~ element(X3,the_carrier(X0)) ) )
| ~ ex_inf_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f171]) ).
fof(f236,plain,
! [X0] :
( ! [X1] :
( ( ex_inf_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& relstr_element_smaller(X0,X1,X3)
& element(X3,the_carrier(X0)) ) ) )
& ( ? [X4] :
( element(X4,the_carrier(X0))
& relstr_element_smaller(X0,X1,X4)
& ! [X5] :
( related(X0,X5,X4)
| ~ relstr_element_smaller(X0,X1,X5)
| ~ element(X5,the_carrier(X0)) ) )
| ~ ex_inf_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(rectify,[],[f235]) ).
fof(f237,plain,
! [X0] :
( ! [X1] :
( ( ex_inf_of_relstr_set(X0,X1)
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ( ~ related(X0,sK23(X0,X1,X2),X2)
& relstr_element_smaller(X0,X1,sK23(X0,X1,X2))
& element(sK23(X0,X1,X2),the_carrier(X0)) ) ) )
& ( ( element(sK24(X0,X1),the_carrier(X0))
& relstr_element_smaller(X0,X1,sK24(X0,X1))
& ! [X5] :
( related(X0,X5,sK24(X0,X1))
| ~ relstr_element_smaller(X0,X1,X5)
| ~ element(X5,the_carrier(X0)) ) )
| ~ ex_inf_of_relstr_set(X0,X1) ) )
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24]),skolemize(X3,sK23(X0,X1,X2)),skolemize(X4,sK24(X0,X1))],[f236]) ).
fof(f239,plain,
! [X0,X1] :
( ! [X2] :
( ( ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2) ) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f176]) ).
fof(f240,plain,
( ( join_of_latt_set(sK25,sK26) != join_on_relstr(poset_of_lattice(sK25),sK26)
| meet_of_latt_set(sK25,sK26) != meet_on_relstr(poset_of_lattice(sK25),sK26) )
& ~ empty_carrier(sK25)
& lattice(sK25)
& complete_latt_str(sK25)
& latt_str(sK25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26]),skolemize(X0,sK25),skolemize(X1,sK26)],[f178]) ).
fof(f243,plain,
! [X0,X1] :
( ! [X2] :
( ( ( latt_element_smaller(X1,X2,X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
& ( relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0) ) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f183]) ).
fof(f244,plain,
! [X0,X1] :
( ! [X2] :
( ( ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2) ) )
| ~ element(X2,the_carrier(poset_of_lattice(X1))) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f185]) ).
fof(f245,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)) ) )
& ( ( 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 ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f187]) ).
fof(f246,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)) ) )
& ( ( 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 ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f245]) ).
fof(f247,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)) ) )
& ( ( latt_set_smaller(X0,X1,X2)
& ! [X4] :
( below_refl(X0,X4,X1)
| ~ latt_set_smaller(X0,X4,X2)
| ~ element(X4,the_carrier(X0)) ) )
| meet_of_latt_set(X0,X2) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f246]) ).
fof(f248,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = meet_of_latt_set(X0,X2)
| ~ latt_set_smaller(X0,X1,X2)
| ( ~ below_refl(X0,sK28(X0,X1,X2),X1)
& latt_set_smaller(X0,sK28(X0,X1,X2),X2)
& element(sK28(X0,X1,X2),the_carrier(X0)) ) )
& ( ( latt_set_smaller(X0,X1,X2)
& ! [X4] :
( below_refl(X0,X4,X1)
| ~ latt_set_smaller(X0,X4,X2)
| ~ element(X4,the_carrier(X0)) ) )
| meet_of_latt_set(X0,X2) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X3,sK28(X0,X1,X2))],[f247]) ).
fof(f249,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( below_refl(X0,X1,X2)
| ~ related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
& ( related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| ~ below_refl(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f195]) ).
fof(f250,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| join_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f251,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f252,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_commutative(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f260,plain,
! [X2,X0,X1] :
( element(sK0(X0,X1,X2),the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| meet_on_relstr(X0,X1) = X2
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f261,plain,
! [X2,X0,X1] :
( relstr_element_smaller(X0,X1,sK0(X0,X1,X2))
| ~ relstr_element_smaller(X0,X1,X2)
| meet_on_relstr(X0,X1) = X2
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f262,plain,
! [X2,X0,X1] :
( ~ related(X0,sK0(X0,X1,X2),X2)
| ~ relstr_element_smaller(X0,X1,X2)
| meet_on_relstr(X0,X1) = X2
| ~ ex_inf_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f200]) ).
fof(f263,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,[],[f204]) ).
fof(f264,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,[],[f204]) ).
fof(f265,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| element(sK1(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,[],[f204]) ).
fof(f266,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| latt_element_smaller(X0,sK1(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,[],[f204]) ).
fof(f267,plain,
! [X2,X0,X1] :
( join_of_latt_set(X0,X1) = X2
| ~ latt_element_smaller(X0,X2,X1)
| ~ below(X0,X2,sK1(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,[],[f204]) ).
fof(f270,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| cast_to_el_of_LattPOSet(X0,X1) = X1
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f271,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| cast_to_el_of_lattice(X0,X1) = X1
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f272,plain,
! [X2,X0,X1,X4] :
( related(X0,X2,X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| join_on_relstr(X0,X1) != X2
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f273,plain,
! [X2,X0,X1] :
( relstr_set_smaller(X0,X1,X2)
| join_on_relstr(X0,X1) != X2
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f279,plain,
! [X0,X1] :
( element(join_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f280,plain,
! [X0,X1] :
( element(meet_of_latt_set(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f281,plain,
! [X0,X1] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f288,plain,
! [X0] :
( rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f293,plain,
! [X0,X1] :
( element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f294,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(cnf_transformation,[],[f132]) ).
fof(f323,plain,
! [X0] :
( antisymmetric_relstr(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f150]) ).
fof(f325,plain,
! [X0] :
( reflexive_relstr(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f150]) ).
fof(f327,plain,
! [X0] :
( ~ empty_carrier(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f150]) ).
fof(f359,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,[],[f230]) ).
fof(f360,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,[],[f230]) ).
fof(f361,plain,
! [X2,X0,X1] :
( ~ related_reflexive(X0,X1,X2)
| related(X0,X1,X2)
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f231]) ).
fof(f362,plain,
! [X2,X0,X1] :
( ~ related(X0,X1,X2)
| related_reflexive(X0,X1,X2)
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f231]) ).
fof(f369,plain,
! [X2,X0,X1] :
( element(sK21(X0,X1,X2),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ex_sup_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f370,plain,
! [X2,X0,X1] :
( relstr_set_smaller(X0,X1,sK21(X0,X1,X2))
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ex_sup_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f371,plain,
! [X2,X0,X1] :
( ~ related(X0,X2,sK21(X0,X1,X2))
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ex_sup_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f375,plain,
! [X2,X0,X1] :
( element(sK23(X0,X1,X2),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ex_inf_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f376,plain,
! [X2,X0,X1] :
( relstr_element_smaller(X0,X1,sK23(X0,X1,X2))
| ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ex_inf_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f377,plain,
! [X2,X0,X1] :
( ~ related(X0,sK23(X0,X1,X2),X2)
| ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(X0,X1,X2)
| ex_inf_of_relstr_set(X0,X1)
| ~ antisymmetric_relstr(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f381,plain,
! [X2,X0,X1] :
( latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(poset_of_lattice(X1)))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f382,plain,
! [X2,X0,X1] :
( ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(poset_of_lattice(X1)))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f239]) ).
fof(f383,plain,
latt_str(sK25),
inference(cnf_transformation,[],[f240]) ).
fof(f384,plain,
complete_latt_str(sK25),
inference(cnf_transformation,[],[f240]) ).
fof(f385,plain,
lattice(sK25),
inference(cnf_transformation,[],[f240]) ).
fof(f386,plain,
~ empty_carrier(sK25),
inference(cnf_transformation,[],[f240]) ).
fof(f387,plain,
( join_of_latt_set(sK25,sK26) != join_on_relstr(poset_of_lattice(sK25),sK26)
| meet_of_latt_set(sK25,sK26) != meet_on_relstr(poset_of_lattice(sK25),sK26) ),
inference(cnf_transformation,[],[f240]) ).
fof(f391,plain,
! [X2,X0,X1] :
( relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f243]) ).
fof(f393,plain,
! [X2,X0,X1] :
( latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(poset_of_lattice(X1)))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f244]) ).
fof(f394,plain,
! [X2,X0,X1] :
( ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(poset_of_lattice(X1)))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f244]) ).
fof(f395,plain,
! [X2,X0,X1,X4] :
( below_refl(X0,X4,X1)
| ~ latt_set_smaller(X0,X4,X2)
| ~ element(X4,the_carrier(X0))
| meet_of_latt_set(X0,X2) != X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f396,plain,
! [X2,X0,X1] :
( latt_set_smaller(X0,X1,X2)
| meet_of_latt_set(X0,X2) != X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f405,plain,
! [X2,X0,X1] :
( related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| ~ below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ~ related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f249]) ).
fof(f410,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,[],[f264]) ).
fof(f411,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,[],[f263]) ).
fof(f412,plain,
! [X0,X1] :
( relstr_set_smaller(X0,X1,join_on_relstr(X0,X1))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(equality_resolution,[],[f273]) ).
fof(f413,plain,
! [X0,X1,X4] :
( related(X0,join_on_relstr(X0,X1),X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(equality_resolution,[],[f272]) ).
fof(f415,plain,
! [X2,X0] :
( ~ element(meet_of_latt_set(X0,X2),the_carrier(X0))
| latt_set_smaller(X0,meet_of_latt_set(X0,X2),X2)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(equality_resolution,[],[f396]) ).
fof(f416,plain,
! [X2,X0,X4] :
( ~ element(meet_of_latt_set(X0,X2),the_carrier(X0))
| ~ latt_set_smaller(X0,X4,X2)
| ~ element(X4,the_carrier(X0))
| below_refl(X0,X4,meet_of_latt_set(X0,X2))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(equality_resolution,[],[f395]) ).
fof(f417,definition,
sF29 = join_of_latt_set(sK25,sK26),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f418,plain,
join_of_latt_set(sK25,sK26) = sF29,
inference(reorient_equations,[],[f417]) ).
fof(f419,definition,
sF30 = poset_of_lattice(sK25),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f420,plain,
poset_of_lattice(sK25) = sF30,
inference(reorient_equations,[],[f419]) ).
fof(f421,definition,
sF31 = join_on_relstr(sF30,sK26),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f422,plain,
join_on_relstr(sF30,sK26) = sF31,
inference(reorient_equations,[],[f421]) ).
fof(f423,definition,
sF32 = meet_of_latt_set(sK25,sK26),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f424,plain,
meet_of_latt_set(sK25,sK26) = sF32,
inference(reorient_equations,[],[f423]) ).
fof(f425,definition,
sF33 = meet_on_relstr(sF30,sK26),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f426,plain,
meet_on_relstr(sF30,sK26) = sF33,
inference(reorient_equations,[],[f425]) ).
fof(f427,plain,
( sF29 != sF31
| sF32 != sF33 ),
inference(definition_folding,[],[f387,f426,f420,f424,f422,f420,f418]) ).
fof(f428,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,[],[f411]) ).
fof(f429,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,[],[f410]) ).
fof(f430,plain,
! [X2,X0,X1] :
( element(sK1(X0,X1,X2),the_carrier(X0))
| ~ 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) ),
inference(duplicate_literal_removal,[],[f265]) ).
fof(f431,plain,
! [X2,X0,X1] :
( latt_element_smaller(X0,sK1(X0,X1,X2),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) ),
inference(duplicate_literal_removal,[],[f266]) ).
fof(f432,plain,
! [X2,X0,X1] :
( ~ below(X0,X2,sK1(X0,X1,X2))
| ~ 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) ),
inference(duplicate_literal_removal,[],[f267]) ).
fof(f434,definition,
( spl34_1
<=> sF32 = sF33 ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f436,plain,
( sF32 != sF33
| spl34_1 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl34_2
<=> sF29 = sF31 ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f440,plain,
( sF29 != sF31
| spl34_2 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl34_1
| ~ spl34_2 ),
inference(avatar_split_clause,[],[f427,f438,f434]) ).
fof(f442,plain,
! [X0,X1,X4] :
( related(X0,join_on_relstr(X0,X1),X4)
| ~ relstr_set_smaller(X0,X1,X4)
| ~ element(X4,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[],[f413,f281]) ).
fof(f443,plain,
! [X0,X1] :
( relstr_set_smaller(X0,X1,join_on_relstr(X0,X1))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[],[f412,f281]) ).
fof(f444,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,[],[f428,f279]) ).
fof(f445,plain,
! [X0,X1] :
( latt_element_smaller(X0,join_of_latt_set(X0,X1),X1)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f429,f279]) ).
fof(f448,plain,
( ~ element(sF32,the_carrier(sK25))
| latt_set_smaller(sK25,sF32,sK26)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f415,f424]) ).
fof(f449,plain,
( ~ element(sF32,the_carrier(sK25))
| latt_set_smaller(sK25,sF32,sK26)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f448,f386]) ).
fof(f450,plain,
( ~ element(sF32,the_carrier(sK25))
| latt_set_smaller(sK25,sF32,sK26)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f449,f385]) ).
fof(f451,plain,
( ~ element(sF32,the_carrier(sK25))
| latt_set_smaller(sK25,sF32,sK26)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f450,f384]) ).
fof(f452,plain,
( ~ element(sF32,the_carrier(sK25))
| latt_set_smaller(sK25,sF32,sK26) ),
inference(forward_subsumption_resolution,[],[f451,f383]) ).
fof(f454,definition,
( spl34_3
<=> latt_set_smaller(sK25,sF32,sK26) ),
introduced(definition,[new_symbols(definition,[spl34_3])],[avatar_definition]) ).
fof(f456,plain,
( latt_set_smaller(sK25,sF32,sK26)
| ~ spl34_3 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f458,definition,
( spl34_4
<=> element(sF32,the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_4])],[avatar_definition]) ).
fof(f459,plain,
( element(sF32,the_carrier(sK25))
| ~ spl34_4 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f460,plain,
( ~ element(sF32,the_carrier(sK25))
| spl34_4 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f461,plain,
( spl34_3
| ~ spl34_4 ),
inference(avatar_split_clause,[],[f452,f458,f454]) ).
fof(f462,plain,
( element(sF29,the_carrier(sK25))
| empty_carrier(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f279,f418]) ).
fof(f463,plain,
( element(sF29,the_carrier(sK25))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f462,f386]) ).
fof(f464,plain,
element(sF29,the_carrier(sK25)),
inference(forward_subsumption_resolution,[],[f463,f383]) ).
fof(f466,plain,
( element(sF32,the_carrier(sK25))
| empty_carrier(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f280,f424]) ).
fof(f468,plain,
( empty_carrier(sK25)
| ~ latt_str(sK25)
| spl34_4 ),
inference(forward_subsumption_resolution,[],[f466,f460]) ).
fof(f469,plain,
( ~ latt_str(sK25)
| spl34_4 ),
inference(forward_subsumption_resolution,[],[f468,f386]) ).
fof(f470,plain,
( $false
| spl34_4 ),
inference(forward_subsumption_resolution,[],[f469,f383]) ).
fof(f471,plain,
spl34_4,
inference(avatar_contradiction_clause,[],[f470]) ).
fof(f478,definition,
( spl34_5
<=> rel_str(sF30) ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f479,plain,
( rel_str(sF30)
| ~ spl34_5 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( ~ rel_str(sF30)
| spl34_5 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f482,definition,
( spl34_6
<=> ex_inf_of_relstr_set(sF30,sK26) ),
introduced(definition,[new_symbols(definition,[spl34_6])],[avatar_definition]) ).
fof(f483,plain,
( ex_inf_of_relstr_set(sF30,sK26)
| ~ spl34_6 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f484,plain,
( ~ ex_inf_of_relstr_set(sF30,sK26)
| spl34_6 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f491,plain,
! [X0] :
( ~ element(sF32,the_carrier(sK25))
| ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f416,f424]) ).
fof(f493,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f491,f459]) ).
fof(f494,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f493,f386]) ).
fof(f495,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f494,f385]) ).
fof(f496,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f495,f384]) ).
fof(f497,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f496,f383]) ).
fof(f498,plain,
( element(sF31,the_carrier(sF30))
| ~ rel_str(sF30) ),
inference(superposition,[],[f281,f422]) ).
fof(f500,plain,
( latt_element_smaller(sK25,sF29,sK26)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f445,f418]) ).
fof(f501,plain,
( latt_element_smaller(sK25,sF29,sK26)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f500,f386]) ).
fof(f502,plain,
( latt_element_smaller(sK25,sF29,sK26)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f501,f385]) ).
fof(f503,plain,
( latt_element_smaller(sK25,sF29,sK26)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f502,f384]) ).
fof(f504,plain,
latt_element_smaller(sK25,sF29,sK26),
inference(forward_subsumption_resolution,[],[f503,f383]) ).
fof(f524,plain,
( sF32 = cast_to_el_of_LattPOSet(sK25,sF32)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_4 ),
inference(resolution,[],[f270,f459]) ).
fof(f525,plain,
( sF29 = cast_to_el_of_LattPOSet(sK25,sF29)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(resolution,[],[f270,f464]) ).
fof(f528,plain,
( sF29 = cast_to_el_of_LattPOSet(sK25,sF29)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f525,f386]) ).
fof(f529,plain,
( sF32 = cast_to_el_of_LattPOSet(sK25,sF32)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f524,f386]) ).
fof(f530,plain,
( sF29 = cast_to_el_of_LattPOSet(sK25,sF29)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f528,f385]) ).
fof(f531,plain,
( sF32 = cast_to_el_of_LattPOSet(sK25,sF32)
| ~ latt_str(sK25)
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f529,f385]) ).
fof(f532,plain,
sF29 = cast_to_el_of_LattPOSet(sK25,sF29),
inference(forward_subsumption_resolution,[],[f530,f383]) ).
fof(f533,plain,
( sF32 = cast_to_el_of_LattPOSet(sK25,sF32)
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f531,f383]) ).
fof(f555,plain,
! [X0,X1] :
( join_on_relstr(poset_of_lattice(X0),X1) = cast_to_el_of_lattice(X0,join_on_relstr(poset_of_lattice(X0),X1))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ rel_str(poset_of_lattice(X0)) ),
inference(resolution,[],[f271,f281]) ).
fof(f556,plain,
! [X0] :
( ~ element(X0,the_carrier(sF30))
| cast_to_el_of_lattice(sK25,X0) = X0
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f271,f420]) ).
fof(f557,plain,
! [X0] :
( ~ element(X0,the_carrier(sF30))
| cast_to_el_of_lattice(sK25,X0) = X0
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f556,f386]) ).
fof(f558,plain,
! [X0,X1] :
( ~ lattice(X0)
| empty_carrier(X0)
| join_on_relstr(poset_of_lattice(X0),X1) = cast_to_el_of_lattice(X0,join_on_relstr(poset_of_lattice(X0),X1))
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f555,f288]) ).
fof(f562,plain,
! [X0] :
( ~ element(X0,the_carrier(sF30))
| cast_to_el_of_lattice(sK25,X0) = X0
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f557,f385]) ).
fof(f563,plain,
! [X0] :
( ~ element(X0,the_carrier(sF30))
| cast_to_el_of_lattice(sK25,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f562,f383]) ).
fof(f573,definition,
( spl34_9
<=> empty_carrier(sF30) ),
introduced(definition,[new_symbols(definition,[spl34_9])],[avatar_definition]) ).
fof(f574,plain,
( ~ empty_carrier(sF30)
| spl34_9 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f602,plain,
( ~ empty_carrier(sF30)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f327,f420]) ).
fof(f603,plain,
( ~ empty_carrier(sF30)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f602,f386]) ).
fof(f604,plain,
( ~ empty_carrier(sF30)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f603,f385]) ).
fof(f605,plain,
~ empty_carrier(sF30),
inference(forward_subsumption_resolution,[],[f604,f383]) ).
fof(f606,plain,
~ spl34_9,
inference(avatar_split_clause,[],[f605,f573]) ).
fof(f607,plain,
( ! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(cast_to_el_of_lattice(sK25,X0),the_carrier(sK25))
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(resolution,[],[f381,f497]) ).
fof(f608,plain,
( ! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f607,f294]) ).
fof(f609,plain,
( ! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f608,f386]) ).
fof(f610,plain,
( ! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25)
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f609,f385]) ).
fof(f611,plain,
( ! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f610,f383]) ).
fof(f612,plain,
( ! [X0] :
( ~ relstr_element_smaller(sF30,sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32) )
| ~ spl34_4 ),
inference(forward_demodulation,[],[f611,f420]) ).
fof(f613,plain,
( ! [X0] :
( below_refl(sK25,cast_to_el_of_lattice(sK25,X0),sF32)
| ~ relstr_element_smaller(sF30,sK26,X0)
| ~ element(X0,the_carrier(sF30)) )
| ~ spl34_4 ),
inference(forward_demodulation,[],[f612,f420]) ).
fof(f625,plain,
( element(sF32,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF32,the_carrier(sK25))
| ~ spl34_4 ),
inference(superposition,[],[f293,f533]) ).
fof(f626,plain,
( element(sF29,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF29,the_carrier(sK25)) ),
inference(superposition,[],[f293,f532]) ).
fof(f627,plain,
! [X0] :
( element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(X0,the_carrier(sK25)) ),
inference(superposition,[],[f293,f420]) ).
fof(f629,plain,
! [X0] :
( element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(X0,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f627,f386]) ).
fof(f630,plain,
( element(sF29,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF29,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f626,f386]) ).
fof(f631,plain,
( element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF32,the_carrier(sK25))
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f625,f386]) ).
fof(f633,plain,
! [X0] :
( element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| ~ latt_str(sK25)
| ~ element(X0,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f629,f385]) ).
fof(f634,plain,
( element(sF29,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25)
| ~ element(sF29,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f630,f385]) ).
fof(f635,plain,
( element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25)
| ~ element(sF32,the_carrier(sK25))
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f631,f385]) ).
fof(f636,plain,
! [X0] :
( element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| ~ element(X0,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f633,f383]) ).
fof(f637,plain,
( element(sF29,the_carrier(poset_of_lattice(sK25)))
| ~ element(sF29,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f634,f383]) ).
fof(f638,plain,
( element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ element(sF32,the_carrier(sK25))
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f635,f383]) ).
fof(f639,plain,
element(sF29,the_carrier(poset_of_lattice(sK25))),
inference(forward_subsumption_resolution,[],[f637,f464]) ).
fof(f640,plain,
( element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f638,f459]) ).
fof(f641,plain,
element(sF29,the_carrier(sF30)),
inference(forward_demodulation,[],[f639,f420]) ).
fof(f642,plain,
( element(sF32,the_carrier(sF30))
| ~ spl34_4 ),
inference(forward_demodulation,[],[f640,f420]) ).
fof(f643,plain,
( sF32 = cast_to_el_of_lattice(sK25,sF32)
| ~ spl34_4 ),
inference(resolution,[],[f642,f563]) ).
fof(f646,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,sF32,X0)
| relstr_element_smaller(poset_of_lattice(sK25),X0,sF32)
| ~ element(sF32,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(superposition,[],[f382,f643]) ).
fof(f649,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,sF32,X0)
| relstr_element_smaller(poset_of_lattice(sK25),X0,sF32)
| ~ element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f646,f386]) ).
fof(f651,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,sF32,X0)
| relstr_element_smaller(poset_of_lattice(sK25),X0,sF32)
| ~ element(sF32,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f649,f385]) ).
fof(f653,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,sF32,X0)
| relstr_element_smaller(poset_of_lattice(sK25),X0,sF32)
| ~ element(sF32,the_carrier(poset_of_lattice(sK25))) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f651,f383]) ).
fof(f655,plain,
( ! [X0] :
( relstr_element_smaller(sF30,X0,sF32)
| ~ latt_set_smaller(sK25,sF32,X0)
| ~ element(sF32,the_carrier(poset_of_lattice(sK25))) )
| ~ spl34_4 ),
inference(forward_demodulation,[],[f653,f420]) ).
fof(f656,plain,
( ! [X0] :
( ~ element(sF32,the_carrier(sF30))
| relstr_element_smaller(sF30,X0,sF32)
| ~ latt_set_smaller(sK25,sF32,X0) )
| ~ spl34_4 ),
inference(forward_demodulation,[],[f655,f420]) ).
fof(f657,plain,
( ! [X0] :
( ~ latt_set_smaller(sK25,sF32,X0)
| relstr_element_smaller(sF30,X0,sF32) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f656,f642]) ).
fof(f658,plain,
sF29 = cast_to_el_of_lattice(sK25,sF29),
inference(resolution,[],[f641,f563]) ).
fof(f750,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0) ),
inference(resolution,[],[f360,f444]) ).
fof(f754,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ complete_latt_str(X0) ),
inference(duplicate_literal_removal,[],[f750]) ).
fof(f757,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ complete_latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f754,f252]) ).
fof(f760,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ complete_latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f757,f251]) ).
fof(f763,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ latt_str(X0)
| ~ element(join_of_latt_set(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ complete_latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f760,f250]) ).
fof(f765,definition,
( spl34_16
<=> join_absorbing(sK25) ),
introduced(definition,[new_symbols(definition,[spl34_16])],[avatar_definition]) ).
fof(f766,plain,
( join_absorbing(sK25)
| ~ spl34_16 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f767,plain,
( ~ join_absorbing(sK25)
| spl34_16 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f769,definition,
( spl34_17
<=> meet_absorbing(sK25) ),
introduced(definition,[new_symbols(definition,[spl34_17])],[avatar_definition]) ).
fof(f770,plain,
( meet_absorbing(sK25)
| ~ spl34_17 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f773,definition,
( spl34_18
<=> meet_commutative(sK25) ),
introduced(definition,[new_symbols(definition,[spl34_18])],[avatar_definition]) ).
fof(f774,plain,
( meet_commutative(sK25)
| ~ spl34_18 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f785,plain,
! [X2,X0,X1] :
( below_refl(X0,join_of_latt_set(X0,X1),X2)
| empty_carrier(X0)
| ~ latt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ complete_latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f763,f279]) ).
fof(f786,plain,
! [X0] :
( below_refl(sK25,sF29,X0)
| empty_carrier(sK25)
| ~ latt_str(sK25)
| ~ element(X0,the_carrier(sK25))
| ~ latt_element_smaller(sK25,X0,sK26)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25) ),
inference(superposition,[],[f785,f418]) ).
fof(f787,plain,
! [X0] :
( below_refl(sK25,sF29,X0)
| ~ latt_str(sK25)
| ~ element(X0,the_carrier(sK25))
| ~ latt_element_smaller(sK25,X0,sK26)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f786,f386]) ).
fof(f788,plain,
! [X0] :
( below_refl(sK25,sF29,X0)
| ~ element(X0,the_carrier(sK25))
| ~ latt_element_smaller(sK25,X0,sK26)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f787,f383]) ).
fof(f789,plain,
! [X0] :
( below_refl(sK25,sF29,X0)
| ~ element(X0,the_carrier(sK25))
| ~ latt_element_smaller(sK25,X0,sK26)
| ~ complete_latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f788,f385]) ).
fof(f790,plain,
! [X0] :
( ~ latt_element_smaller(sK25,X0,sK26)
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,sF29,X0) ),
inference(forward_subsumption_resolution,[],[f789,f384]) ).
fof(f793,plain,
! [X0] :
( ~ element(cast_to_el_of_lattice(sK25,X0),the_carrier(sK25))
| below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(resolution,[],[f790,f393]) ).
fof(f794,plain,
! [X0] :
( below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f793,f294]) ).
fof(f797,plain,
! [X0] :
( below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f794,f386]) ).
fof(f800,plain,
! [X0] :
( below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f797,f385]) ).
fof(f802,plain,
! [X0] :
( below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(poset_of_lattice(sK25),sK26,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f800,f383]) ).
fof(f804,plain,
! [X0] :
( ~ relstr_set_smaller(sF30,sK26,X0)
| below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ element(X0,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_demodulation,[],[f802,f420]) ).
fof(f806,plain,
! [X0] :
( below_refl(sK25,sF29,cast_to_el_of_lattice(sK25,X0))
| ~ relstr_set_smaller(sF30,sK26,X0)
| ~ element(X0,the_carrier(sF30)) ),
inference(forward_demodulation,[],[f804,f420]) ).
fof(f885,plain,
! [X2,X0,X1] :
( related_reflexive(X0,join_on_relstr(X0,X1),X2)
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ ex_sup_of_relstr_set(X0,X1)
| ~ rel_str(X0) ),
inference(resolution,[],[f362,f442]) ).
fof(f886,plain,
! [X2,X0,X1] :
( related_reflexive(X0,join_on_relstr(X0,X1),X2)
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ ex_sup_of_relstr_set(X0,X1) ),
inference(duplicate_literal_removal,[],[f885]) ).
fof(f888,plain,
! [X2,X0,X1] :
( related_reflexive(X0,join_on_relstr(X0,X1),X2)
| empty_carrier(X0)
| ~ reflexive_relstr(X0)
| ~ rel_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(X0,X1,X2)
| ~ ex_sup_of_relstr_set(X0,X1) ),
inference(forward_subsumption_resolution,[],[f886,f281]) ).
fof(f894,plain,
! [X0] :
( related_reflexive(sF30,sF31,X0)
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(X0,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,X0)
| ~ ex_sup_of_relstr_set(sF30,sK26) ),
inference(superposition,[],[f888,f422]) ).
fof(f942,plain,
! [X0] :
( ~ latt_element_smaller(sK25,sF29,X0)
| relstr_set_smaller(poset_of_lattice(sK25),X0,sF29)
| ~ element(sF29,the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f394,f658]) ).
fof(f944,plain,
! [X0] :
( ~ latt_element_smaller(sK25,sF29,X0)
| relstr_set_smaller(poset_of_lattice(sK25),X0,sF29)
| ~ element(sF29,the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f942,f386]) ).
fof(f946,plain,
! [X0] :
( ~ latt_element_smaller(sK25,sF29,X0)
| relstr_set_smaller(poset_of_lattice(sK25),X0,sF29)
| ~ element(sF29,the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f944,f385]) ).
fof(f948,plain,
! [X0] :
( ~ latt_element_smaller(sK25,sF29,X0)
| relstr_set_smaller(poset_of_lattice(sK25),X0,sF29)
| ~ element(sF29,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f946,f383]) ).
fof(f950,plain,
! [X0] :
( relstr_set_smaller(sF30,X0,sF29)
| ~ latt_element_smaller(sK25,sF29,X0)
| ~ element(sF29,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_demodulation,[],[f948,f420]) ).
fof(f952,plain,
! [X0] :
( ~ element(sF29,the_carrier(sF30))
| relstr_set_smaller(sF30,X0,sF29)
| ~ latt_element_smaller(sK25,sF29,X0) ),
inference(forward_demodulation,[],[f950,f420]) ).
fof(f954,plain,
! [X0] :
( ~ latt_element_smaller(sK25,sF29,X0)
| relstr_set_smaller(sF30,X0,sF29) ),
inference(forward_subsumption_resolution,[],[f952,f641]) ).
fof(f987,plain,
( empty_carrier(sK25)
| meet_commutative(sK25)
| ~ latt_str(sK25) ),
inference(resolution,[],[f252,f385]) ).
fof(f988,plain,
( meet_commutative(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f987,f386]) ).
fof(f989,plain,
meet_commutative(sK25),
inference(forward_subsumption_resolution,[],[f988,f383]) ).
fof(f990,plain,
spl34_18,
inference(avatar_split_clause,[],[f989,f773]) ).
fof(f998,plain,
( empty_carrier(sK25)
| meet_absorbing(sK25)
| ~ latt_str(sK25) ),
inference(resolution,[],[f251,f385]) ).
fof(f999,plain,
( meet_absorbing(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f998,f386]) ).
fof(f1000,plain,
meet_absorbing(sK25),
inference(forward_subsumption_resolution,[],[f999,f383]) ).
fof(f1001,plain,
spl34_17,
inference(avatar_split_clause,[],[f1000,f769]) ).
fof(f1037,plain,
( antisymmetric_relstr(sF30)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f323,f420]) ).
fof(f1038,plain,
( antisymmetric_relstr(sF30)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1037,f386]) ).
fof(f1039,plain,
( antisymmetric_relstr(sF30)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1038,f385]) ).
fof(f1040,plain,
antisymmetric_relstr(sF30),
inference(forward_subsumption_resolution,[],[f1039,f383]) ).
fof(f1041,plain,
( empty_carrier(sK25)
| join_absorbing(sK25)
| ~ latt_str(sK25) ),
inference(resolution,[],[f250,f385]) ).
fof(f1042,plain,
( join_absorbing(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1041,f386]) ).
fof(f1043,plain,
( ~ latt_str(sK25)
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f1042,f767]) ).
fof(f1044,plain,
( $false
| spl34_16 ),
inference(forward_subsumption_resolution,[],[f1043,f383]) ).
fof(f1045,plain,
spl34_16,
inference(avatar_contradiction_clause,[],[f1044]) ).
fof(f1113,plain,
! [X0] :
( empty_carrier(sK25)
| join_on_relstr(poset_of_lattice(sK25),X0) = cast_to_el_of_lattice(sK25,join_on_relstr(poset_of_lattice(sK25),X0))
| ~ latt_str(sK25) ),
inference(resolution,[],[f558,f385]) ).
fof(f1114,plain,
! [X0] :
( join_on_relstr(poset_of_lattice(sK25),X0) = cast_to_el_of_lattice(sK25,join_on_relstr(poset_of_lattice(sK25),X0))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1113,f386]) ).
fof(f1115,plain,
! [X0] : join_on_relstr(poset_of_lattice(sK25),X0) = cast_to_el_of_lattice(sK25,join_on_relstr(poset_of_lattice(sK25),X0)),
inference(forward_subsumption_resolution,[],[f1114,f383]) ).
fof(f1116,plain,
! [X0] : join_on_relstr(sF30,X0) = cast_to_el_of_lattice(sK25,join_on_relstr(sF30,X0)),
inference(forward_demodulation,[],[f1115,f420]) ).
fof(f1117,plain,
sF31 = cast_to_el_of_lattice(sK25,sF31),
inference(superposition,[],[f1116,f422]) ).
fof(f1121,plain,
! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(superposition,[],[f294,f1116]) ).
fof(f1123,plain,
! [X0,X1] :
( latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1)
| ~ relstr_set_smaller(poset_of_lattice(sK25),X1,join_on_relstr(sF30,X0))
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f393,f1116]) ).
fof(f1128,plain,
! [X0,X1] :
( latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1)
| ~ relstr_set_smaller(poset_of_lattice(sK25),X1,join_on_relstr(sF30,X0))
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1123,f386]) ).
fof(f1130,plain,
! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1121,f386]) ).
fof(f1133,plain,
! [X0,X1] :
( latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1)
| ~ relstr_set_smaller(poset_of_lattice(sK25),X1,join_on_relstr(sF30,X0))
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1128,f385]) ).
fof(f1135,plain,
! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sK25))
| ~ latt_str(sK25)
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1130,f385]) ).
fof(f1138,plain,
! [X0,X1] :
( latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1)
| ~ relstr_set_smaller(poset_of_lattice(sK25),X1,join_on_relstr(sF30,X0))
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1133,f383]) ).
fof(f1140,plain,
! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sK25))
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1135,f383]) ).
fof(f1143,plain,
! [X0,X1] :
( ~ relstr_set_smaller(sF30,X1,join_on_relstr(sF30,X0))
| latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1)
| ~ element(join_on_relstr(sF30,X0),the_carrier(poset_of_lattice(sK25))) ),
inference(forward_demodulation,[],[f1138,f420]) ).
fof(f1145,plain,
! [X0] :
( ~ element(join_on_relstr(sF30,X0),the_carrier(sF30))
| element(join_on_relstr(sF30,X0),the_carrier(sK25)) ),
inference(forward_demodulation,[],[f1140,f420]) ).
fof(f1148,plain,
! [X0,X1] :
( ~ relstr_set_smaller(sF30,X1,join_on_relstr(sF30,X0))
| ~ element(join_on_relstr(sF30,X0),the_carrier(sF30))
| latt_element_smaller(sK25,join_on_relstr(sF30,X0),X1) ),
inference(forward_demodulation,[],[f1143,f420]) ).
fof(f1153,plain,
( element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(poset_of_lattice(sK25))) ),
inference(superposition,[],[f294,f1117]) ).
fof(f1162,plain,
( element(sF31,the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1153,f386]) ).
fof(f1164,definition,
( spl34_29
<=> element(sF31,the_carrier(sF30)) ),
introduced(definition,[new_symbols(definition,[spl34_29])],[avatar_definition]) ).
fof(f1166,plain,
( ~ element(sF31,the_carrier(sF30))
| spl34_29 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1194,plain,
( element(sF31,the_carrier(sK25))
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1162,f385]) ).
fof(f1199,plain,
( element(sF31,the_carrier(sK25))
| ~ element(sF31,the_carrier(poset_of_lattice(sK25))) ),
inference(forward_subsumption_resolution,[],[f1194,f383]) ).
fof(f1204,plain,
( ~ element(sF31,the_carrier(sF30))
| element(sF31,the_carrier(sK25)) ),
inference(forward_demodulation,[],[f1199,f420]) ).
fof(f1210,definition,
( spl34_35
<=> element(sF31,the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_35])],[avatar_definition]) ).
fof(f1212,plain,
( element(sF31,the_carrier(sK25))
| ~ spl34_35 ),
inference(avatar_component_clause,[],[f1210]) ).
fof(f1213,plain,
( spl34_35
| ~ spl34_29 ),
inference(avatar_split_clause,[],[f1204,f1164,f1210]) ).
fof(f1230,plain,
! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sK25))
| ~ rel_str(sF30) ),
inference(resolution,[],[f1145,f281]) ).
fof(f1353,plain,
! [X0,X1] :
( related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f405,f420]) ).
fof(f1356,plain,
( ! [X0] :
( related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(sF32,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(superposition,[],[f405,f533]) ).
fof(f1360,plain,
( ! [X0] :
( related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f1356,f459]) ).
fof(f1363,plain,
! [X0,X1] :
( related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1353,f386]) ).
fof(f1366,plain,
( ! [X0] :
( related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f1360,f386]) ).
fof(f1369,plain,
! [X0,X1] :
( related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| ~ latt_str(sK25) ),
inference(forward_subsumption_resolution,[],[f1363,f385]) ).
fof(f1372,plain,
( ! [X0] :
( related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| ~ latt_str(sK25) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f1366,f385]) ).
fof(f1375,plain,
! [X0,X1] :
( related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25)) ),
inference(forward_subsumption_resolution,[],[f1369,f383]) ).
fof(f1378,plain,
( ! [X0] :
( related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f1372,f383]) ).
fof(f1383,plain,
( ! [X0] :
( related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_4 ),
inference(forward_demodulation,[],[f1378,f420]) ).
fof(f1388,plain,
! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| ~ element(cast_to_el_of_LattPOSet(sK25,X1),the_carrier(sF30)) ),
inference(resolution,[],[f1375,f361]) ).
fof(f1404,plain,
( rel_str(sF30)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f288,f420]) ).
fof(f1405,plain,
( empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| spl34_5 ),
inference(forward_subsumption_resolution,[],[f1404,f480]) ).
fof(f1406,plain,
( ~ lattice(sK25)
| ~ latt_str(sK25)
| spl34_5 ),
inference(forward_subsumption_resolution,[],[f1405,f386]) ).
fof(f1407,plain,
( ~ latt_str(sK25)
| spl34_5 ),
inference(forward_subsumption_resolution,[],[f1406,f385]) ).
fof(f1408,plain,
( $false
| spl34_5 ),
inference(forward_subsumption_resolution,[],[f1407,f383]) ).
fof(f1409,plain,
spl34_5,
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1411,plain,
( ~ rel_str(sF30)
| spl34_29 ),
inference(forward_subsumption_resolution,[],[f498,f1166]) ).
fof(f1414,plain,
( ! [X0] :
( related_reflexive(sF30,sF31,X0)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(X0,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,X0)
| ~ ex_sup_of_relstr_set(sF30,sK26) )
| spl34_9 ),
inference(forward_subsumption_resolution,[],[f894,f574]) ).
fof(f1416,plain,
( ! [X0] : element(join_on_relstr(sF30,X0),the_carrier(sK25))
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f1230,f479]) ).
fof(f1418,plain,
! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30)) ),
inference(forward_subsumption_resolution,[],[f1388,f636]) ).
fof(f1420,definition,
( spl34_51
<=> ex_sup_of_relstr_set(sF30,sK26) ),
introduced(definition,[new_symbols(definition,[spl34_51])],[avatar_definition]) ).
fof(f1421,plain,
( ex_sup_of_relstr_set(sF30,sK26)
| ~ spl34_51 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1422,plain,
( ~ ex_sup_of_relstr_set(sF30,sK26)
| spl34_51 ),
inference(avatar_component_clause,[],[f1420]) ).
fof(f1427,plain,
( $false
| ~ spl34_5
| spl34_29 ),
inference(forward_subsumption_resolution,[],[f1411,f479]) ).
fof(f1428,plain,
( ~ spl34_5
| spl34_29 ),
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1432,plain,
( ! [X0] :
( related_reflexive(sF30,sF31,X0)
| ~ reflexive_relstr(sF30)
| ~ element(X0,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,X0)
| ~ ex_sup_of_relstr_set(sF30,sK26) )
| ~ spl34_5
| spl34_9 ),
inference(forward_subsumption_resolution,[],[f1414,f479]) ).
fof(f1434,plain,
! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30) ),
inference(forward_subsumption_resolution,[],[f1418,f636]) ).
fof(f1436,definition,
( spl34_53
<=> reflexive_relstr(sF30) ),
introduced(definition,[new_symbols(definition,[spl34_53])],[avatar_definition]) ).
fof(f1437,plain,
( reflexive_relstr(sF30)
| ~ spl34_53 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1438,plain,
( ~ reflexive_relstr(sF30)
| spl34_53 ),
inference(avatar_component_clause,[],[f1436]) ).
fof(f1440,definition,
( spl34_54
<=> ! [X0] :
( related_reflexive(sF30,sF31,X0)
| ~ relstr_set_smaller(sF30,sK26,X0)
| ~ element(X0,the_carrier(sF30)) ) ),
introduced(definition,[new_symbols(definition,[spl34_54])],[avatar_definition]) ).
fof(f1441,plain,
( ! [X0] :
( ~ relstr_set_smaller(sF30,sK26,X0)
| related_reflexive(sF30,sF31,X0)
| ~ element(X0,the_carrier(sF30)) )
| ~ spl34_54 ),
inference(avatar_component_clause,[],[f1440]) ).
fof(f1442,plain,
( ~ spl34_51
| ~ spl34_53
| spl34_54
| ~ spl34_5
| spl34_9 ),
inference(avatar_split_clause,[],[f1432,f573,f478,f1440,f1436,f1420]) ).
fof(f1443,plain,
( ! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30) )
| spl34_9 ),
inference(forward_subsumption_resolution,[],[f1434,f574]) ).
fof(f1444,plain,
( ! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| ~ element(X1,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ reflexive_relstr(sF30) )
| ~ spl34_5
| spl34_9 ),
inference(forward_subsumption_resolution,[],[f1443,f479]) ).
fof(f1446,definition,
( spl34_55
<=> ! [X0,X1] :
( ~ below_refl(sK25,X0,X1)
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ element(X0,the_carrier(sK25))
| ~ element(X1,the_carrier(sK25)) ) ),
introduced(definition,[new_symbols(definition,[spl34_55])],[avatar_definition]) ).
fof(f1447,plain,
( ! [X0,X1] :
( related(sF30,cast_to_el_of_LattPOSet(sK25,X0),cast_to_el_of_LattPOSet(sK25,X1))
| ~ below_refl(sK25,X0,X1)
| ~ element(X0,the_carrier(sK25))
| ~ element(X1,the_carrier(sK25)) )
| ~ spl34_55 ),
inference(avatar_component_clause,[],[f1446]) ).
fof(f1448,plain,
( ~ spl34_53
| spl34_55
| ~ spl34_5
| spl34_9 ),
inference(avatar_split_clause,[],[f1444,f573,f478,f1446,f1436]) ).
fof(f1450,plain,
( sF31 = cast_to_el_of_LattPOSet(sK25,sF31)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_35 ),
inference(resolution,[],[f1212,f270]) ).
fof(f1451,plain,
( sF31 = cast_to_el_of_LattPOSet(sK25,sF31)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_35 ),
inference(forward_subsumption_resolution,[],[f1450,f386]) ).
fof(f1452,plain,
( sF31 = cast_to_el_of_LattPOSet(sK25,sF31)
| ~ latt_str(sK25)
| ~ spl34_35 ),
inference(forward_subsumption_resolution,[],[f1451,f385]) ).
fof(f1453,plain,
( sF31 = cast_to_el_of_LattPOSet(sK25,sF31)
| ~ spl34_35 ),
inference(forward_subsumption_resolution,[],[f1452,f383]) ).
fof(f1622,plain,
( ! [X0] :
( join_on_relstr(sF30,X0) = cast_to_el_of_LattPOSet(sK25,join_on_relstr(sF30,X0))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_5 ),
inference(resolution,[],[f1416,f270]) ).
fof(f1624,plain,
( ! [X0] :
( join_on_relstr(sF30,X0) = cast_to_el_of_LattPOSet(sK25,join_on_relstr(sF30,X0))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f1622,f386]) ).
fof(f1625,plain,
( ! [X0] :
( join_on_relstr(sF30,X0) = cast_to_el_of_LattPOSet(sK25,join_on_relstr(sF30,X0))
| ~ latt_str(sK25) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f1624,f385]) ).
fof(f1626,plain,
( ! [X0] : join_on_relstr(sF30,X0) = cast_to_el_of_LattPOSet(sK25,join_on_relstr(sF30,X0))
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f1625,f383]) ).
fof(f1712,plain,
( ! [X0] :
( ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(cast_to_el_of_LattPOSet(sK25,X0),the_carrier(sF30))
| ~ element(sF32,the_carrier(sF30)) )
| ~ spl34_4 ),
inference(resolution,[],[f1383,f361]) ).
fof(f1795,plain,
( ! [X0] :
( element(join_on_relstr(sF30,X0),the_carrier(sF30))
| ~ element(join_on_relstr(sF30,X0),the_carrier(sK25)) )
| ~ spl34_5 ),
inference(superposition,[],[f636,f1626]) ).
fof(f1830,plain,
( ! [X0] : element(join_on_relstr(sF30,X0),the_carrier(sF30))
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f1795,f1416]) ).
fof(f1865,plain,
( relstr_element_smaller(sF30,sK26,sF32)
| ~ spl34_3
| ~ spl34_4 ),
inference(resolution,[],[f657,f456]) ).
fof(f1906,plain,
( reflexive_relstr(sF30)
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) ),
inference(superposition,[],[f325,f420]) ).
fof(f1907,plain,
( empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| spl34_53 ),
inference(forward_subsumption_resolution,[],[f1906,f1438]) ).
fof(f1908,plain,
( ~ lattice(sK25)
| ~ latt_str(sK25)
| spl34_53 ),
inference(forward_subsumption_resolution,[],[f1907,f386]) ).
fof(f1909,plain,
( ~ latt_str(sK25)
| spl34_53 ),
inference(forward_subsumption_resolution,[],[f1908,f385]) ).
fof(f1910,plain,
( $false
| spl34_53 ),
inference(forward_subsumption_resolution,[],[f1909,f383]) ).
fof(f1911,plain,
spl34_53,
inference(avatar_contradiction_clause,[],[f1910]) ).
fof(f1912,plain,
( ! [X0] :
( ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(sF32,the_carrier(sF30)) )
| ~ spl34_4 ),
inference(forward_subsumption_resolution,[],[f1712,f636]) ).
fof(f1915,plain,
( ! [X0] :
( ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(sF32,the_carrier(sF30)) )
| ~ spl34_4
| spl34_9 ),
inference(forward_subsumption_resolution,[],[f1912,f574]) ).
fof(f1918,plain,
( ! [X0] :
( ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ rel_str(sF30)
| ~ element(sF32,the_carrier(sF30)) )
| ~ spl34_4
| spl34_9
| ~ spl34_53 ),
inference(forward_subsumption_resolution,[],[f1915,f1437]) ).
fof(f1921,plain,
( ! [X0] :
( ~ below_refl(sK25,X0,sF32)
| ~ element(X0,the_carrier(sK25))
| related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ element(sF32,the_carrier(sF30)) )
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53 ),
inference(forward_subsumption_resolution,[],[f1918,f479]) ).
fof(f1924,plain,
( ! [X0] :
( related(sF30,cast_to_el_of_LattPOSet(sK25,X0),sF32)
| ~ element(X0,the_carrier(sK25))
| ~ below_refl(sK25,X0,sF32) )
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53 ),
inference(forward_subsumption_resolution,[],[f1921,f642]) ).
fof(f1931,plain,
( ! [X0] :
( related(sF30,sF29,cast_to_el_of_LattPOSet(sK25,X0))
| ~ below_refl(sK25,sF29,X0)
| ~ element(sF29,the_carrier(sK25))
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_55 ),
inference(superposition,[],[f1447,f532]) ).
fof(f1948,plain,
( ! [X0] :
( related(sF30,sF29,cast_to_el_of_LattPOSet(sK25,X0))
| ~ below_refl(sK25,sF29,X0)
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_55 ),
inference(forward_subsumption_resolution,[],[f1931,f464]) ).
fof(f1958,plain,
relstr_set_smaller(sF30,sK26,sF29),
inference(resolution,[],[f954,f504]) ).
fof(f2013,plain,
! [X2,X0,X1] :
( ~ latt_element_smaller(X0,X1,X2)
| join_of_latt_set(X0,X2) = X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| sK1(X0,X2,X1) = cast_to_el_of_LattPOSet(X0,sK1(X0,X2,X1))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(resolution,[],[f430,f270]) ).
fof(f2017,plain,
! [X2,X0,X1] :
( ~ latt_element_smaller(X0,X1,X2)
| join_of_latt_set(X0,X2) = X1
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ complete_latt_str(X0)
| ~ latt_str(X0)
| sK1(X0,X2,X1) = cast_to_el_of_LattPOSet(X0,sK1(X0,X2,X1)) ),
inference(duplicate_literal_removal,[],[f2013]) ).
fof(f2032,plain,
! [X0] :
( ~ element(join_on_relstr(sF30,X0),the_carrier(sF30))
| latt_element_smaller(sK25,join_on_relstr(sF30,X0),X0)
| ~ ex_sup_of_relstr_set(sF30,X0)
| ~ rel_str(sF30) ),
inference(resolution,[],[f1148,f443]) ).
fof(f2034,plain,
( ! [X0] :
( ~ element(join_on_relstr(sF30,X0),the_carrier(sF30))
| latt_element_smaller(sK25,join_on_relstr(sF30,X0),X0)
| ~ ex_sup_of_relstr_set(sF30,X0) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f2032,f479]) ).
fof(f2035,plain,
( ! [X0] :
( latt_element_smaller(sK25,join_on_relstr(sF30,X0),X0)
| ~ ex_sup_of_relstr_set(sF30,X0) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f2034,f1830]) ).
fof(f2089,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,X1,X0)
| ex_sup_of_relstr_set(sF30,X1)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| sK21(sF30,X1,X0) = cast_to_el_of_lattice(sK25,sK21(sF30,X1,X0)) ),
inference(resolution,[],[f369,f563]) ).
fof(f2091,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,X1,X0)
| ex_sup_of_relstr_set(sF30,X1)
| ~ rel_str(sF30)
| sK21(sF30,X1,X0) = cast_to_el_of_lattice(sK25,sK21(sF30,X1,X0)) ),
inference(forward_subsumption_resolution,[],[f2089,f1040]) ).
fof(f2093,plain,
( ! [X0,X1] :
( ~ relstr_set_smaller(sF30,X1,X0)
| ~ element(X0,the_carrier(sF30))
| ex_sup_of_relstr_set(sF30,X1)
| sK21(sF30,X1,X0) = cast_to_el_of_lattice(sK25,sK21(sF30,X1,X0)) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f2091,f479]) ).
fof(f2095,plain,
( ~ element(sF29,the_carrier(sF30))
| ex_sup_of_relstr_set(sF30,sK26)
| sK21(sF30,sK26,sF29) = cast_to_el_of_lattice(sK25,sK21(sF30,sK26,sF29))
| ~ spl34_5 ),
inference(resolution,[],[f2093,f1958]) ).
fof(f2103,plain,
( ex_sup_of_relstr_set(sF30,sK26)
| sK21(sF30,sK26,sF29) = cast_to_el_of_lattice(sK25,sK21(sF30,sK26,sF29))
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f2095,f641]) ).
fof(f2105,plain,
( sK21(sF30,sK26,sF29) = cast_to_el_of_lattice(sK25,sK21(sF30,sK26,sF29))
| ~ spl34_5
| spl34_51 ),
inference(forward_subsumption_resolution,[],[f2103,f1422]) ).
fof(f2109,plain,
( below_refl(sK25,sF29,sK21(sF30,sK26,sF29))
| ~ relstr_set_smaller(sF30,sK26,sK21(sF30,sK26,sF29))
| ~ element(sK21(sF30,sK26,sF29),the_carrier(sF30))
| ~ spl34_5
| spl34_51 ),
inference(superposition,[],[f806,f2105]) ).
fof(f2112,plain,
( element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK21(sF30,sK26,sF29),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_5
| spl34_51 ),
inference(superposition,[],[f294,f2105]) ).
fof(f2121,plain,
( element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK21(sF30,sK26,sF29),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_5
| spl34_51 ),
inference(forward_subsumption_resolution,[],[f2112,f386]) ).
fof(f2123,definition,
( spl34_66
<=> element(sK21(sF30,sK26,sF29),the_carrier(sF30)) ),
introduced(definition,[new_symbols(definition,[spl34_66])],[avatar_definition]) ).
fof(f2125,plain,
( ~ element(sK21(sF30,sK26,sF29),the_carrier(sF30))
| spl34_66 ),
inference(avatar_component_clause,[],[f2123]) ).
fof(f2136,definition,
( spl34_69
<=> relstr_set_smaller(sF30,sK26,sK21(sF30,sK26,sF29)) ),
introduced(definition,[new_symbols(definition,[spl34_69])],[avatar_definition]) ).
fof(f2138,plain,
( ~ relstr_set_smaller(sF30,sK26,sK21(sF30,sK26,sF29))
| spl34_69 ),
inference(avatar_component_clause,[],[f2136]) ).
fof(f2145,definition,
( spl34_71
<=> below_refl(sK25,sF29,sK21(sF30,sK26,sF29)) ),
introduced(definition,[new_symbols(definition,[spl34_71])],[avatar_definition]) ).
fof(f2147,plain,
( below_refl(sK25,sF29,sK21(sF30,sK26,sF29))
| ~ spl34_71 ),
inference(avatar_component_clause,[],[f2145]) ).
fof(f2148,plain,
( ~ spl34_66
| ~ spl34_69
| spl34_71
| ~ spl34_5
| spl34_51 ),
inference(avatar_split_clause,[],[f2109,f1420,f478,f2145,f2136,f2123]) ).
fof(f2161,plain,
( element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ latt_str(sK25)
| ~ element(sK21(sF30,sK26,sF29),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_5
| spl34_51 ),
inference(forward_subsumption_resolution,[],[f2121,f385]) ).
fof(f2166,plain,
( element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ element(sK21(sF30,sK26,sF29),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_5
| spl34_51 ),
inference(forward_subsumption_resolution,[],[f2161,f383]) ).
fof(f2171,plain,
( ~ element(sK21(sF30,sK26,sF29),the_carrier(sF30))
| element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ spl34_5
| spl34_51 ),
inference(forward_demodulation,[],[f2166,f420]) ).
fof(f2177,definition,
( spl34_74
<=> element(sK21(sF30,sK26,sF29),the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_74])],[avatar_definition]) ).
fof(f2179,plain,
( element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ spl34_74 ),
inference(avatar_component_clause,[],[f2177]) ).
fof(f2180,plain,
( spl34_74
| ~ spl34_66
| ~ spl34_5
| spl34_51 ),
inference(avatar_split_clause,[],[f2171,f1420,f478,f2123,f2177]) ).
fof(f2197,plain,
( ~ element(sF29,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_66 ),
inference(resolution,[],[f2125,f369]) ).
fof(f2198,plain,
( ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_66 ),
inference(forward_subsumption_resolution,[],[f2197,f641]) ).
fof(f2199,plain,
( ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_66 ),
inference(forward_subsumption_resolution,[],[f2198,f1958]) ).
fof(f2200,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_51
| spl34_66 ),
inference(forward_subsumption_resolution,[],[f2199,f1422]) ).
fof(f2201,plain,
( ~ rel_str(sF30)
| spl34_51
| spl34_66 ),
inference(forward_subsumption_resolution,[],[f2200,f1040]) ).
fof(f2202,plain,
( $false
| ~ spl34_5
| spl34_51
| spl34_66 ),
inference(forward_subsumption_resolution,[],[f2201,f479]) ).
fof(f2203,plain,
( ~ spl34_5
| spl34_51
| spl34_66 ),
inference(avatar_contradiction_clause,[],[f2202]) ).
fof(f2343,definition,
( spl34_83
<=> sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31)) ),
introduced(definition,[new_symbols(definition,[spl34_83])],[avatar_definition]) ).
fof(f2344,plain,
( sK1(sK25,sK26,sF31) != cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| spl34_83 ),
inference(avatar_component_clause,[],[f2343]) ).
fof(f2345,plain,
( sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_83 ),
inference(avatar_component_clause,[],[f2343]) ).
fof(f2354,definition,
( spl34_84
<=> latt_element_smaller(sK25,sF31,sK26) ),
introduced(definition,[new_symbols(definition,[spl34_84])],[avatar_definition]) ).
fof(f2355,plain,
( latt_element_smaller(sK25,sF31,sK26)
| ~ spl34_84 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2356,plain,
( ~ latt_element_smaller(sK25,sF31,sK26)
| spl34_84 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2374,plain,
( sK21(sF30,sK26,sF29) = cast_to_el_of_LattPOSet(sK25,sK21(sF30,sK26,sF29))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_74 ),
inference(resolution,[],[f2179,f270]) ).
fof(f2375,plain,
( sK21(sF30,sK26,sF29) = cast_to_el_of_LattPOSet(sK25,sK21(sF30,sK26,sF29))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f2374,f386]) ).
fof(f2376,plain,
( sK21(sF30,sK26,sF29) = cast_to_el_of_LattPOSet(sK25,sK21(sF30,sK26,sF29))
| ~ latt_str(sK25)
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f2375,f385]) ).
fof(f2377,plain,
( sK21(sF30,sK26,sF29) = cast_to_el_of_LattPOSet(sK25,sK21(sF30,sK26,sF29))
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f2376,f383]) ).
fof(f2561,definition,
( spl34_91
<=> element(sK23(sF30,sK26,sF32),the_carrier(sF30)) ),
introduced(definition,[new_symbols(definition,[spl34_91])],[avatar_definition]) ).
fof(f2562,plain,
( element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ spl34_91 ),
inference(avatar_component_clause,[],[f2561]) ).
fof(f2563,plain,
( ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| spl34_91 ),
inference(avatar_component_clause,[],[f2561]) ).
fof(f2565,definition,
( spl34_92
<=> relstr_element_smaller(sF30,sK26,sK23(sF30,sK26,sF32)) ),
introduced(definition,[new_symbols(definition,[spl34_92])],[avatar_definition]) ).
fof(f2567,plain,
( ~ relstr_element_smaller(sF30,sK26,sK23(sF30,sK26,sF32))
| spl34_92 ),
inference(avatar_component_clause,[],[f2565]) ).
fof(f2569,definition,
( spl34_93
<=> below_refl(sK25,sK23(sF30,sK26,sF32),sF32) ),
introduced(definition,[new_symbols(definition,[spl34_93])],[avatar_definition]) ).
fof(f2600,definition,
( spl34_100
<=> element(sK23(sF30,sK26,sF32),the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_100])],[avatar_definition]) ).
fof(f2601,plain,
( element(sK23(sF30,sK26,sF32),the_carrier(sK25))
| ~ spl34_100 ),
inference(avatar_component_clause,[],[f2600]) ).
fof(f2602,plain,
( ~ element(sK23(sF30,sK26,sF32),the_carrier(sK25))
| spl34_100 ),
inference(avatar_component_clause,[],[f2600]) ).
fof(f2640,plain,
( ~ element(sF32,the_carrier(sF30))
| ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_91 ),
inference(resolution,[],[f2563,f375]) ).
fof(f2641,plain,
( ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_4
| spl34_91 ),
inference(forward_subsumption_resolution,[],[f2640,f642]) ).
fof(f2642,plain,
( ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_91 ),
inference(forward_subsumption_resolution,[],[f2641,f1865]) ).
fof(f2643,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_6
| spl34_91 ),
inference(forward_subsumption_resolution,[],[f2642,f484]) ).
fof(f2644,plain,
( ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_6
| spl34_91 ),
inference(forward_subsumption_resolution,[],[f2643,f1040]) ).
fof(f2645,plain,
( $false
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_91 ),
inference(forward_subsumption_resolution,[],[f2644,f479]) ).
fof(f2646,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_91 ),
inference(avatar_contradiction_clause,[],[f2645]) ).
fof(f2780,plain,
( ~ element(sF29,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_69 ),
inference(resolution,[],[f2138,f370]) ).
fof(f2781,plain,
( ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_69 ),
inference(forward_subsumption_resolution,[],[f2780,f641]) ).
fof(f2782,plain,
( ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_69 ),
inference(forward_subsumption_resolution,[],[f2781,f1958]) ).
fof(f2783,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_51
| spl34_69 ),
inference(forward_subsumption_resolution,[],[f2782,f1422]) ).
fof(f2784,plain,
( ~ rel_str(sF30)
| spl34_51
| spl34_69 ),
inference(forward_subsumption_resolution,[],[f2783,f1040]) ).
fof(f2785,plain,
( $false
| ~ spl34_5
| spl34_51
| spl34_69 ),
inference(forward_subsumption_resolution,[],[f2784,f479]) ).
fof(f2786,plain,
( ~ spl34_5
| spl34_51
| spl34_69 ),
inference(avatar_contradiction_clause,[],[f2785]) ).
fof(f2963,plain,
( sK23(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK23(sF30,sK26,sF32))
| ~ spl34_91 ),
inference(resolution,[],[f2562,f563]) ).
fof(f2968,plain,
( sK23(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK23(sF30,sK26,sF32))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_100 ),
inference(resolution,[],[f2601,f270]) ).
fof(f2969,plain,
( sK23(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK23(sF30,sK26,sF32))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f2968,f386]) ).
fof(f2970,plain,
( sK23(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK23(sF30,sK26,sF32))
| ~ latt_str(sK25)
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f2969,f385]) ).
fof(f2971,plain,
( sK23(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK23(sF30,sK26,sF32))
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f2970,f383]) ).
fof(f3009,plain,
( related_reflexive(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ below_refl(sK25,sK23(sF30,sK26,sF32),sF32)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sK25))
| ~ spl34_4
| ~ spl34_100 ),
inference(superposition,[],[f1383,f2971]) ).
fof(f3037,plain,
( related_reflexive(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ below_refl(sK25,sK23(sF30,sK26,sF32),sF32)
| ~ spl34_4
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f3009,f2601]) ).
fof(f3072,definition,
( spl34_130
<=> related_reflexive(sF30,sK23(sF30,sK26,sF32),sF32) ),
introduced(definition,[new_symbols(definition,[spl34_130])],[avatar_definition]) ).
fof(f3074,plain,
( related_reflexive(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ spl34_130 ),
inference(avatar_component_clause,[],[f3072]) ).
fof(f3075,plain,
( ~ spl34_93
| spl34_130
| ~ spl34_4
| ~ spl34_100 ),
inference(avatar_split_clause,[],[f3037,f2600,f458,f3072,f2569]) ).
fof(f3440,plain,
( latt_element_smaller(sK25,sF31,sK26)
| ~ ex_sup_of_relstr_set(sF30,sK26)
| ~ spl34_5 ),
inference(superposition,[],[f2035,f422]) ).
fof(f3455,plain,
! [X0,X1] :
( ~ relstr_element_smaller(sF30,X0,X1)
| meet_on_relstr(sF30,X0) = X1
| ~ ex_inf_of_relstr_set(sF30,X0)
| ~ element(X1,the_carrier(sF30))
| ~ rel_str(sF30)
| sK0(sF30,X0,X1) = cast_to_el_of_lattice(sK25,sK0(sF30,X0,X1)) ),
inference(resolution,[],[f260,f563]) ).
fof(f3457,plain,
( ! [X0,X1] :
( ~ relstr_element_smaller(sF30,X0,X1)
| meet_on_relstr(sF30,X0) = X1
| ~ ex_inf_of_relstr_set(sF30,X0)
| ~ element(X1,the_carrier(sF30))
| sK0(sF30,X0,X1) = cast_to_el_of_lattice(sK25,sK0(sF30,X0,X1)) )
| ~ spl34_5 ),
inference(forward_subsumption_resolution,[],[f3455,f479]) ).
fof(f3463,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| sK0(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK0(sF30,sK26,sF32))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5 ),
inference(resolution,[],[f3457,f1865]) ).
fof(f3473,plain,
( ~ element(sF32,the_carrier(sF30))
| ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_92 ),
inference(resolution,[],[f2567,f376]) ).
fof(f3474,plain,
( ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_4
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f3473,f642]) ).
fof(f3475,plain,
( ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f3474,f1865]) ).
fof(f3476,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_6
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f3475,f484]) ).
fof(f3477,plain,
( ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_6
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f3476,f1040]) ).
fof(f3478,plain,
( $false
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f3477,f479]) ).
fof(f3479,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_92 ),
inference(avatar_contradiction_clause,[],[f3478]) ).
fof(f3490,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| sK0(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK0(sF30,sK26,sF32))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3463,f483]) ).
fof(f3493,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| sK0(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK0(sF30,sK26,sF32))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3490,f642]) ).
fof(f3495,plain,
( sF32 = sF33
| sK0(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK0(sF30,sK26,sF32))
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_demodulation,[],[f3493,f426]) ).
fof(f3496,plain,
( sK0(sF30,sK26,sF32) = cast_to_el_of_lattice(sK25,sK0(sF30,sK26,sF32))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3495,f436]) ).
fof(f3506,plain,
( element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(superposition,[],[f294,f3496]) ).
fof(f3510,plain,
( ! [X0] :
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0)
| ~ relstr_element_smaller(poset_of_lattice(sK25),X0,sK0(sF30,sK26,sF32))
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(superposition,[],[f381,f3496]) ).
fof(f3511,plain,
( ! [X0] :
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0)
| ~ relstr_element_smaller(poset_of_lattice(sK25),X0,sK0(sF30,sK26,sF32))
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3510,f386]) ).
fof(f3515,plain,
( element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3506,f386]) ).
fof(f3517,definition,
( spl34_141
<=> element(sK0(sF30,sK26,sF32),the_carrier(sF30)) ),
introduced(definition,[new_symbols(definition,[spl34_141])],[avatar_definition]) ).
fof(f3519,plain,
( ~ element(sK0(sF30,sK26,sF32),the_carrier(sF30))
| spl34_141 ),
inference(avatar_component_clause,[],[f3517]) ).
fof(f3525,definition,
( spl34_143
<=> below_refl(sK25,sK0(sF30,sK26,sF32),sF32) ),
introduced(definition,[new_symbols(definition,[spl34_143])],[avatar_definition]) ).
fof(f3527,plain,
( below_refl(sK25,sK0(sF30,sK26,sF32),sF32)
| ~ spl34_143 ),
inference(avatar_component_clause,[],[f3525]) ).
fof(f3556,definition,
( spl34_150
<=> element(sK0(sF30,sK26,sF32),the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_150])],[avatar_definition]) ).
fof(f3557,plain,
( element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| ~ spl34_150 ),
inference(avatar_component_clause,[],[f3556]) ).
fof(f3560,plain,
( ! [X0] :
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0)
| ~ relstr_element_smaller(poset_of_lattice(sK25),X0,sK0(sF30,sK26,sF32))
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3511,f385]) ).
fof(f3564,plain,
( element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| ~ latt_str(sK25)
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3515,f385]) ).
fof(f3565,plain,
( ! [X0] :
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0)
| ~ relstr_element_smaller(poset_of_lattice(sK25),X0,sK0(sF30,sK26,sF32))
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25))) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3560,f383]) ).
fof(f3569,plain,
( element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_subsumption_resolution,[],[f3564,f383]) ).
fof(f3570,plain,
( ! [X0] :
( ~ relstr_element_smaller(sF30,X0,sK0(sF30,sK26,sF32))
| latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0)
| ~ element(sK0(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25))) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_demodulation,[],[f3565,f420]) ).
fof(f3574,plain,
( ~ element(sK0(sF30,sK26,sF32),the_carrier(sF30))
| element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_demodulation,[],[f3569,f420]) ).
fof(f3575,plain,
( ! [X0] :
( ~ element(sK0(sF30,sK26,sF32),the_carrier(sF30))
| ~ relstr_element_smaller(sF30,X0,sK0(sF30,sK26,sF32))
| latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0) )
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(forward_demodulation,[],[f3570,f420]) ).
fof(f3579,plain,
( spl34_150
| ~ spl34_141
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(avatar_split_clause,[],[f3574,f482,f478,f458,f454,f434,f3517,f3556]) ).
fof(f3581,definition,
( spl34_151
<=> ! [X0] :
( ~ relstr_element_smaller(sF30,X0,sK0(sF30,sK26,sF32))
| latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_151])],[avatar_definition]) ).
fof(f3582,plain,
( ! [X0] :
( ~ relstr_element_smaller(sF30,X0,sK0(sF30,sK26,sF32))
| latt_set_smaller(sK25,sK0(sF30,sK26,sF32),X0) )
| ~ spl34_151 ),
inference(avatar_component_clause,[],[f3581]) ).
fof(f3583,plain,
( spl34_151
| ~ spl34_141
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6 ),
inference(avatar_split_clause,[],[f3575,f482,f478,f458,f454,f434,f3517,f3581]) ).
fof(f3597,plain,
( ~ relstr_element_smaller(sF30,sK26,sF32)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| spl34_141 ),
inference(resolution,[],[f3519,f260]) ).
fof(f3598,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| spl34_141 ),
inference(forward_subsumption_resolution,[],[f3597,f1865]) ).
fof(f3599,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_6
| spl34_141 ),
inference(forward_subsumption_resolution,[],[f3598,f483]) ).
fof(f3600,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_6
| spl34_141 ),
inference(forward_subsumption_resolution,[],[f3599,f642]) ).
fof(f3601,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_141 ),
inference(forward_subsumption_resolution,[],[f3600,f479]) ).
fof(f3602,plain,
( sF32 = sF33
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_141 ),
inference(forward_demodulation,[],[f3601,f426]) ).
fof(f3603,plain,
( $false
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_141 ),
inference(forward_subsumption_resolution,[],[f3602,f436]) ).
fof(f3604,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_141 ),
inference(avatar_contradiction_clause,[],[f3603]) ).
fof(f3703,plain,
( below_refl(sK25,sK23(sF30,sK26,sF32),sF32)
| ~ relstr_element_smaller(sF30,sK26,sK23(sF30,sK26,sF32))
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ spl34_4
| ~ spl34_91 ),
inference(superposition,[],[f613,f2963]) ).
fof(f3704,plain,
( element(sK23(sF30,sK26,sF32),the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_91 ),
inference(superposition,[],[f294,f2963]) ).
fof(f3713,plain,
( empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_91
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f3704,f2602]) ).
fof(f3714,plain,
( below_refl(sK25,sK23(sF30,sK26,sF32),sF32)
| ~ relstr_element_smaller(sF30,sK26,sK23(sF30,sK26,sF32))
| ~ spl34_4
| ~ spl34_91 ),
inference(forward_subsumption_resolution,[],[f3703,f2562]) ).
fof(f3719,plain,
( ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_91
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f3713,f386]) ).
fof(f3720,plain,
( ~ spl34_92
| spl34_93
| ~ spl34_4
| ~ spl34_91 ),
inference(avatar_split_clause,[],[f3714,f2561,f458,f2569,f2565]) ).
fof(f3725,plain,
( ~ latt_str(sK25)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_91
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f3719,f385]) ).
fof(f3730,plain,
( ~ element(sK23(sF30,sK26,sF32),the_carrier(poset_of_lattice(sK25)))
| ~ spl34_91
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f3725,f383]) ).
fof(f3731,plain,
( ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ spl34_91
| spl34_100 ),
inference(forward_demodulation,[],[f3730,f420]) ).
fof(f3732,plain,
( $false
| ~ spl34_91
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f3731,f2562]) ).
fof(f3733,plain,
( ~ spl34_91
| spl34_100 ),
inference(avatar_contradiction_clause,[],[f3732]) ).
fof(f3935,plain,
( ~ ex_sup_of_relstr_set(sF30,sK26)
| ~ spl34_5
| spl34_84 ),
inference(forward_subsumption_resolution,[],[f3440,f2356]) ).
fof(f3945,plain,
( $false
| ~ spl34_5
| ~ spl34_51
| spl34_84 ),
inference(forward_subsumption_resolution,[],[f3935,f1421]) ).
fof(f3946,plain,
( ~ spl34_5
| ~ spl34_51
| spl34_84 ),
inference(avatar_contradiction_clause,[],[f3945]) ).
fof(f4095,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(poset_of_lattice(sK25)))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_83 ),
inference(superposition,[],[f293,f2345]) ).
fof(f4098,plain,
( ! [X0] :
( relstr_set_smaller(poset_of_lattice(sK25),X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(superposition,[],[f391,f2345]) ).
fof(f4103,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(superposition,[],[f406,f2345]) ).
fof(f4104,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4103,f386]) ).
fof(f4109,plain,
( ! [X0] :
( relstr_set_smaller(poset_of_lattice(sK25),X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ lattice(sK25)
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4098,f386]) ).
fof(f4112,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(poset_of_lattice(sK25)))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4095,f386]) ).
fof(f4114,definition,
( spl34_185
<=> element(sK1(sK25,sK26,sF31),the_carrier(sK25)) ),
introduced(definition,[new_symbols(definition,[spl34_185])],[avatar_definition]) ).
fof(f4115,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_185 ),
inference(avatar_component_clause,[],[f4114]) ).
fof(f4116,plain,
( ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| spl34_185 ),
inference(avatar_component_clause,[],[f4114]) ).
fof(f4127,definition,
( spl34_188
<=> ! [X0] :
( relstr_set_smaller(sF30,X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_188])],[avatar_definition]) ).
fof(f4128,plain,
( ! [X0] :
( ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| relstr_set_smaller(sF30,X0,sK1(sK25,sK26,sF31)) )
| ~ spl34_188 ),
inference(avatar_component_clause,[],[f4127]) ).
fof(f4199,definition,
( spl34_204
<=> ! [X0] :
( ~ related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31)) ) ),
introduced(definition,[new_symbols(definition,[spl34_204])],[avatar_definition]) ).
fof(f4200,plain,
( ! [X0] :
( ~ related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| ~ element(X0,the_carrier(sK25))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31)) )
| ~ spl34_204 ),
inference(avatar_component_clause,[],[f4199]) ).
fof(f4203,definition,
( spl34_205
<=> element(sK1(sK25,sK26,sF31),the_carrier(sF30)) ),
introduced(definition,[new_symbols(definition,[spl34_205])],[avatar_definition]) ).
fof(f4205,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(sF30))
| ~ spl34_205 ),
inference(avatar_component_clause,[],[f4203]) ).
fof(f4215,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ element(X0,the_carrier(sK25))
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4104,f385]) ).
fof(f4220,plain,
( ! [X0] :
( relstr_set_smaller(poset_of_lattice(sK25),X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ latt_str(sK25) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4109,f385]) ).
fof(f4223,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(poset_of_lattice(sK25)))
| ~ latt_str(sK25)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4112,f385]) ).
fof(f4224,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK25),cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4215,f383]) ).
fof(f4229,plain,
( ! [X0] :
( relstr_set_smaller(poset_of_lattice(sK25),X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25)) )
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4220,f383]) ).
fof(f4232,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(poset_of_lattice(sK25)))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f4223,f383]) ).
fof(f4233,plain,
( ! [X0] :
( ~ related_reflexive(sF30,cast_to_el_of_LattPOSet(sK25,X0),sK1(sK25,sK26,sF31))
| below_refl(sK25,X0,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ element(X0,the_carrier(sK25)) )
| ~ spl34_83 ),
inference(forward_demodulation,[],[f4224,f420]) ).
fof(f4238,plain,
( ! [X0] :
( relstr_set_smaller(sF30,X0,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sK1(sK25,sK26,sF31),X0)
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25)) )
| ~ spl34_83 ),
inference(forward_demodulation,[],[f4229,f420]) ).
fof(f4241,plain,
( element(sK1(sK25,sK26,sF31),the_carrier(sF30))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_83 ),
inference(forward_demodulation,[],[f4232,f420]) ).
fof(f4242,plain,
( ~ spl34_185
| spl34_204
| ~ spl34_83 ),
inference(avatar_split_clause,[],[f4233,f2343,f4199,f4114]) ).
fof(f4247,plain,
( ~ spl34_185
| spl34_188
| ~ spl34_83 ),
inference(avatar_split_clause,[],[f4238,f2343,f4127,f4114]) ).
fof(f4250,plain,
( ~ spl34_185
| spl34_205
| ~ spl34_83 ),
inference(avatar_split_clause,[],[f4241,f2343,f4203,f4114]) ).
fof(f4274,plain,
( ~ latt_element_smaller(sK25,sF31,sK26)
| join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| spl34_185 ),
inference(resolution,[],[f4116,f430]) ).
fof(f4275,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4274,f2355]) ).
fof(f4276,plain,
( join_of_latt_set(sK25,sK26) = sF31
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4275,f1212]) ).
fof(f4277,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4276,f386]) ).
fof(f4278,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4277,f385]) ).
fof(f4279,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4278,f384]) ).
fof(f4280,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4279,f383]) ).
fof(f4281,plain,
( sF29 = sF31
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_demodulation,[],[f4280,f418]) ).
fof(f4282,plain,
( $false
| spl34_2
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(forward_subsumption_resolution,[],[f4281,f440]) ).
fof(f4283,plain,
( spl34_2
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(avatar_contradiction_clause,[],[f4282]) ).
fof(f4300,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_84 ),
inference(resolution,[],[f2355,f2017]) ).
fof(f5033,definition,
( spl34_257
<=> relstr_set_smaller(sF30,sK26,sK1(sK25,sK26,sF31)) ),
introduced(definition,[new_symbols(definition,[spl34_257])],[avatar_definition]) ).
fof(f5034,plain,
( relstr_set_smaller(sF30,sK26,sK1(sK25,sK26,sF31))
| ~ spl34_257 ),
inference(avatar_component_clause,[],[f5033]) ).
fof(f5035,plain,
( ~ relstr_set_smaller(sF30,sK26,sK1(sK25,sK26,sF31))
| spl34_257 ),
inference(avatar_component_clause,[],[f5033]) ).
fof(f5131,plain,
( relstr_set_smaller(sF30,sK26,sK1(sK25,sK26,sF31))
| ~ latt_element_smaller(sK25,sF31,sK26)
| join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_188 ),
inference(resolution,[],[f4128,f431]) ).
fof(f5132,plain,
( ~ latt_element_smaller(sK25,sF31,sK26)
| join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5131,f5035]) ).
fof(f5133,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5132,f2355]) ).
fof(f5134,plain,
( join_of_latt_set(sK25,sK26) = sF31
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5133,f1212]) ).
fof(f5135,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5134,f386]) ).
fof(f5136,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5135,f385]) ).
fof(f5137,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ latt_str(sK25)
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5136,f384]) ).
fof(f5138,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5137,f383]) ).
fof(f5139,plain,
( sF29 = sF31
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_demodulation,[],[f5138,f418]) ).
fof(f5140,plain,
( $false
| spl34_2
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(forward_subsumption_resolution,[],[f5139,f440]) ).
fof(f5141,plain,
( spl34_2
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(avatar_contradiction_clause,[],[f5140]) ).
fof(f5147,plain,
( join_of_latt_set(sK25,sK26) = sF31
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f4300,f1212]) ).
fof(f5165,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5147,f386]) ).
fof(f5172,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5165,f385]) ).
fof(f5176,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ latt_str(sK25)
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5172,f384]) ).
fof(f5179,plain,
( join_of_latt_set(sK25,sK26) = sF31
| sK1(sK25,sK26,sF31) = cast_to_el_of_LattPOSet(sK25,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5176,f383]) ).
fof(f5290,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ spl34_35
| spl34_83
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5179,f2344]) ).
fof(f5303,plain,
( sF29 = sF31
| ~ spl34_35
| spl34_83
| ~ spl34_84 ),
inference(forward_demodulation,[],[f5290,f418]) ).
fof(f5308,plain,
( $false
| spl34_2
| ~ spl34_35
| spl34_83
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f5303,f440]) ).
fof(f5309,plain,
( spl34_2
| ~ spl34_35
| spl34_83
| ~ spl34_84 ),
inference(avatar_contradiction_clause,[],[f5308]) ).
fof(f5358,plain,
( sK0(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK0(sF30,sK26,sF32))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_150 ),
inference(resolution,[],[f3557,f270]) ).
fof(f5359,plain,
( sK0(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK0(sF30,sK26,sF32))
| ~ lattice(sK25)
| ~ latt_str(sK25)
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f5358,f386]) ).
fof(f5361,plain,
( sK0(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK0(sF30,sK26,sF32))
| ~ latt_str(sK25)
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f5359,f385]) ).
fof(f5362,plain,
( sK0(sF30,sK26,sF32) = cast_to_el_of_LattPOSet(sK25,sK0(sF30,sK26,sF32))
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f5361,f383]) ).
fof(f5470,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| ~ relstr_element_smaller(sF30,sK26,sF32)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_151 ),
inference(resolution,[],[f3582,f261]) ).
fof(f5471,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5470,f1865]) ).
fof(f5472,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_6
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5471,f483]) ).
fof(f5473,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_6
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5472,f642]) ).
fof(f5474,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5473,f479]) ).
fof(f5475,plain,
( sF32 = sF33
| latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_151 ),
inference(forward_demodulation,[],[f5474,f426]) ).
fof(f5476,plain,
( latt_set_smaller(sK25,sK0(sF30,sK26,sF32),sK26)
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5475,f436]) ).
fof(f5477,plain,
( ~ element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| below_refl(sK25,sK0(sF30,sK26,sF32),sF32)
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_151 ),
inference(resolution,[],[f5476,f497]) ).
fof(f5479,plain,
( below_refl(sK25,sK0(sF30,sK26,sF32),sF32)
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_150
| ~ spl34_151 ),
inference(forward_subsumption_resolution,[],[f5477,f3557]) ).
fof(f5480,plain,
( spl34_143
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_150
| ~ spl34_151 ),
inference(avatar_split_clause,[],[f5479,f3581,f3556,f482,f478,f458,f454,f434,f3525]) ).
fof(f5663,plain,
( related(sF30,sK0(sF30,sK26,sF32),sF32)
| ~ element(sK0(sF30,sK26,sF32),the_carrier(sK25))
| ~ below_refl(sK25,sK0(sF30,sK26,sF32),sF32)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_150 ),
inference(superposition,[],[f1924,f5362]) ).
fof(f5687,plain,
( related(sF30,sK0(sF30,sK26,sF32),sF32)
| ~ below_refl(sK25,sK0(sF30,sK26,sF32),sF32)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f5663,f3557]) ).
fof(f5726,plain,
( related(sF30,sK0(sF30,sK26,sF32),sF32)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f5687,f3527]) ).
fof(f6152,plain,
( ~ relstr_element_smaller(sF30,sK26,sF32)
| sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(resolution,[],[f5726,f262]) ).
fof(f6154,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ ex_inf_of_relstr_set(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f6152,f1865]) ).
fof(f6155,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ element(sF32,the_carrier(sF30))
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f6154,f483]) ).
fof(f6156,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f6155,f642]) ).
fof(f6157,plain,
( sF32 = meet_on_relstr(sF30,sK26)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f6156,f479]) ).
fof(f6158,plain,
( sF32 = sF33
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_demodulation,[],[f6157,f426]) ).
fof(f6159,plain,
( $false
| spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f6158,f436]) ).
fof(f6160,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(avatar_contradiction_clause,[],[f6159]) ).
fof(f6358,definition,
( spl34_308
<=> below_refl(sK25,sF31,sK1(sK25,sK26,sF31)) ),
introduced(definition,[new_symbols(definition,[spl34_308])],[avatar_definition]) ).
fof(f6359,plain,
( below_refl(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ spl34_308 ),
inference(avatar_component_clause,[],[f6358]) ).
fof(f6360,plain,
( ~ below_refl(sK25,sF31,sK1(sK25,sK26,sF31))
| spl34_308 ),
inference(avatar_component_clause,[],[f6358]) ).
fof(f6471,plain,
( ~ related_reflexive(sF30,sF31,sK1(sK25,sK26,sF31))
| ~ element(sF31,the_carrier(sK25))
| below_refl(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_204 ),
inference(superposition,[],[f4200,f1453]) ).
fof(f6476,plain,
( ~ related_reflexive(sF30,sF31,sK1(sK25,sK26,sF31))
| below_refl(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_204 ),
inference(forward_subsumption_resolution,[],[f6471,f1212]) ).
fof(f6483,plain,
( ~ related_reflexive(sF30,sF31,sK1(sK25,sK26,sF31))
| ~ spl34_35
| ~ spl34_204
| spl34_308 ),
inference(forward_subsumption_resolution,[],[f6476,f6360]) ).
fof(f6970,plain,
( related(sF30,sF29,sK21(sF30,sK26,sF29))
| ~ below_refl(sK25,sF29,sK21(sF30,sK26,sF29))
| ~ element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ spl34_55
| ~ spl34_74 ),
inference(superposition,[],[f1948,f2377]) ).
fof(f6977,plain,
( related(sF30,sF29,sK21(sF30,sK26,sF29))
| ~ element(sK21(sF30,sK26,sF29),the_carrier(sK25))
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f6970,f2147]) ).
fof(f6985,plain,
( related(sF30,sF29,sK21(sF30,sK26,sF29))
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f6977,f2179]) ).
fof(f7006,plain,
( ~ element(sF29,the_carrier(sF30))
| ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(resolution,[],[f6985,f371]) ).
fof(f7009,plain,
( ~ relstr_set_smaller(sF30,sK26,sF29)
| ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f7006,f641]) ).
fof(f7011,plain,
( ex_sup_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f7009,f1958]) ).
fof(f7013,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| spl34_51
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f7011,f1422]) ).
fof(f7015,plain,
( ~ rel_str(sF30)
| spl34_51
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f7013,f1040]) ).
fof(f7017,plain,
( $false
| ~ spl34_5
| spl34_51
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(forward_subsumption_resolution,[],[f7015,f479]) ).
fof(f7018,plain,
( ~ spl34_5
| spl34_51
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(avatar_contradiction_clause,[],[f7017]) ).
fof(f7219,plain,
( related_reflexive(sF30,sF31,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sF30))
| ~ spl34_54
| ~ spl34_257 ),
inference(resolution,[],[f5034,f1441]) ).
fof(f7224,plain,
( ~ element(sK1(sK25,sK26,sF31),the_carrier(sF30))
| ~ spl34_35
| ~ spl34_54
| ~ spl34_204
| ~ spl34_257
| spl34_308 ),
inference(forward_subsumption_resolution,[],[f7219,f6483]) ).
fof(f7226,plain,
( $false
| ~ spl34_35
| ~ spl34_54
| ~ spl34_204
| ~ spl34_205
| ~ spl34_257
| spl34_308 ),
inference(forward_subsumption_resolution,[],[f7224,f4205]) ).
fof(f7227,plain,
( ~ spl34_35
| ~ spl34_54
| ~ spl34_204
| ~ spl34_205
| ~ spl34_257
| spl34_308 ),
inference(avatar_contradiction_clause,[],[f7226]) ).
fof(f7292,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| empty_carrier(sK25)
| ~ meet_commutative(sK25)
| ~ meet_absorbing(sK25)
| ~ join_absorbing(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_308 ),
inference(resolution,[],[f6359,f359]) ).
fof(f7293,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ meet_commutative(sK25)
| ~ meet_absorbing(sK25)
| ~ join_absorbing(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7292,f386]) ).
fof(f7294,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ meet_absorbing(sK25)
| ~ join_absorbing(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_18
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7293,f774]) ).
fof(f7295,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ join_absorbing(sK25)
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_17
| ~ spl34_18
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7294,f770]) ).
fof(f7296,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ latt_str(sK25)
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7295,f766]) ).
fof(f7297,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ element(sF31,the_carrier(sK25))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7296,f383]) ).
fof(f7298,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ element(sK1(sK25,sK26,sF31),the_carrier(sK25))
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7297,f1212]) ).
fof(f7299,plain,
( below(sK25,sF31,sK1(sK25,sK26,sF31))
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7298,f4115]) ).
fof(f7310,plain,
( ~ latt_element_smaller(sK25,sF31,sK26)
| join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_185
| ~ spl34_308 ),
inference(resolution,[],[f7299,f432]) ).
fof(f7312,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ element(sF31,the_carrier(sK25))
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7310,f2355]) ).
fof(f7313,plain,
( join_of_latt_set(sK25,sK26) = sF31
| empty_carrier(sK25)
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7312,f1212]) ).
fof(f7314,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ lattice(sK25)
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7313,f386]) ).
fof(f7315,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ complete_latt_str(sK25)
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7314,f385]) ).
fof(f7316,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ latt_str(sK25)
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7315,f384]) ).
fof(f7317,plain,
( join_of_latt_set(sK25,sK26) = sF31
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7316,f383]) ).
fof(f7318,plain,
( sF29 = sF31
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_demodulation,[],[f7317,f418]) ).
fof(f7319,plain,
( $false
| spl34_2
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(forward_subsumption_resolution,[],[f7318,f440]) ).
fof(f7320,plain,
( spl34_2
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(avatar_contradiction_clause,[],[f7319]) ).
fof(f8188,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| empty_carrier(sF30)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ element(sF32,the_carrier(sF30))
| ~ spl34_130 ),
inference(resolution,[],[f3074,f361]) ).
fof(f8189,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ reflexive_relstr(sF30)
| ~ rel_str(sF30)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ element(sF32,the_carrier(sF30))
| spl34_9
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8188,f574]) ).
fof(f8190,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ rel_str(sF30)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ element(sF32,the_carrier(sF30))
| spl34_9
| ~ spl34_53
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8189,f1437]) ).
fof(f8191,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ element(sK23(sF30,sK26,sF32),the_carrier(sF30))
| ~ element(sF32,the_carrier(sF30))
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8190,f479]) ).
fof(f8192,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ element(sF32,the_carrier(sF30))
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8191,f2562]) ).
fof(f8193,plain,
( related(sF30,sK23(sF30,sK26,sF32),sF32)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8192,f642]) ).
fof(f8355,plain,
( ~ element(sF32,the_carrier(sF30))
| ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(resolution,[],[f8193,f377]) ).
fof(f8357,plain,
( ~ relstr_element_smaller(sF30,sK26,sF32)
| ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8355,f642]) ).
fof(f8358,plain,
( ex_inf_of_relstr_set(sF30,sK26)
| ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8357,f1865]) ).
fof(f8359,plain,
( ~ antisymmetric_relstr(sF30)
| ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8358,f484]) ).
fof(f8360,plain,
( ~ rel_str(sF30)
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8359,f1040]) ).
fof(f8361,plain,
( $false
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(forward_subsumption_resolution,[],[f8360,f479]) ).
fof(f8362,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(avatar_contradiction_clause,[],[f8361]) ).
cnf(s1,plain,
( ~ spl34_1
| ~ spl34_2 ),
inference(sat_conversion,[],[f441]) ).
cnf(s2,plain,
( spl34_3
| ~ spl34_4 ),
inference(sat_conversion,[],[f461]) ).
cnf(s3,plain,
spl34_4,
inference(sat_conversion,[],[f471]) ).
cnf(s7,plain,
~ spl34_9,
inference(sat_conversion,[],[f606]) ).
cnf(s16,plain,
spl34_18,
inference(sat_conversion,[],[f990]) ).
cnf(s17,plain,
spl34_17,
inference(sat_conversion,[],[f1001]) ).
cnf(s19,plain,
spl34_16,
inference(sat_conversion,[],[f1045]) ).
cnf(s25,plain,
( ~ spl34_29
| spl34_35 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s38,plain,
spl34_5,
inference(sat_conversion,[],[f1409]) ).
cnf(s40,plain,
( ~ spl34_5
| spl34_29 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s43,plain,
( ~ spl34_5
| spl34_9
| ~ spl34_51
| ~ spl34_53
| spl34_54 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s44,plain,
( ~ spl34_5
| spl34_9
| ~ spl34_53
| spl34_55 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s58,plain,
spl34_53,
inference(sat_conversion,[],[f1911]) ).
cnf(s62,plain,
( ~ spl34_5
| spl34_51
| ~ spl34_66
| ~ spl34_69
| spl34_71 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s65,plain,
( ~ spl34_5
| spl34_51
| ~ spl34_66
| spl34_74 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s70,plain,
( ~ spl34_5
| spl34_51
| spl34_66 ),
inference(sat_conversion,[],[f2203]) ).
cnf(s91,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_91 ),
inference(sat_conversion,[],[f2646]) ).
cnf(s97,plain,
( ~ spl34_5
| spl34_51
| spl34_69 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s116,plain,
( ~ spl34_4
| ~ spl34_93
| ~ spl34_100
| spl34_130 ),
inference(sat_conversion,[],[f3075]) ).
cnf(s126,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_92 ),
inference(sat_conversion,[],[f3479]) ).
cnf(s139,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_141
| spl34_150 ),
inference(sat_conversion,[],[f3579]) ).
cnf(s140,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| ~ spl34_141
| spl34_151 ),
inference(sat_conversion,[],[f3583]) ).
cnf(s144,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_141 ),
inference(sat_conversion,[],[f3604]) ).
cnf(s145,plain,
( ~ spl34_4
| ~ spl34_91
| ~ spl34_92
| spl34_93 ),
inference(sat_conversion,[],[f3720]) ).
cnf(s146,plain,
( ~ spl34_91
| spl34_100 ),
inference(sat_conversion,[],[f3733]) ).
cnf(s167,plain,
( ~ spl34_5
| ~ spl34_51
| spl34_84 ),
inference(sat_conversion,[],[f3946]) ).
cnf(s203,plain,
( ~ spl34_83
| ~ spl34_185
| spl34_204 ),
inference(sat_conversion,[],[f4242]) ).
cnf(s208,plain,
( ~ spl34_83
| ~ spl34_185
| spl34_188 ),
inference(sat_conversion,[],[f4247]) ).
cnf(s211,plain,
( ~ spl34_83
| ~ spl34_185
| spl34_205 ),
inference(sat_conversion,[],[f4250]) ).
cnf(s213,plain,
( spl34_2
| ~ spl34_35
| ~ spl34_84
| spl34_185 ),
inference(sat_conversion,[],[f4283]) ).
cnf(s272,plain,
( spl34_2
| ~ spl34_35
| ~ spl34_84
| ~ spl34_188
| spl34_257 ),
inference(sat_conversion,[],[f5141]) ).
cnf(s290,plain,
( spl34_2
| ~ spl34_35
| spl34_83
| ~ spl34_84 ),
inference(sat_conversion,[],[f5309]) ).
cnf(s292,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_143
| ~ spl34_150
| ~ spl34_151 ),
inference(sat_conversion,[],[f5480]) ).
cnf(s325,plain,
( spl34_1
| ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| ~ spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_143
| ~ spl34_150 ),
inference(sat_conversion,[],[f6160]) ).
cnf(s372,plain,
( ~ spl34_5
| spl34_51
| ~ spl34_55
| ~ spl34_71
| ~ spl34_74 ),
inference(sat_conversion,[],[f7018]) ).
cnf(s388,plain,
( ~ spl34_35
| ~ spl34_54
| ~ spl34_204
| ~ spl34_205
| ~ spl34_257
| spl34_308 ),
inference(sat_conversion,[],[f7227]) ).
cnf(s393,plain,
( spl34_2
| ~ spl34_16
| ~ spl34_17
| ~ spl34_18
| ~ spl34_35
| ~ spl34_84
| ~ spl34_185
| ~ spl34_308 ),
inference(sat_conversion,[],[f7320]) ).
cnf(s468,plain,
( ~ spl34_3
| ~ spl34_4
| ~ spl34_5
| spl34_6
| spl34_9
| ~ spl34_53
| ~ spl34_91
| ~ spl34_130 ),
inference(sat_conversion,[],[f8362]) ).
cnf(s469,plain,
( ~ spl34_5
| spl34_9
| spl34_55 ),
inference(rat,[],[s44,s58]) ).
cnf(s470,plain,
( ~ spl34_5
| spl34_9
| ~ spl34_51
| spl34_54 ),
inference(rat,[],[s43,s58]) ).
cnf(s472,plain,
spl34_29,
inference(rat,[],[s40,s38]) ).
cnf(s485,plain,
spl34_35,
inference(rat,[],[s25,s472]) ).
cnf(s491,plain,
spl34_55,
inference(rat,[],[s469,s38,s7]) ).
cnf(s495,plain,
spl34_3,
inference(rat,[],[s2,s3]) ).
cnf(s496,plain,
spl34_6,
inference(rat,[],[s116,s468,s145,s146,s91,s126,s3,s38,s7,s58,s495]) ).
cnf(s513,plain,
( ~ spl34_150
| ~ spl34_151
| spl34_1 ),
inference(rat,[],[s325,s292,s496,s58,s7,s495,s38,s3]) ).
cnf(s514,plain,
( ~ spl34_141
| spl34_1 ),
inference(rat,[],[s513,s139,s140,s496,s495,s38,s3]) ).
cnf(s515,plain,
spl34_1,
inference(rat,[],[s514,s144,s496,s3,s38,s495]) ).
cnf(s516,plain,
~ spl34_2,
inference(rat,[],[s1,s515]) ).
cnf(s517,plain,
spl34_51,
inference(rat,[],[s372,s62,s65,s70,s97,s38,s491]) ).
cnf(s518,plain,
spl34_84,
inference(rat,[],[s167,s38,s517]) ).
cnf(s521,plain,
spl34_54,
inference(rat,[],[s470,s7,s38,s517]) ).
cnf(s525,plain,
spl34_185,
inference(rat,[],[s213,s516,s485,s518]) ).
cnf(s527,plain,
spl34_83,
inference(rat,[],[s290,s516,s485,s518]) ).
cnf(s539,plain,
~ spl34_308,
inference(rat,[],[s393,s518,s516,s16,s485,s17,s19,s525]) ).
cnf(s543,plain,
spl34_205,
inference(rat,[],[s211,s525,s527]) ).
cnf(s544,plain,
spl34_204,
inference(rat,[],[s203,s525,s527]) ).
cnf(s551,plain,
spl34_188,
inference(rat,[],[s208,s525,s527]) ).
cnf(s558,plain,
~ spl34_257,
inference(rat,[],[s388,s521,s539,s543,s485,s544]) ).
cnf(s559,plain,
$false,
inference(rat,[],[s272,s518,s516,s485,s558,s551]) ).
fof(f8363,plain,
$false,
inference(avatar_sat_refutation,[],[s559]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU358+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n016.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 28 04:58:48 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 Running first-order theorem proving
% 0.22/0.48 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
% 17.73/3.59 % (3267114)Detected formulas, will run a generic FOF schedule.
% 17.73/3.59 % (3267131)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1723333219:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 17.73/3.59 % (3267133)dis-21_1_sil=8000:lcm=predicate:random_seed=539543177: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)
% 17.73/3.59 % (3267133)Instruction limit reached!
% 17.73/3.59 % (3267133)------------------------------
% 17.73/3.59 % (3267133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267133)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267133)Termination reason: Instruction limit
% 17.73/3.59 % (3267133)Termination phase: Saturation
% 17.73/3.59 % (3267133)Time elapsed: 0.066 s
% 17.73/3.59 % (3267133)Peak memory usage: 90 MB
% 17.73/3.59 % (3267133)Instructions burned: 132 (million)
% 17.73/3.59 % (3267129)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=3279440134:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 17.73/3.59 % (3267127)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=1481235958:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 17.73/3.59 % (3267128)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=2489563096:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 17.73/3.59 % (3267131)Instruction limit reached!
% 17.73/3.59 % (3267131)------------------------------
% 17.73/3.59 % (3267131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267132)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3872548921:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 17.73/3.59 % (3267131)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267131)Termination reason: Instruction limit
% 17.73/3.59 % (3267131)Termination phase: Saturation
% 17.73/3.59 % (3267131)Time elapsed: 0.073 s
% 17.73/3.59 % (3267131)Peak memory usage: 88 MB
% 17.73/3.59 % (3267131)Instructions burned: 119 (million)
% 17.73/3.59 % (3267130)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=47632696:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 17.73/3.59 % (3267130)Refutation not found, incomplete strategy
% 17.73/3.59 % (3267130)------------------------------
% 17.73/3.59 % (3267130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267130)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267130)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.59 % (3267130)Time elapsed: 0.003 s
% 17.73/3.59 % (3267130)Peak memory usage: 88 MB
% 17.73/3.59 % (3267130)Instructions burned: 2 (million)
% 17.73/3.59 % (3267144)lrs+10_1_sil=32000:urr=on:br=off:random_seed=172166972:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.73/3.59 % (3267144)Refutation not found, incomplete strategy
% 17.73/3.59 % (3267144)------------------------------
% 17.73/3.59 % (3267144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267144)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267144)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.59 % (3267144)Time elapsed: 0.004 s
% 17.73/3.59 % (3267144)Peak memory usage: 89 MB
% 17.73/3.59 % (3267144)Instructions burned: 4 (million)
% 17.73/3.59 % (3267132)Instruction limit reached!
% 17.73/3.59 % (3267132)------------------------------
% 17.73/3.59 % (3267132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267132)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267132)Termination reason: Instruction limit
% 17.73/3.59 % (3267132)Termination phase: Saturation
% 17.73/3.59 % (3267132)Time elapsed: 0.154 s
% 17.73/3.59 % (3267132)Peak memory usage: 90 MB
% 17.73/3.59 % (3267132)Instructions burned: 140 (million)
% 17.73/3.59 % (3267142)lrs+10_1_sil=8000:sp=occurrence:random_seed=1142458998:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 17.73/3.59 % (3267142)Instruction limit reached!
% 17.73/3.59 % (3267142)------------------------------
% 17.73/3.59 % (3267142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267142)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267142)Termination reason: Instruction limit
% 17.73/3.59 % (3267142)Termination phase: Saturation
% 17.73/3.59 % (3267142)Time elapsed: 0.155 s
% 17.73/3.59 % (3267142)Peak memory usage: 92 MB
% 17.73/3.59 % (3267142)Instructions burned: 286 (million)
% 17.73/3.59 % (3267146)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1099725814:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 17.73/3.59 % (3267130)------------------------------
% 17.73/3.59 % (3267130)------------------------------
% 17.73/3.59 % (3267144)------------------------------
% 17.73/3.59 % (3267144)------------------------------
% 17.73/3.59 % (3267148)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=1187777437:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 17.73/3.59 % (3267150)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3766028868:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 17.73/3.59 % (3267150)Refutation not found, incomplete strategy
% 17.73/3.59 % (3267150)------------------------------
% 17.73/3.59 % (3267150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267150)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267150)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.59 % (3267150)Time elapsed: 0.004 s
% 17.73/3.59 % (3267150)Peak memory usage: 89 MB
% 17.73/3.59 % (3267150)Instructions burned: 6 (million)
% 17.73/3.59 % (3267154)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1271087583:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 17.73/3.59 % (3267146)Instruction limit reached!
% 17.73/3.59 % (3267146)------------------------------
% 17.73/3.59 % (3267146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267146)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267146)Termination reason: Instruction limit
% 17.73/3.59 % (3267146)Termination phase: Saturation
% 17.73/3.59 % (3267146)Time elapsed: 0.329 s
% 17.73/3.59 % (3267146)Peak memory usage: 90 MB
% 17.73/3.59 % (3267146)Instructions burned: 325 (million)
% 17.73/3.59 % (3267148)Instruction limit reached!
% 17.73/3.59 % (3267148)------------------------------
% 17.73/3.59 % (3267148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267148)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267148)Termination reason: Instruction limit
% 17.73/3.59 % (3267148)Termination phase: Saturation
% 17.73/3.59 % (3267148)Time elapsed: 0.247 s
% 17.73/3.59 % (3267148)Peak memory usage: 91 MB
% 17.73/3.59 % (3267148)Instructions burned: 248 (million)
% 17.73/3.59 % (3267150)------------------------------
% 17.73/3.59 % (3267150)------------------------------
% 17.73/3.59 % (3267157)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1268503551:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 17.73/3.59 % (3267157)Instruction limit reached!
% 17.73/3.59 % (3267157)------------------------------
% 17.73/3.59 % (3267157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267157)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267157)Termination reason: Instruction limit
% 17.73/3.59 % (3267157)Termination phase: Saturation
% 17.73/3.59 % (3267157)Time elapsed: 0.061 s
% 17.73/3.59 % (3267157)Peak memory usage: 91 MB
% 17.73/3.59 % (3267157)Instructions burned: 114 (million)
% 17.73/3.59 % (3267158)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1247882678:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.73/3.59 % (3267159)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3903360578:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 17.73/3.59 % (3267158)Instruction limit reached!
% 17.73/3.59 % (3267158)------------------------------
% 17.73/3.59 % (3267158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267158)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267158)Termination reason: Instruction limit
% 17.73/3.59 % (3267158)Termination phase: Saturation
% 17.73/3.59 % (3267158)Time elapsed: 0.113 s
% 17.73/3.59 % (3267158)Peak memory usage: 89 MB
% 17.73/3.59 % (3267158)Instructions burned: 127 (million)
% 17.73/3.59 % (3267161)lrs+10_1_sil=8000:sp=occurrence:random_seed=3012390111:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 17.73/3.59 % (3267159)Instruction limit reached!
% 17.73/3.59 % (3267159)------------------------------
% 17.73/3.59 % (3267159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267159)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267159)Termination reason: Instruction limit
% 17.73/3.59 % (3267159)Termination phase: Saturation
% 17.73/3.59 % (3267159)Time elapsed: 0.104 s
% 17.73/3.59 % (3267159)Peak memory usage: 89 MB
% 17.73/3.59 % (3267159)Instructions burned: 115 (million)
% 17.73/3.59 % (3267167)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=927131349:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 17.73/3.59 % (3267167)Refutation not found, incomplete strategy
% 17.73/3.59 % (3267167)------------------------------
% 17.73/3.59 % (3267167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267167)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267167)Termination reason: Refutation not found, incomplete strategy
% 17.73/3.59 % (3267167)Time elapsed: 0.010 s
% 17.73/3.59 % (3267167)Peak memory usage: 88 MB
% 17.73/3.59 % (3267167)Instructions burned: 8 (million)
% 17.73/3.59 % (3267168)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1688551264:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 17.73/3.59 % (3267161)Instruction limit reached!
% 17.73/3.59 % (3267161)------------------------------
% 17.73/3.59 % (3267161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267161)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267161)Termination reason: Instruction limit
% 17.73/3.59 % (3267161)Termination phase: Saturation
% 17.73/3.59 % (3267161)Time elapsed: 0.448 s
% 17.73/3.59 % (3267161)Peak memory usage: 99 MB
% 17.73/3.59 % (3267161)Instructions burned: 908 (million)
% 17.73/3.59 % (3267171)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3360350475:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 17.73/3.59 % (3267167)------------------------------
% 17.73/3.59 % (3267167)------------------------------
% 17.73/3.59 % (3267171)Instruction limit reached!
% 17.73/3.59 % (3267171)------------------------------
% 17.73/3.59 % (3267171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.73/3.59 % (3267171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.73/3.59 % (3267171)CaDiCaL version: 2.1.3
% 17.73/3.59 % (3267171)Termination reason: Instruction limit
% 17.73/3.59 % (3267171)Termination phase: Saturation
% 17.73/3.59 % (3267171)Time elapsed: 0.095 s
% 17.73/3.59 % (3267171)Peak memory usage: 91 MB
% 17.73/3.59 % (3267171)Instructions burned: 135 (million)
% 17.73/3.59 % (3267127)First to succeed.
% 17.73/3.59 % (3267173)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2645766683:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 17.73/3.59 % (3267127)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3267114"
% 17.73/3.59 % (3267174)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2194933751:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 17.73/3.59 % (3267154)Also succeeded, but the first one will report.
% 17.73/3.59 % (3267127)Refutation found. Thanks to Tanya!
% 17.73/3.59 % SZS status Theorem for theBenchmark
% 17.73/3.59 % SZS output start Proof for theBenchmark
% See solution above
% 18.98/3.73 % (3267127)------------------------------
% 18.98/3.73 % (3267127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/3.73 % (3267127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/3.73 % (3267127)CaDiCaL version: 2.1.3
% 18.98/3.73 % (3267127)Termination reason: Refutation
% 18.98/3.73 % (3267127)Time elapsed: 1.949 s
% 18.98/3.73 % (3267127)Peak memory usage: 137 MB
% 18.98/3.73 % (3267127)Instructions burned: 1760 (million)
% 18.98/3.73 % (3267127)------------------------------
% 18.98/3.73 % (3267127)------------------------------
% 18.98/3.73 % (3267114)Success in time 2.597 s
% 18.98/3.73 % Vampire exiting
%------------------------------------------------------------------------------