%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU349+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:28 PM UTC 2026
% Result : Theorem 5.83s 2.30s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 39
% Syntax : Number of formulae : 370 ( 39 unt; 24 def)
% Number of atoms : 1526 ( 33 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 2008 ( 852 ~; 969 |; 118 &)
% ( 38 <=>; 29 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 22 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 256 ( 0 sgn 240 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f59,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
=> below(X0,X3,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d17_lattice3) ).
fof(f97,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/sandbox/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f106,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/sandbox/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f142,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( relstr_set_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X1)
=> related(X0,X3,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_lattice3) ).
fof(f178,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/sandbox/benchmark/theBenchmark.p',dt_k3_lattice3) ).
fof(f184,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/sandbox/benchmark/theBenchmark.p',dt_k4_lattice3) ).
fof(f191,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/sandbox/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f209,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f291,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/sandbox/benchmark/theBenchmark.p',fc4_lattice3) ).
fof(f389,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/sandbox/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f390,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/sandbox/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f453,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f532,conjecture,
! [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/sandbox/benchmark/theBenchmark.p',t30_lattice3) ).
fof(f533,negated_conjecture,
~ ! [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)) ) ) ),
inference(negated_conjecture,[status(cth)],[f532]) ).
fof(f620,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/sandbox/benchmark/theBenchmark.p',t7_lattice3) ).
fof(f717,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f718,plain,
! [X0] :
( ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f717]) ).
fof(f770,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f59]) ).
fof(f771,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_element_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f770]) ).
fof(f813,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,[],[f97]) ).
fof(f814,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,[],[f813]) ).
fof(f824,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,[],[f106]) ).
fof(f825,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,[],[f824]) ).
fof(f864,plain,
! [X0] :
( ! [X1,X2] :
( ( relstr_set_smaller(X0,X1,X2)
<=> ! [X3] :
( related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f142]) ).
fof(f865,plain,
! [X0] :
( ! [X1,X2] :
( ( relstr_set_smaller(X0,X1,X2)
<=> ! [X3] :
( related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f864]) ).
fof(f890,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,[],[f178]) ).
fof(f891,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,[],[f890]) ).
fof(f895,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,[],[f184]) ).
fof(f896,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,[],[f895]) ).
fof(f903,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,[],[f191]) ).
fof(f904,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,[],[f903]) ).
fof(f926,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f209]) ).
fof(f1004,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,[],[f291]) ).
fof(f1005,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,[],[f1004]) ).
fof(f1099,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,[],[f389]) ).
fof(f1100,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,[],[f1099]) ).
fof(f1101,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,[],[f390]) ).
fof(f1102,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,[],[f1101]) ).
fof(f1203,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f453]) ).
fof(f1314,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,[],[f533]) ).
fof(f1315,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,[],[f1314]) ).
fof(f1423,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,[],[f620]) ).
fof(f1424,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,[],[f1423]) ).
fof(f1576,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X3,X1)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( below(X0,X3,X1)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f771]) ).
fof(f1577,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X3,X1)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X4,X1)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f1576]) ).
fof(f1578,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_element_smaller(X0,X1,X2)
| ( ~ below(X0,sK78(X0,X1,X2),X1)
& in(sK78(X0,X1,X2),X2)
& element(sK78(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X4,X1)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_element_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78]),skolemize(X3,sK78(X0,X1,X2))],[f1577]) ).
fof(f1758,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& in(X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) )
| ~ relstr_set_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f865]) ).
fof(f1759,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X3,X2)
& in(X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( related(X0,X4,X2)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0)) )
| ~ relstr_set_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(rectify,[],[f1758]) ).
fof(f1760,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_set_smaller(X0,X1,X2)
| ( ~ related(X0,sK167(X0,X1,X2),X2)
& in(sK167(X0,X1,X2),X1)
& element(sK167(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( related(X0,X4,X2)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0)) )
| ~ relstr_set_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK167]),skolemize(X3,sK167(X0,X1,X2))],[f1759]) ).
fof(f1837,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,[],[f1100]) ).
fof(f1838,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,[],[f1102]) ).
fof(f2123,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0) )
& ( 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,[],[f1315]) ).
fof(f2124,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0) )
& ( 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(flattening,[],[f2123]) ).
fof(f2125,plain,
( ( ~ relstr_set_smaller(poset_of_lattice(sK481),sK480,cast_to_el_of_LattPOSet(sK481,sK482))
| ~ latt_element_smaller(sK481,sK482,sK480) )
& ( relstr_set_smaller(poset_of_lattice(sK481),sK480,cast_to_el_of_LattPOSet(sK481,sK482))
| latt_element_smaller(sK481,sK482,sK480) )
& element(sK482,the_carrier(sK481))
& ~ empty_carrier(sK481)
& lattice(sK481)
& latt_str(sK481) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK480,sK481,sK482]),skolemize(X0,sK480),skolemize(X1,sK481),skolemize(X2,sK482)],[f2124]) ).
fof(f2175,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,[],[f1424]) ).
fof(f2211,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| join_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f718]) ).
fof(f2212,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f718]) ).
fof(f2214,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_commutative(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f718]) ).
fof(f2338,plain,
! [X2,X0,X1,X4] :
( ~ latt_element_smaller(X0,X1,X2)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0))
| below(X0,X4,X1)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1578]) ).
fof(f2339,plain,
! [X2,X0,X1] :
( element(sK78(X0,X1,X2),the_carrier(X0))
| latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1578]) ).
fof(f2340,plain,
! [X2,X0,X1] :
( in(sK78(X0,X1,X2),X2)
| latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1578]) ).
fof(f2341,plain,
! [X2,X0,X1] :
( ~ below(X0,sK78(X0,X1,X2),X1)
| latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1578]) ).
fof(f2497,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,[],[f814]) ).
fof(f2528,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,[],[f825]) ).
fof(f2667,plain,
! [X2,X0,X1,X4] :
( ~ relstr_set_smaller(X0,X1,X2)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0))
| related(X0,X4,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1760]) ).
fof(f2668,plain,
! [X2,X0,X1] :
( element(sK167(X0,X1,X2),the_carrier(X0))
| relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1760]) ).
fof(f2669,plain,
! [X2,X0,X1] :
( in(sK167(X0,X1,X2),X1)
| relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1760]) ).
fof(f2670,plain,
! [X2,X0,X1] :
( ~ related(X0,sK167(X0,X1,X2),X2)
| relstr_set_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1760]) ).
fof(f2699,plain,
! [X0] :
( rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f891]) ).
fof(f2706,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,[],[f896]) ).
fof(f2711,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,[],[f904]) ).
fof(f2728,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f926]) ).
fof(f2905,plain,
! [X0] :
( reflexive_relstr(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1005]) ).
fof(f2907,plain,
! [X0] :
( ~ empty_carrier(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1005]) ).
fof(f3137,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,[],[f1837]) ).
fof(f3138,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,[],[f1837]) ).
fof(f3139,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,[],[f1838]) ).
fof(f3140,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,[],[f1838]) ).
fof(f3646,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f1203]) ).
fof(f3770,plain,
latt_str(sK481),
inference(cnf_transformation,[],[f2125]) ).
fof(f3771,plain,
lattice(sK481),
inference(cnf_transformation,[],[f2125]) ).
fof(f3772,plain,
~ empty_carrier(sK481),
inference(cnf_transformation,[],[f2125]) ).
fof(f3773,plain,
element(sK482,the_carrier(sK481)),
inference(cnf_transformation,[],[f2125]) ).
fof(f3774,plain,
( relstr_set_smaller(poset_of_lattice(sK481),sK480,cast_to_el_of_LattPOSet(sK481,sK482))
| latt_element_smaller(sK481,sK482,sK480) ),
inference(cnf_transformation,[],[f2125]) ).
fof(f3775,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK481),sK480,cast_to_el_of_LattPOSet(sK481,sK482))
| ~ latt_element_smaller(sK481,sK482,sK480) ),
inference(cnf_transformation,[],[f2125]) ).
fof(f3933,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,[],[f2175]) ).
fof(f3934,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,[],[f2175]) ).
fof(f4615,definition,
sF501 = poset_of_lattice(sK481),
introduced(definition,[new_symbols(definition,[sF501])],[function_definition]) ).
fof(f4616,plain,
poset_of_lattice(sK481) = sF501,
inference(reorient_equations,[],[f4615]) ).
fof(f4617,definition,
sF502 = cast_to_el_of_LattPOSet(sK481,sK482),
introduced(definition,[new_symbols(definition,[sF502])],[function_definition]) ).
fof(f4618,plain,
cast_to_el_of_LattPOSet(sK481,sK482) = sF502,
inference(reorient_equations,[],[f4617]) ).
fof(f4619,plain,
( ~ relstr_set_smaller(sF501,sK480,sF502)
| ~ latt_element_smaller(sK481,sK482,sK480) ),
inference(definition_folding,[],[f3775,f4618,f4616]) ).
fof(f4620,plain,
( relstr_set_smaller(sF501,sK480,sF502)
| latt_element_smaller(sK481,sK482,sK480) ),
inference(definition_folding,[],[f3774,f4618,f4616]) ).
fof(f4621,definition,
sF503 = the_carrier(sK481),
introduced(definition,[new_symbols(definition,[sF503])],[function_definition]) ).
fof(f4622,plain,
the_carrier(sK481) = sF503,
inference(reorient_equations,[],[f4621]) ).
fof(f4623,plain,
element(sK482,sF503),
inference(definition_folding,[],[f3773,f4622]) ).
fof(f4660,definition,
( spl504_5
<=> latt_element_smaller(sK481,sK482,sK480) ),
introduced(definition,[new_symbols(definition,[spl504_5])],[avatar_definition]) ).
fof(f4661,plain,
( ~ latt_element_smaller(sK481,sK482,sK480)
| spl504_5 ),
inference(avatar_component_clause,[],[f4660]) ).
fof(f4662,plain,
( latt_element_smaller(sK481,sK482,sK480)
| ~ spl504_5 ),
inference(avatar_component_clause,[],[f4660]) ).
fof(f4664,definition,
( spl504_6
<=> relstr_set_smaller(sF501,sK480,sF502) ),
introduced(definition,[new_symbols(definition,[spl504_6])],[avatar_definition]) ).
fof(f4665,plain,
( ~ relstr_set_smaller(sF501,sK480,sF502)
| spl504_6 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4666,plain,
( relstr_set_smaller(sF501,sK480,sF502)
| ~ spl504_6 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4667,plain,
( spl504_5
| spl504_6 ),
inference(avatar_split_clause,[],[f4620,f4664,f4660]) ).
fof(f4668,plain,
( ~ spl504_5
| ~ spl504_6 ),
inference(avatar_split_clause,[],[f4619,f4664,f4660]) ).
fof(f4974,plain,
( element(sF502,the_carrier(poset_of_lattice(sK481)))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(sK481)) ),
inference(superposition,[],[f2706,f4618]) ).
fof(f4977,plain,
( element(sF502,the_carrier(poset_of_lattice(sK481)))
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(sK481)) ),
inference(forward_subsumption_resolution,[],[f4974,f3772]) ).
fof(f4979,plain,
( element(sF502,the_carrier(poset_of_lattice(sK481)))
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(sK481)) ),
inference(forward_subsumption_resolution,[],[f4977,f3771]) ).
fof(f4981,plain,
( element(sF502,the_carrier(poset_of_lattice(sK481)))
| ~ element(sK482,the_carrier(sK481)) ),
inference(forward_subsumption_resolution,[],[f4979,f3770]) ).
fof(f4983,plain,
( element(sF502,the_carrier(sF501))
| ~ element(sK482,the_carrier(sK481)) ),
inference(forward_demodulation,[],[f4981,f4616]) ).
fof(f4984,plain,
( ~ element(sK482,sF503)
| element(sF502,the_carrier(sF501)) ),
inference(forward_demodulation,[],[f4983,f4622]) ).
fof(f4985,plain,
element(sF502,the_carrier(sF501)),
inference(forward_subsumption_resolution,[],[f4984,f4623]) ).
fof(f4988,plain,
! [X0] :
( ~ element(X0,sF503)
| cast_to_el_of_LattPOSet(sK481,X0) = X0
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2497,f4622]) ).
fof(f4989,plain,
! [X0] :
( ~ element(X0,sF503)
| cast_to_el_of_LattPOSet(sK481,X0) = X0
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f4988,f3772]) ).
fof(f4999,definition,
( spl504_63
<=> empty_carrier(sF501) ),
introduced(definition,[new_symbols(definition,[spl504_63])],[avatar_definition]) ).
fof(f5000,plain,
( ~ empty_carrier(sF501)
| spl504_63 ),
inference(avatar_component_clause,[],[f4999]) ).
fof(f5008,plain,
! [X0] :
( ~ element(X0,sF503)
| cast_to_el_of_LattPOSet(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f4989,f3771]) ).
fof(f5009,plain,
! [X0] :
( ~ element(X0,sF503)
| cast_to_el_of_LattPOSet(sK481,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f5008,f3770]) ).
fof(f5010,plain,
sK482 = cast_to_el_of_LattPOSet(sK481,sK482),
inference(resolution,[],[f5009,f4623]) ).
fof(f5011,plain,
sK482 = sF502,
inference(forward_demodulation,[],[f5010,f4618]) ).
fof(f5012,plain,
element(sK482,the_carrier(sF501)),
inference(superposition,[],[f4985,f5011]) ).
fof(f5013,plain,
( ~ relstr_set_smaller(sF501,sK480,sK482)
| spl504_6 ),
inference(superposition,[],[f4665,f5011]) ).
fof(f5016,plain,
! [X0] :
( ~ element(X0,the_carrier(sF501))
| cast_to_el_of_lattice(sK481,X0) = X0
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2528,f4616]) ).
fof(f5018,plain,
! [X0] :
( ~ element(X0,the_carrier(sF501))
| cast_to_el_of_lattice(sK481,X0) = X0
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5016,f3772]) ).
fof(f5019,plain,
! [X0] :
( ~ element(X0,the_carrier(sF501))
| cast_to_el_of_lattice(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5018,f3771]) ).
fof(f5020,plain,
! [X0] :
( ~ element(X0,the_carrier(sF501))
| cast_to_el_of_lattice(sK481,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f5019,f3770]) ).
fof(f5030,plain,
! [X0,X1] :
( element(sK78(sK481,X0,X1),sF503)
| latt_element_smaller(sK481,X0,X1)
| ~ element(X0,sF503)
| empty_carrier(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2339,f4622]) ).
fof(f5032,plain,
! [X0,X1] :
( element(sK78(sK481,X0,X1),sF503)
| latt_element_smaller(sK481,X0,X1)
| ~ element(X0,sF503)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5030,f3772]) ).
fof(f5034,plain,
! [X0,X1] :
( element(sK78(sK481,X0,X1),sF503)
| latt_element_smaller(sK481,X0,X1)
| ~ element(X0,sF503) ),
inference(forward_subsumption_resolution,[],[f5032,f3770]) ).
fof(f5035,plain,
! [X0,X1] :
( latt_element_smaller(sK481,X0,X1)
| ~ element(X0,sF503)
| sK78(sK481,X0,X1) = cast_to_el_of_LattPOSet(sK481,sK78(sK481,X0,X1)) ),
inference(resolution,[],[f5034,f5009]) ).
fof(f5036,plain,
( ~ empty_carrier(sF501)
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2907,f4616]) ).
fof(f5037,plain,
( ~ empty_carrier(sF501)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5036,f3772]) ).
fof(f5038,plain,
( ~ empty_carrier(sF501)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5037,f3771]) ).
fof(f5039,plain,
~ empty_carrier(sF501),
inference(forward_subsumption_resolution,[],[f5038,f3770]) ).
fof(f5040,plain,
~ spl504_63,
inference(avatar_split_clause,[],[f5039,f4999]) ).
fof(f5041,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sK481))
| below(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ latt_str(sK481) )
| ~ spl504_5 ),
inference(resolution,[],[f2338,f4662]) ).
fof(f5042,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sK481))
| below(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ latt_str(sK481) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5041,f3772]) ).
fof(f5043,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sK481))
| below(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481)) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5042,f3770]) ).
fof(f5044,plain,
( ! [X0] :
( ~ element(X0,sF503)
| ~ in(X0,sK480)
| below(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481)) )
| ~ spl504_5 ),
inference(forward_demodulation,[],[f5043,f4622]) ).
fof(f5045,plain,
( ! [X0] :
( ~ element(sK482,sF503)
| ~ element(X0,sF503)
| ~ in(X0,sK480)
| below(sK481,X0,sK482) )
| ~ spl504_5 ),
inference(forward_demodulation,[],[f5044,f4622]) ).
fof(f5046,plain,
( ! [X0] :
( below(sK481,X0,sK482)
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5045,f4623]) ).
fof(f5111,definition,
( spl504_67
<=> rel_str(sF501) ),
introduced(definition,[new_symbols(definition,[spl504_67])],[avatar_definition]) ).
fof(f5112,plain,
( rel_str(sF501)
| ~ spl504_67 ),
inference(avatar_component_clause,[],[f5111]) ).
fof(f5113,plain,
( ~ rel_str(sF501)
| spl504_67 ),
inference(avatar_component_clause,[],[f5111]) ).
fof(f5207,plain,
( reflexive_relstr(sF501)
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2905,f4616]) ).
fof(f5208,plain,
( reflexive_relstr(sF501)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5207,f3772]) ).
fof(f5209,plain,
( reflexive_relstr(sF501)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5208,f3771]) ).
fof(f5210,plain,
reflexive_relstr(sF501),
inference(forward_subsumption_resolution,[],[f5209,f3770]) ).
fof(f5215,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK481),cast_to_el_of_LattPOSet(sK481,X0),sF502)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f3933,f4618]) ).
fof(f5217,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK481),cast_to_el_of_LattPOSet(sK481,X0),sF502)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481))
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5215,f3772]) ).
fof(f5221,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK481),cast_to_el_of_LattPOSet(sK481,X0),sF502)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481))
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5217,f3771]) ).
fof(f5225,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK481),cast_to_el_of_LattPOSet(sK481,X0),sF502)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481)) ),
inference(forward_subsumption_resolution,[],[f5221,f3770]) ).
fof(f5229,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK481),cast_to_el_of_LattPOSet(sK481,X0),sK482)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481)) ),
inference(forward_demodulation,[],[f5225,f5011]) ).
fof(f5233,plain,
! [X0] :
( related_reflexive(sF501,cast_to_el_of_LattPOSet(sK481,X0),sK482)
| ~ below_refl(sK481,X0,sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ element(X0,the_carrier(sK481)) ),
inference(forward_demodulation,[],[f5229,f4616]) ).
fof(f5237,plain,
! [X0] :
( ~ element(sK482,sF503)
| related_reflexive(sF501,cast_to_el_of_LattPOSet(sK481,X0),sK482)
| ~ below_refl(sK481,X0,sK482)
| ~ element(X0,the_carrier(sK481)) ),
inference(forward_demodulation,[],[f5233,f4622]) ).
fof(f5239,plain,
! [X0] :
( related_reflexive(sF501,cast_to_el_of_LattPOSet(sK481,X0),sK482)
| ~ below_refl(sK481,X0,sK482)
| ~ element(X0,the_carrier(sK481)) ),
inference(forward_subsumption_resolution,[],[f5237,f4623]) ).
fof(f5241,plain,
! [X0] :
( related_reflexive(sF501,cast_to_el_of_LattPOSet(sK481,X0),sK482)
| ~ element(X0,sF503)
| ~ below_refl(sK481,X0,sK482) ),
inference(forward_demodulation,[],[f5239,f4622]) ).
fof(f5264,plain,
( rel_str(sF501)
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) ),
inference(superposition,[],[f2699,f4616]) ).
fof(f5265,plain,
( empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481)
| spl504_67 ),
inference(forward_subsumption_resolution,[],[f5264,f5113]) ).
fof(f5266,plain,
( ~ lattice(sK481)
| ~ latt_str(sK481)
| spl504_67 ),
inference(forward_subsumption_resolution,[],[f5265,f3772]) ).
fof(f5267,plain,
( ~ latt_str(sK481)
| spl504_67 ),
inference(forward_subsumption_resolution,[],[f5266,f3771]) ).
fof(f5268,plain,
( $false
| spl504_67 ),
inference(forward_subsumption_resolution,[],[f5267,f3770]) ).
fof(f5269,plain,
spl504_67,
inference(avatar_contradiction_clause,[],[f5268]) ).
fof(f5305,plain,
( ! [X0] :
( below_refl(sK481,X0,sK482)
| empty_carrier(sK481)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_5 ),
inference(resolution,[],[f3138,f5046]) ).
fof(f5306,plain,
( ! [X0] :
( below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5305,f3772]) ).
fof(f5307,plain,
( ! [X0] :
( below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5306,f3770]) ).
fof(f5308,plain,
( ! [X0] :
( ~ element(X0,sF503)
| below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ element(sK482,the_carrier(sK481))
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_5 ),
inference(forward_demodulation,[],[f5307,f4622]) ).
fof(f5309,plain,
( ! [X0] :
( ~ element(X0,sF503)
| below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ element(sK482,the_carrier(sK481))
| ~ in(X0,sK480) )
| ~ spl504_5 ),
inference(duplicate_literal_removal,[],[f5308]) ).
fof(f5310,plain,
( ! [X0] :
( ~ element(sK482,sF503)
| ~ element(X0,sF503)
| below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ in(X0,sK480) )
| ~ spl504_5 ),
inference(forward_demodulation,[],[f5309,f4622]) ).
fof(f5311,plain,
( ! [X0] :
( ~ element(X0,sF503)
| below_refl(sK481,X0,sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ in(X0,sK480) )
| ~ spl504_5 ),
inference(forward_subsumption_resolution,[],[f5310,f4623]) ).
fof(f5313,definition,
( spl504_73
<=> join_absorbing(sK481) ),
introduced(definition,[new_symbols(definition,[spl504_73])],[avatar_definition]) ).
fof(f5314,plain,
( join_absorbing(sK481)
| ~ spl504_73 ),
inference(avatar_component_clause,[],[f5313]) ).
fof(f5315,plain,
( ~ join_absorbing(sK481)
| spl504_73 ),
inference(avatar_component_clause,[],[f5313]) ).
fof(f5317,definition,
( spl504_74
<=> meet_absorbing(sK481) ),
introduced(definition,[new_symbols(definition,[spl504_74])],[avatar_definition]) ).
fof(f5318,plain,
( meet_absorbing(sK481)
| ~ spl504_74 ),
inference(avatar_component_clause,[],[f5317]) ).
fof(f5319,plain,
( ~ meet_absorbing(sK481)
| spl504_74 ),
inference(avatar_component_clause,[],[f5317]) ).
fof(f5321,definition,
( spl504_75
<=> meet_commutative(sK481) ),
introduced(definition,[new_symbols(definition,[spl504_75])],[avatar_definition]) ).
fof(f5322,plain,
( meet_commutative(sK481)
| ~ spl504_75 ),
inference(avatar_component_clause,[],[f5321]) ).
fof(f5325,definition,
( spl504_76
<=> ! [X0] :
( ~ element(X0,sF503)
| ~ in(X0,sK480)
| below_refl(sK481,X0,sK482) ) ),
introduced(definition,[new_symbols(definition,[spl504_76])],[avatar_definition]) ).
fof(f5326,plain,
( ! [X0] :
( below_refl(sK481,X0,sK482)
| ~ in(X0,sK480)
| ~ element(X0,sF503) )
| ~ spl504_76 ),
inference(avatar_component_clause,[],[f5325]) ).
fof(f5327,plain,
( ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| spl504_76
| ~ spl504_5 ),
inference(avatar_split_clause,[],[f5311,f4660,f5325,f5321,f5317,f5313]) ).
fof(f5349,definition,
( spl504_77
<=> element(sK167(sF501,sK480,sK482),the_carrier(sF501)) ),
introduced(definition,[new_symbols(definition,[spl504_77])],[avatar_definition]) ).
fof(f5350,plain,
( element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ spl504_77 ),
inference(avatar_component_clause,[],[f5349]) ).
fof(f5351,plain,
( ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| spl504_77 ),
inference(avatar_component_clause,[],[f5349]) ).
fof(f5353,definition,
( spl504_78
<=> element(sK167(sF501,sK480,sK482),sF503) ),
introduced(definition,[new_symbols(definition,[spl504_78])],[avatar_definition]) ).
fof(f5354,plain,
( ~ element(sK167(sF501,sK480,sK482),sF503)
| spl504_78 ),
inference(avatar_component_clause,[],[f5353]) ).
fof(f5355,plain,
( element(sK167(sF501,sK480,sK482),sF503)
| ~ spl504_78 ),
inference(avatar_component_clause,[],[f5353]) ).
fof(f5370,plain,
( relstr_set_smaller(sF501,sK480,sK482)
| ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| spl504_77 ),
inference(resolution,[],[f5351,f2668]) ).
fof(f5371,plain,
( ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| spl504_6
| spl504_77 ),
inference(forward_subsumption_resolution,[],[f5370,f5013]) ).
fof(f5372,plain,
( ~ rel_str(sF501)
| spl504_6
| spl504_77 ),
inference(forward_subsumption_resolution,[],[f5371,f5012]) ).
fof(f5373,plain,
( $false
| spl504_6
| ~ spl504_67
| spl504_77 ),
inference(forward_subsumption_resolution,[],[f5372,f5112]) ).
fof(f5374,plain,
( spl504_6
| ~ spl504_67
| spl504_77 ),
inference(avatar_contradiction_clause,[],[f5373]) ).
fof(f5376,plain,
( sK167(sF501,sK480,sK482) = cast_to_el_of_lattice(sK481,sK167(sF501,sK480,sK482))
| ~ spl504_77 ),
inference(resolution,[],[f5350,f5020]) ).
fof(f5380,plain,
( sK167(sF501,sK480,sK482) = cast_to_el_of_LattPOSet(sK481,sK167(sF501,sK480,sK482))
| ~ spl504_78 ),
inference(resolution,[],[f5355,f5009]) ).
fof(f5391,plain,
( related_reflexive(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ element(sK167(sF501,sK480,sK482),sF503)
| ~ below_refl(sK481,sK167(sF501,sK480,sK482),sK482)
| ~ spl504_78 ),
inference(superposition,[],[f5241,f5380]) ).
fof(f5408,plain,
( related_reflexive(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ below_refl(sK481,sK167(sF501,sK480,sK482),sK482)
| ~ spl504_78 ),
inference(forward_subsumption_resolution,[],[f5391,f5355]) ).
fof(f5433,definition,
( spl504_82
<=> below_refl(sK481,sK167(sF501,sK480,sK482),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_82])],[avatar_definition]) ).
fof(f5435,plain,
( ~ below_refl(sK481,sK167(sF501,sK480,sK482),sK482)
| spl504_82 ),
inference(avatar_component_clause,[],[f5433]) ).
fof(f5437,definition,
( spl504_83
<=> related_reflexive(sF501,sK167(sF501,sK480,sK482),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_83])],[avatar_definition]) ).
fof(f5439,plain,
( related_reflexive(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ spl504_83 ),
inference(avatar_component_clause,[],[f5437]) ).
fof(f5440,plain,
( ~ spl504_82
| spl504_83
| ~ spl504_78 ),
inference(avatar_split_clause,[],[f5408,f5353,f5437,f5433]) ).
fof(f5712,plain,
( one_sorted_str(sF501)
| ~ spl504_67 ),
inference(resolution,[],[f2728,f5112]) ).
fof(f5713,plain,
( the_carrier(sF501) = cast_as_carrier_subset(sF501)
| ~ spl504_67 ),
inference(resolution,[],[f5712,f3646]) ).
fof(f5812,plain,
( empty_carrier(sK481)
| meet_commutative(sK481)
| ~ latt_str(sK481) ),
inference(resolution,[],[f2214,f3771]) ).
fof(f5813,plain,
( meet_commutative(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f5812,f3772]) ).
fof(f5814,plain,
meet_commutative(sK481),
inference(forward_subsumption_resolution,[],[f5813,f3770]) ).
fof(f5815,plain,
spl504_75,
inference(avatar_split_clause,[],[f5814,f5321]) ).
fof(f6035,plain,
( relstr_set_smaller(sF501,sK480,sK482)
| ~ spl504_6 ),
inference(forward_demodulation,[],[f4666,f5011]) ).
fof(f6041,plain,
( ~ element(sK482,sF503)
| sK78(sK481,sK482,sK480) = cast_to_el_of_LattPOSet(sK481,sK78(sK481,sK482,sK480))
| spl504_5 ),
inference(resolution,[],[f4661,f5035]) ).
fof(f6042,plain,
( sK78(sK481,sK482,sK480) = cast_to_el_of_LattPOSet(sK481,sK78(sK481,sK482,sK480))
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6041,f4623]) ).
fof(f6055,plain,
( element(sK78(sK481,sK482,sK480),the_carrier(poset_of_lattice(sK481)))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5 ),
inference(superposition,[],[f2706,f6042]) ).
fof(f6060,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK481),sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481) )
| spl504_5 ),
inference(superposition,[],[f3934,f6042]) ).
fof(f6067,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK481),sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ lattice(sK481)
| ~ latt_str(sK481) )
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6060,f3772]) ).
fof(f6072,plain,
( element(sK78(sK481,sK482,sK480),the_carrier(poset_of_lattice(sK481)))
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6055,f3772]) ).
fof(f6074,definition,
( spl504_95
<=> element(sK78(sK481,sK482,sK480),sF503) ),
introduced(definition,[new_symbols(definition,[spl504_95])],[avatar_definition]) ).
fof(f6075,plain,
( element(sK78(sK481,sK482,sK480),sF503)
| ~ spl504_95 ),
inference(avatar_component_clause,[],[f6074]) ).
fof(f6076,plain,
( ~ element(sK78(sK481,sK482,sK480),sF503)
| spl504_95 ),
inference(avatar_component_clause,[],[f6074]) ).
fof(f6078,definition,
( spl504_96
<=> element(sK78(sK481,sK482,sK480),cast_as_carrier_subset(sF501)) ),
introduced(definition,[new_symbols(definition,[spl504_96])],[avatar_definition]) ).
fof(f6080,plain,
( element(sK78(sK481,sK482,sK480),cast_as_carrier_subset(sF501))
| ~ spl504_96 ),
inference(avatar_component_clause,[],[f6078]) ).
fof(f6092,definition,
( spl504_99
<=> below_refl(sK481,sK78(sK481,sK482,sK480),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_99])],[avatar_definition]) ).
fof(f6093,plain,
( below_refl(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ spl504_99 ),
inference(avatar_component_clause,[],[f6092]) ).
fof(f6094,plain,
( ~ below_refl(sK481,sK78(sK481,sK482,sK480),sK482)
| spl504_99 ),
inference(avatar_component_clause,[],[f6092]) ).
fof(f6096,definition,
( spl504_100
<=> related_reflexive(sF501,sK78(sK481,sK482,sK480),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_100])],[avatar_definition]) ).
fof(f6097,plain,
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),sK482)
| spl504_100 ),
inference(avatar_component_clause,[],[f6096]) ).
fof(f6119,definition,
( spl504_105
<=> ! [X0] :
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,sF503) ) ),
introduced(definition,[new_symbols(definition,[spl504_105])],[avatar_definition]) ).
fof(f6120,plain,
( ! [X0] :
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,sF503) )
| ~ spl504_105 ),
inference(avatar_component_clause,[],[f6119]) ).
fof(f6130,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK481),sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ latt_str(sK481) )
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6067,f3771]) ).
fof(f6135,plain,
( element(sK78(sK481,sK482,sK480),the_carrier(poset_of_lattice(sK481)))
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6072,f3771]) ).
fof(f6140,plain,
( ! [X0] :
( ~ related_reflexive(poset_of_lattice(sK481),sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481)) )
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6130,f3770]) ).
fof(f6145,plain,
( element(sK78(sK481,sK482,sK480),the_carrier(poset_of_lattice(sK481)))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5 ),
inference(forward_subsumption_resolution,[],[f6135,f3770]) ).
fof(f6149,plain,
( ! [X0] :
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(X0,the_carrier(sK481))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481)) )
| spl504_5 ),
inference(forward_demodulation,[],[f6140,f4616]) ).
fof(f6154,plain,
( element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5 ),
inference(forward_demodulation,[],[f6145,f4616]) ).
fof(f6158,plain,
( ! [X0] :
( ~ element(X0,sF503)
| ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481)) )
| spl504_5 ),
inference(forward_demodulation,[],[f6149,f4622]) ).
fof(f6163,plain,
( element(sK78(sK481,sK482,sK480),cast_as_carrier_subset(sF501))
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| spl504_5
| ~ spl504_67 ),
inference(forward_demodulation,[],[f6154,f5713]) ).
fof(f6167,plain,
( ! [X0] :
( ~ element(sK78(sK481,sK482,sK480),sF503)
| ~ element(X0,sF503)
| ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),cast_to_el_of_LattPOSet(sK481,X0))
| below_refl(sK481,sK78(sK481,sK482,sK480),X0) )
| spl504_5 ),
inference(forward_demodulation,[],[f6158,f4622]) ).
fof(f6172,plain,
( ~ element(sK78(sK481,sK482,sK480),sF503)
| element(sK78(sK481,sK482,sK480),cast_as_carrier_subset(sF501))
| spl504_5
| ~ spl504_67 ),
inference(forward_demodulation,[],[f6163,f4622]) ).
fof(f6182,plain,
( spl504_105
| ~ spl504_95
| spl504_5 ),
inference(avatar_split_clause,[],[f6167,f4660,f6074,f6119]) ).
fof(f6185,plain,
( spl504_96
| ~ spl504_95
| spl504_5
| ~ spl504_67 ),
inference(avatar_split_clause,[],[f6172,f5111,f4660,f6074,f6078]) ).
fof(f6191,definition,
( spl504_109
<=> related(sF501,sK167(sF501,sK480,sK482),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_109])],[avatar_definition]) ).
fof(f6193,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ spl504_109 ),
inference(avatar_component_clause,[],[f6191]) ).
fof(f6195,definition,
( spl504_110
<=> in(sK167(sF501,sK480,sK482),sK480) ),
introduced(definition,[new_symbols(definition,[spl504_110])],[avatar_definition]) ).
fof(f6196,plain,
( in(sK167(sF501,sK480,sK482),sK480)
| ~ spl504_110 ),
inference(avatar_component_clause,[],[f6195]) ).
fof(f6197,plain,
( ~ in(sK167(sF501,sK480,sK482),sK480)
| spl504_110 ),
inference(avatar_component_clause,[],[f6195]) ).
fof(f6202,plain,
( element(sK167(sF501,sK480,sK482),the_carrier(sK481))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77 ),
inference(superposition,[],[f2711,f5376]) ).
fof(f6203,plain,
( element(sK167(sF501,sK480,sK482),the_carrier(sK481))
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77 ),
inference(forward_subsumption_resolution,[],[f6202,f3772]) ).
fof(f6206,plain,
( element(sK167(sF501,sK480,sK482),the_carrier(sK481))
| ~ latt_str(sK481)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77 ),
inference(forward_subsumption_resolution,[],[f6203,f3771]) ).
fof(f6209,plain,
( element(sK167(sF501,sK480,sK482),the_carrier(sK481))
| ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77 ),
inference(forward_subsumption_resolution,[],[f6206,f3770]) ).
fof(f6212,plain,
( element(sK167(sF501,sK480,sK482),sF503)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77 ),
inference(forward_demodulation,[],[f6209,f4622]) ).
fof(f6215,plain,
( relstr_set_smaller(sF501,sK480,sK482)
| ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| spl504_110 ),
inference(resolution,[],[f6197,f2669]) ).
fof(f6216,plain,
( latt_element_smaller(sK481,sK482,sK480)
| ~ element(sK482,sF503)
| spl504_95 ),
inference(resolution,[],[f6076,f5034]) ).
fof(f6217,plain,
( ~ element(sK482,sF503)
| spl504_5
| spl504_95 ),
inference(forward_subsumption_resolution,[],[f6216,f4661]) ).
fof(f6218,plain,
( $false
| spl504_5
| spl504_95 ),
inference(forward_subsumption_resolution,[],[f6217,f4623]) ).
fof(f6219,plain,
( spl504_5
| spl504_95 ),
inference(avatar_contradiction_clause,[],[f6218]) ).
fof(f6221,plain,
( ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| spl504_6
| spl504_110 ),
inference(forward_subsumption_resolution,[],[f6215,f5013]) ).
fof(f6222,plain,
( ~ rel_str(sF501)
| spl504_6
| spl504_110 ),
inference(forward_subsumption_resolution,[],[f6221,f5012]) ).
fof(f6223,plain,
( $false
| spl504_6
| ~ spl504_67
| spl504_110 ),
inference(forward_subsumption_resolution,[],[f6222,f5112]) ).
fof(f6224,plain,
( spl504_6
| ~ spl504_67
| spl504_110 ),
inference(avatar_contradiction_clause,[],[f6223]) ).
fof(f6226,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sF501))
| related(sF501,X0,sK482)
| ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501) )
| ~ spl504_6 ),
inference(resolution,[],[f6035,f2667]) ).
fof(f6227,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sF501))
| related(sF501,X0,sK482)
| ~ rel_str(sF501) )
| ~ spl504_6 ),
inference(forward_subsumption_resolution,[],[f6226,f5012]) ).
fof(f6228,plain,
( ! [X0] :
( ~ in(X0,sK480)
| ~ element(X0,the_carrier(sF501))
| related(sF501,X0,sK482) )
| ~ spl504_6
| ~ spl504_67 ),
inference(forward_subsumption_resolution,[],[f6227,f5112]) ).
fof(f6229,plain,
( ! [X0] :
( ~ element(X0,cast_as_carrier_subset(sF501))
| ~ in(X0,sK480)
| related(sF501,X0,sK482) )
| ~ spl504_6
| ~ spl504_67 ),
inference(forward_demodulation,[],[f6228,f5713]) ).
fof(f6317,plain,
( ~ in(sK78(sK481,sK482,sK480),sK480)
| related(sF501,sK78(sK481,sK482,sK480),sK482)
| ~ spl504_6
| ~ spl504_67
| ~ spl504_96 ),
inference(resolution,[],[f6229,f6080]) ).
fof(f6322,definition,
( spl504_111
<=> related(sF501,sK78(sK481,sK482,sK480),sK482) ),
introduced(definition,[new_symbols(definition,[spl504_111])],[avatar_definition]) ).
fof(f6324,plain,
( related(sF501,sK78(sK481,sK482,sK480),sK482)
| ~ spl504_111 ),
inference(avatar_component_clause,[],[f6322]) ).
fof(f6326,definition,
( spl504_112
<=> in(sK78(sK481,sK482,sK480),sK480) ),
introduced(definition,[new_symbols(definition,[spl504_112])],[avatar_definition]) ).
fof(f6328,plain,
( ~ in(sK78(sK481,sK482,sK480),sK480)
| spl504_112 ),
inference(avatar_component_clause,[],[f6326]) ).
fof(f6329,plain,
( spl504_111
| ~ spl504_112
| ~ spl504_6
| ~ spl504_67
| ~ spl504_96 ),
inference(avatar_split_clause,[],[f6317,f6078,f5111,f4664,f6326,f6322]) ).
fof(f6330,plain,
( latt_element_smaller(sK481,sK482,sK480)
| ~ element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ latt_str(sK481)
| spl504_112 ),
inference(resolution,[],[f6328,f2340]) ).
fof(f6331,plain,
( ~ element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ latt_str(sK481)
| spl504_5
| spl504_112 ),
inference(forward_subsumption_resolution,[],[f6330,f4661]) ).
fof(f6332,plain,
( ~ element(sK482,the_carrier(sK481))
| ~ latt_str(sK481)
| spl504_5
| spl504_112 ),
inference(forward_subsumption_resolution,[],[f6331,f3772]) ).
fof(f6333,plain,
( ~ element(sK482,the_carrier(sK481))
| spl504_5
| spl504_112 ),
inference(forward_subsumption_resolution,[],[f6332,f3770]) ).
fof(f6334,plain,
( ~ element(sK482,sF503)
| spl504_5
| spl504_112 ),
inference(forward_demodulation,[],[f6333,f4622]) ).
fof(f6335,plain,
( $false
| spl504_5
| spl504_112 ),
inference(forward_subsumption_resolution,[],[f6334,f4623]) ).
fof(f6336,plain,
( spl504_5
| spl504_112 ),
inference(avatar_contradiction_clause,[],[f6335]) ).
fof(f6501,plain,
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),sF502)
| below_refl(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ element(sK482,sF503)
| ~ spl504_105 ),
inference(superposition,[],[f6120,f4618]) ).
fof(f6506,plain,
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),sF502)
| ~ element(sK482,sF503)
| spl504_99
| ~ spl504_105 ),
inference(forward_subsumption_resolution,[],[f6501,f6094]) ).
fof(f6508,plain,
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),sF502)
| spl504_99
| ~ spl504_105 ),
inference(forward_subsumption_resolution,[],[f6506,f4623]) ).
fof(f6509,plain,
( ~ related_reflexive(sF501,sK78(sK481,sK482,sK480),sK482)
| spl504_99
| ~ spl504_105 ),
inference(forward_demodulation,[],[f6508,f5011]) ).
fof(f6837,plain,
( empty_carrier(sK481)
| join_absorbing(sK481)
| ~ latt_str(sK481) ),
inference(resolution,[],[f2211,f3771]) ).
fof(f6838,plain,
( join_absorbing(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f6837,f3772]) ).
fof(f6839,plain,
( ~ latt_str(sK481)
| spl504_73 ),
inference(forward_subsumption_resolution,[],[f6838,f5315]) ).
fof(f6840,plain,
( $false
| spl504_73 ),
inference(forward_subsumption_resolution,[],[f6839,f3770]) ).
fof(f6841,plain,
spl504_73,
inference(avatar_contradiction_clause,[],[f6840]) ).
fof(f6848,plain,
( empty_carrier(sK481)
| meet_absorbing(sK481)
| ~ latt_str(sK481) ),
inference(resolution,[],[f2212,f3771]) ).
fof(f6849,plain,
( meet_absorbing(sK481)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f6848,f3772]) ).
fof(f6850,plain,
( ~ latt_str(sK481)
| spl504_74 ),
inference(forward_subsumption_resolution,[],[f6849,f5319]) ).
fof(f6851,plain,
( $false
| spl504_74 ),
inference(forward_subsumption_resolution,[],[f6850,f3770]) ).
fof(f6852,plain,
spl504_74,
inference(avatar_contradiction_clause,[],[f6851]) ).
fof(f6867,plain,
( ~ in(sK167(sF501,sK480,sK482),sK480)
| ~ element(sK167(sF501,sK480,sK482),sF503)
| ~ spl504_76
| spl504_82 ),
inference(resolution,[],[f5326,f5435]) ).
fof(f6869,plain,
( ~ element(sK167(sF501,sK480,sK482),sF503)
| ~ spl504_76
| spl504_82
| ~ spl504_110 ),
inference(forward_subsumption_resolution,[],[f6867,f6196]) ).
fof(f6871,plain,
( $false
| ~ spl504_76
| ~ spl504_78
| spl504_82
| ~ spl504_110 ),
inference(forward_subsumption_resolution,[],[f6869,f5355]) ).
fof(f6872,plain,
( ~ spl504_76
| ~ spl504_78
| spl504_82
| ~ spl504_110 ),
inference(avatar_contradiction_clause,[],[f6871]) ).
fof(f6873,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| empty_carrier(sF501)
| ~ reflexive_relstr(sF501)
| ~ rel_str(sF501)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| ~ spl504_83 ),
inference(resolution,[],[f5439,f3139]) ).
fof(f6874,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ reflexive_relstr(sF501)
| ~ rel_str(sF501)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| ~ spl504_83 ),
inference(forward_subsumption_resolution,[],[f6873,f5000]) ).
fof(f6875,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ rel_str(sF501)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| ~ spl504_83 ),
inference(forward_subsumption_resolution,[],[f6874,f5210]) ).
fof(f6876,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| ~ spl504_67
| ~ spl504_83 ),
inference(forward_subsumption_resolution,[],[f6875,f5112]) ).
fof(f6877,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| ~ spl504_67
| ~ spl504_77
| ~ spl504_83 ),
inference(forward_subsumption_resolution,[],[f6876,f5350]) ).
fof(f6878,plain,
( related(sF501,sK167(sF501,sK480,sK482),sK482)
| spl504_63
| ~ spl504_67
| ~ spl504_77
| ~ spl504_83 ),
inference(forward_subsumption_resolution,[],[f6877,f5012]) ).
fof(f6879,plain,
( spl504_109
| spl504_63
| ~ spl504_67
| ~ spl504_77
| ~ spl504_83 ),
inference(avatar_split_clause,[],[f6878,f5437,f5349,f5111,f4999,f6191]) ).
fof(f6908,plain,
( relstr_set_smaller(sF501,sK480,sK482)
| ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| ~ spl504_109 ),
inference(resolution,[],[f6193,f2670]) ).
fof(f6912,plain,
( ~ element(sK482,the_carrier(sF501))
| ~ rel_str(sF501)
| spl504_6
| ~ spl504_109 ),
inference(forward_subsumption_resolution,[],[f6908,f5013]) ).
fof(f6914,plain,
( ~ rel_str(sF501)
| spl504_6
| ~ spl504_109 ),
inference(forward_subsumption_resolution,[],[f6912,f5012]) ).
fof(f6916,plain,
( $false
| spl504_6
| ~ spl504_67
| ~ spl504_109 ),
inference(forward_subsumption_resolution,[],[f6914,f5112]) ).
fof(f6917,plain,
( spl504_6
| ~ spl504_67
| ~ spl504_109 ),
inference(avatar_contradiction_clause,[],[f6916]) ).
fof(f6927,plain,
( ~ element(sK167(sF501,sK480,sK482),the_carrier(poset_of_lattice(sK481)))
| ~ spl504_77
| spl504_78 ),
inference(forward_subsumption_resolution,[],[f6212,f5354]) ).
fof(f6934,plain,
( ~ element(sK167(sF501,sK480,sK482),the_carrier(sF501))
| ~ spl504_77
| spl504_78 ),
inference(forward_demodulation,[],[f6927,f4616]) ).
fof(f6937,plain,
( $false
| ~ spl504_77
| spl504_78 ),
inference(forward_subsumption_resolution,[],[f6934,f5350]) ).
fof(f6938,plain,
( ~ spl504_77
| spl504_78 ),
inference(avatar_contradiction_clause,[],[f6937]) ).
fof(f6960,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| empty_carrier(sK481)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_99 ),
inference(resolution,[],[f6093,f3137]) ).
fof(f6961,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ meet_commutative(sK481)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6960,f3772]) ).
fof(f6962,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ meet_absorbing(sK481)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_75
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6961,f5322]) ).
fof(f6963,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ join_absorbing(sK481)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_74
| ~ spl504_75
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6962,f5318]) ).
fof(f6964,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ latt_str(sK481)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6963,f5314]) ).
fof(f6965,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sK481))
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6964,f3770]) ).
fof(f6966,plain,
( ~ element(sK78(sK481,sK482,sK480),sF503)
| below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_99 ),
inference(forward_demodulation,[],[f6965,f4622]) ).
fof(f6967,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ element(sK482,the_carrier(sK481))
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6966,f6075]) ).
fof(f6968,plain,
( ~ element(sK482,sF503)
| below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_demodulation,[],[f6967,f4622]) ).
fof(f6969,plain,
( below(sK481,sK78(sK481,sK482,sK480),sK482)
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6968,f4623]) ).
fof(f6970,plain,
( latt_element_smaller(sK481,sK482,sK480)
| ~ element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ latt_str(sK481)
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(resolution,[],[f6969,f2341]) ).
fof(f6974,plain,
( ~ element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ latt_str(sK481)
| spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6970,f4661]) ).
fof(f6976,plain,
( ~ element(sK482,the_carrier(sK481))
| ~ latt_str(sK481)
| spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6974,f3772]) ).
fof(f6978,plain,
( ~ element(sK482,the_carrier(sK481))
| spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6976,f3770]) ).
fof(f6980,plain,
( ~ element(sK482,sF503)
| spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_demodulation,[],[f6978,f4622]) ).
fof(f6982,plain,
( $false
| spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(forward_subsumption_resolution,[],[f6980,f4623]) ).
fof(f6983,plain,
( spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(avatar_contradiction_clause,[],[f6982]) ).
fof(f6995,plain,
( ~ spl504_100
| spl504_99
| ~ spl504_105 ),
inference(avatar_split_clause,[],[f6509,f6119,f6092,f6096]) ).
fof(f7018,plain,
( related_reflexive(sF501,sK78(sK481,sK482,sK480),sK482)
| empty_carrier(sF501)
| ~ reflexive_relstr(sF501)
| ~ rel_str(sF501)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| ~ spl504_111 ),
inference(resolution,[],[f6324,f3140]) ).
fof(f7019,plain,
( empty_carrier(sF501)
| ~ reflexive_relstr(sF501)
| ~ rel_str(sF501)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7018,f6097]) ).
fof(f7021,plain,
( ~ reflexive_relstr(sF501)
| ~ rel_str(sF501)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7019,f5000]) ).
fof(f7023,plain,
( ~ rel_str(sF501)
| ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7021,f5210]) ).
fof(f7025,plain,
( ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| ~ element(sK482,the_carrier(sF501))
| spl504_63
| ~ spl504_67
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7023,f5112]) ).
fof(f7027,plain,
( ~ element(sK78(sK481,sK482,sK480),the_carrier(sF501))
| spl504_63
| ~ spl504_67
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7025,f5012]) ).
fof(f7029,plain,
( ~ element(sK78(sK481,sK482,sK480),cast_as_carrier_subset(sF501))
| spl504_63
| ~ spl504_67
| spl504_100
| ~ spl504_111 ),
inference(forward_demodulation,[],[f7027,f5713]) ).
fof(f7035,plain,
( $false
| spl504_63
| ~ spl504_67
| ~ spl504_96
| spl504_100
| ~ spl504_111 ),
inference(forward_subsumption_resolution,[],[f7029,f6080]) ).
fof(f7036,plain,
( spl504_63
| ~ spl504_67
| ~ spl504_96
| spl504_100
| ~ spl504_111 ),
inference(avatar_contradiction_clause,[],[f7035]) ).
cnf(s3,plain,
( spl504_5
| spl504_6 ),
inference(sat_conversion,[],[f4667]) ).
cnf(s4,plain,
( ~ spl504_5
| ~ spl504_6 ),
inference(sat_conversion,[],[f4668]) ).
cnf(s52,plain,
~ spl504_63,
inference(sat_conversion,[],[f5040]) ).
cnf(s57,plain,
spl504_67,
inference(sat_conversion,[],[f5269]) ).
cnf(s59,plain,
( ~ spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| spl504_76 ),
inference(sat_conversion,[],[f5327]) ).
cnf(s63,plain,
( spl504_6
| ~ spl504_67
| spl504_77 ),
inference(sat_conversion,[],[f5374]) ).
cnf(s65,plain,
( ~ spl504_78
| ~ spl504_82
| spl504_83 ),
inference(sat_conversion,[],[f5440]) ).
cnf(s76,plain,
spl504_75,
inference(sat_conversion,[],[f5815]) ).
cnf(s99,plain,
( spl504_5
| ~ spl504_95
| spl504_105 ),
inference(sat_conversion,[],[f6182]) ).
cnf(s102,plain,
( spl504_5
| ~ spl504_67
| ~ spl504_95
| spl504_96 ),
inference(sat_conversion,[],[f6185]) ).
cnf(s104,plain,
( spl504_5
| spl504_95 ),
inference(sat_conversion,[],[f6219]) ).
cnf(s105,plain,
( spl504_6
| ~ spl504_67
| spl504_110 ),
inference(sat_conversion,[],[f6224]) ).
cnf(s106,plain,
( ~ spl504_6
| ~ spl504_67
| ~ spl504_96
| spl504_111
| ~ spl504_112 ),
inference(sat_conversion,[],[f6329]) ).
cnf(s107,plain,
( spl504_5
| spl504_112 ),
inference(sat_conversion,[],[f6336]) ).
cnf(s121,plain,
spl504_73,
inference(sat_conversion,[],[f6841]) ).
cnf(s122,plain,
spl504_74,
inference(sat_conversion,[],[f6852]) ).
cnf(s123,plain,
( ~ spl504_76
| ~ spl504_78
| spl504_82
| ~ spl504_110 ),
inference(sat_conversion,[],[f6872]) ).
cnf(s124,plain,
( spl504_63
| ~ spl504_67
| ~ spl504_77
| ~ spl504_83
| spl504_109 ),
inference(sat_conversion,[],[f6879]) ).
cnf(s126,plain,
( spl504_6
| ~ spl504_67
| ~ spl504_109 ),
inference(sat_conversion,[],[f6917]) ).
cnf(s130,plain,
( ~ spl504_77
| spl504_78 ),
inference(sat_conversion,[],[f6938]) ).
cnf(s132,plain,
( spl504_5
| ~ spl504_73
| ~ spl504_74
| ~ spl504_75
| ~ spl504_95
| ~ spl504_99 ),
inference(sat_conversion,[],[f6983]) ).
cnf(s134,plain,
( spl504_99
| ~ spl504_100
| ~ spl504_105 ),
inference(sat_conversion,[],[f6995]) ).
cnf(s137,plain,
( spl504_63
| ~ spl504_67
| ~ spl504_96
| spl504_100
| ~ spl504_111 ),
inference(sat_conversion,[],[f7036]) ).
cnf(s139,plain,
( ~ spl504_5
| spl504_76 ),
inference(rat,[],[s59,s76,s122,s121]) ).
cnf(s145,plain,
spl504_5,
inference(rat,[],[s137,s106,s134,s102,s132,s99,s3,s104,s107,s57,s52,s122,s121,s76]) ).
cnf(s147,plain,
spl504_76,
inference(rat,[],[s139,s145]) ).
cnf(s148,plain,
~ spl504_6,
inference(rat,[],[s4,s145]) ).
cnf(s149,plain,
~ spl504_109,
inference(rat,[],[s126,s57,s148]) ).
cnf(s150,plain,
spl504_110,
inference(rat,[],[s105,s57,s148]) ).
cnf(s151,plain,
spl504_77,
inference(rat,[],[s63,s57,s148]) ).
cnf(s152,plain,
spl504_78,
inference(rat,[],[s130,s151]) ).
cnf(s153,plain,
~ spl504_83,
inference(rat,[],[s124,s149,s52,s57,s151]) ).
cnf(s155,plain,
spl504_82,
inference(rat,[],[s123,s150,s147,s152]) ).
cnf(s156,plain,
$false,
inference(rat,[],[s65,s153,s155,s152]) ).
fof(f7037,plain,
$false,
inference(avatar_sat_refutation,[],[s156]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU349+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n001.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 04:56:02 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.83/2.30 % (31298)Detected formulas, will run a generic FOF schedule.
% 5.83/2.30 % (31303)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=1606314914:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.83/2.30 % (31304)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=1273015075:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.83/2.30 % (31308)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2522352254:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.83/2.30 % (31309)dis-21_1_sil=8000:lcm=predicate:random_seed=558131600: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)
% 5.83/2.30 % (31306)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3148979136:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.83/2.30 % (31305)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=845271979:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.83/2.30 % (31307)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=528988376:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.83/2.30 % (31306)Instruction limit reached!
% 5.83/2.30 % (31306)------------------------------
% 5.83/2.30 % (31306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31306)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31306)Termination reason: Instruction limit
% 5.83/2.30 % (31306)Termination phase: Saturation
% 5.83/2.30 % (31306)Time elapsed: 0.059 s
% 5.83/2.30 % (31306)Peak memory usage: 91 MB
% 5.83/2.30 % (31306)Instructions burned: 110 (million)
% 5.83/2.30 % (31309)Instruction limit reached!
% 5.83/2.30 % (31309)------------------------------
% 5.83/2.30 % (31309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31309)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31309)Termination reason: Instruction limit
% 5.83/2.30 % (31309)Termination phase: Saturation
% 5.83/2.30 % (31309)Time elapsed: 0.066 s
% 5.83/2.30 % (31309)Peak memory usage: 91 MB
% 5.83/2.30 % (31309)Instructions burned: 131 (million)
% 5.83/2.30 % (31307)Instruction limit reached!
% 5.83/2.30 % (31307)------------------------------
% 5.83/2.30 % (31307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31307)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31307)Termination reason: Instruction limit
% 5.83/2.30 % (31307)Termination phase: Saturation
% 5.83/2.30 % (31307)Time elapsed: 0.075 s
% 5.83/2.30 % (31307)Peak memory usage: 91 MB
% 5.83/2.30 % (31307)Instructions burned: 119 (million)
% 5.83/2.30 % (31308)Instruction limit reached!
% 5.83/2.30 % (31308)------------------------------
% 5.83/2.30 % (31308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31308)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31308)Termination reason: Instruction limit
% 5.83/2.30 % (31308)Termination phase: Saturation
% 5.83/2.30 % (31308)Time elapsed: 0.086 s
% 5.83/2.30 % (31308)Peak memory usage: 92 MB
% 5.83/2.30 % (31308)Instructions burned: 139 (million)
% 5.83/2.30 % (31317)lrs+10_1_sil=8000:sp=occurrence:random_seed=828250485:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.83/2.30 % (31318)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3867258739:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.83/2.30 % (31319)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1484040449:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.83/2.30 % (31318)Refutation not found, incomplete strategy
% 5.83/2.30 % (31318)------------------------------
% 5.83/2.30 % (31318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31318)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31318)Termination reason: Refutation not found, incomplete strategy
% 5.83/2.30 % (31318)Time elapsed: 0.013 s
% 5.83/2.30 % (31318)Peak memory usage: 89 MB
% 5.83/2.30 % (31318)Instructions burned: 18 (million)
% 5.83/2.30 % (31320)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=1884506701:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.83/2.30 % (31317)Instruction limit reached!
% 5.83/2.30 % (31317)------------------------------
% 5.83/2.30 % (31317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31317)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31317)Termination reason: Instruction limit
% 5.83/2.30 % (31317)Termination phase: Saturation
% 5.83/2.30 % (31317)Time elapsed: 0.182 s
% 5.83/2.30 % (31317)Peak memory usage: 95 MB
% 5.83/2.30 % (31317)Instructions burned: 286 (million)
% 5.83/2.30 % (31320)Instruction limit reached!
% 5.83/2.30 % (31320)------------------------------
% 5.83/2.30 % (31320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31320)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31320)Termination reason: Instruction limit
% 5.83/2.30 % (31320)Termination phase: Saturation
% 5.83/2.30 % (31320)Time elapsed: 0.142 s
% 5.83/2.30 % (31320)Peak memory usage: 94 MB
% 5.83/2.30 % (31320)Instructions burned: 248 (million)
% 5.83/2.30 % (31319)Instruction limit reached!
% 5.83/2.30 % (31319)------------------------------
% 5.83/2.30 % (31319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31319)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31319)Termination reason: Instruction limit
% 5.83/2.30 % (31319)Termination phase: Saturation
% 5.83/2.30 % (31319)Time elapsed: 0.218 s
% 5.83/2.30 % (31319)Peak memory usage: 95 MB
% 5.83/2.30 % (31319)Instructions burned: 326 (million)
% 5.83/2.30 % (31318)------------------------------
% 5.83/2.30 % (31318)------------------------------
% 5.83/2.30 % (31327)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2775836001:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.83/2.30 % (31326)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2578819280:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.83/2.30 % (31328)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2038300906:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.83/2.30 % (31329)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=899434680:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.83/2.30 % (31328)Instruction limit reached!
% 5.83/2.30 % (31328)------------------------------
% 5.83/2.30 % (31328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31328)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31328)Termination reason: Instruction limit
% 5.83/2.30 % (31328)Termination phase: Saturation
% 5.83/2.30 % (31328)Time elapsed: 0.064 s
% 5.83/2.30 % (31328)Peak memory usage: 92 MB
% 5.83/2.30 % (31328)Instructions burned: 113 (million)
% 5.83/2.30 % (31329)Instruction limit reached!
% 5.83/2.30 % (31329)------------------------------
% 5.83/2.30 % (31329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31329)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31329)Termination reason: Instruction limit
% 5.83/2.30 % (31329)Termination phase: Saturation
% 5.83/2.30 % (31329)Time elapsed: 0.068 s
% 5.83/2.30 % (31329)Peak memory usage: 91 MB
% 5.83/2.30 % (31329)Instructions burned: 128 (million)
% 5.83/2.30 % (31326)Instruction limit reached!
% 5.83/2.30 % (31326)------------------------------
% 5.83/2.30 % (31326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31326)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31326)Termination reason: Instruction limit
% 5.83/2.30 % (31326)Termination phase: Saturation
% 5.83/2.30 % (31326)Time elapsed: 0.183 s
% 5.83/2.30 % (31326)Peak memory usage: 93 MB
% 5.83/2.30 % (31326)Instructions burned: 295 (million)
% 5.83/2.30 % (31334)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2933453180:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 5.83/2.30 % (31335)lrs+10_1_sil=8000:sp=occurrence:random_seed=1783923433:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 5.83/2.30 % (31336)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3732755170:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 5.83/2.30 % (31334)Instruction limit reached!
% 5.83/2.30 % (31334)------------------------------
% 5.83/2.30 % (31334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31334)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31334)Termination reason: Instruction limit
% 5.83/2.30 % (31334)Termination phase: Saturation
% 5.83/2.30 % (31334)Time elapsed: 0.070 s
% 5.83/2.30 % (31334)Peak memory usage: 89 MB
% 5.83/2.30 % (31334)Instructions burned: 115 (million)
% 5.83/2.30 % (31303)First to succeed.
% 5.83/2.30 % (31303)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-31298"
% 5.83/2.30 % (31340)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=462277677:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 5.83/2.30 % (31336)Instruction limit reached!
% 5.83/2.30 % (31336)------------------------------
% 5.83/2.30 % (31336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/2.30 % (31336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/2.30 % (31336)CaDiCaL version: 2.1.3
% 5.83/2.30 % (31336)Termination reason: Instruction limit
% 5.83/2.30 % (31336)Termination phase: Saturation
% 5.83/2.30 % (31336)Time elapsed: 0.267 s
% 5.83/2.30 % (31336)Peak memory usage: 95 MB
% 5.83/2.30 % (31336)Instructions burned: 437 (million)
% 5.83/2.30 % (31303)Refutation found. Thanks to Tanya!
% 5.83/2.30 % SZS status Theorem for theBenchmark
% 5.83/2.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/2.40 % (31303)------------------------------
% 0.17/2.40 % (31303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/2.40 % (31303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/2.40 % (31303)CaDiCaL version: 2.1.3
% 0.17/2.40 % (31303)Termination reason: Refutation
% 0.17/2.40 % (31303)Time elapsed: 0.982 s
% 0.17/2.40 % (31303)Peak memory usage: 146 MB
% 0.17/2.40 % (31303)Instructions burned: 1969 (million)
% 0.17/2.40 % (31303)------------------------------
% 0.17/2.40 % (31303)------------------------------
% 0.17/2.40 % (31298)Success in time 1.417 s
% 0.17/2.40 % Vampire exiting
%------------------------------------------------------------------------------