%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU347+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 10.23s 3.52s
% Output : Refutation 19.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 38
% Syntax : Number of formulae : 365 ( 39 unt; 23 def)
% Number of atoms : 1496 ( 34 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 1969 ( 838 ~; 945 |; 118 &)
% ( 37 <=>; 29 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 21 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/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f56,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X2)
=> below(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_lattice3) ).
fof(f96,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(f105,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(f133,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1,X2] :
( element(X2,the_carrier(X0))
=> ( relstr_element_smaller(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( in(X3,X1)
=> related(X0,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_lattice3) ).
fof(f176,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(f182,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(f189,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(f207,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f289,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(f387,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(f388,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(f451,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f519,conjecture,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_lattice3) ).
fof(f520,negated_conjecture,
~ ! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
inference(negated_conjecture,[status(cth)],[f519]) ).
fof(f616,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(f713,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(f714,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,[],[f713]) ).
fof(f761,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f762,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( latt_set_smaller(X0,X1,X2)
<=> ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f761]) ).
fof(f807,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,[],[f96]) ).
fof(f808,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,[],[f807]) ).
fof(f818,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,[],[f105]) ).
fof(f819,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,[],[f818]) ).
fof(f845,plain,
! [X0] :
( ! [X1,X2] :
( ( relstr_element_smaller(X0,X1,X2)
<=> ! [X3] :
( related(X0,X2,X3)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f133]) ).
fof(f846,plain,
! [X0] :
( ! [X1,X2] :
( ( relstr_element_smaller(X0,X1,X2)
<=> ! [X3] :
( related(X0,X2,X3)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(flattening,[],[f845]) ).
fof(f882,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,[],[f176]) ).
fof(f883,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,[],[f882]) ).
fof(f887,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,[],[f182]) ).
fof(f888,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,[],[f887]) ).
fof(f895,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,[],[f189]) ).
fof(f896,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,[],[f895]) ).
fof(f918,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f207]) ).
fof(f996,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,[],[f289]) ).
fof(f997,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,[],[f996]) ).
fof(f1091,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,[],[f387]) ).
fof(f1092,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,[],[f1091]) ).
fof(f1093,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,[],[f388]) ).
fof(f1094,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,[],[f1093]) ).
fof(f1195,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f451]) ).
fof(f1294,plain,
? [X0,X1] :
( ? [X2] :
( ( latt_set_smaller(X1,X2,X0)
<~> relstr_element_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,[],[f520]) ).
fof(f1295,plain,
? [X0,X1] :
( ? [X2] :
( ( latt_set_smaller(X1,X2,X0)
<~> relstr_element_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,[],[f1294]) ).
fof(f1411,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,[],[f616]) ).
fof(f1412,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,[],[f1411]) ).
fof(f1557,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X1,X3)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( below(X0,X1,X3)
| ~ in(X3,X2)
| ~ element(X3,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f762]) ).
fof(f1558,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ? [X3] :
( ~ below(X0,X1,X3)
& in(X3,X2)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X1,X4)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(rectify,[],[f1557]) ).
fof(f1559,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( latt_set_smaller(X0,X1,X2)
| ( ~ below(X0,X1,sK76(X0,X1,X2))
& in(sK76(X0,X1,X2),X2)
& element(sK76(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( below(X0,X1,X4)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0)) )
| ~ latt_set_smaller(X0,X1,X2) ) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76]),skolemize(X3,sK76(X0,X1,X2))],[f1558]) ).
fof(f1726,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& in(X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ! [X3] :
( related(X0,X2,X3)
| ~ in(X3,X1)
| ~ element(X3,the_carrier(X0)) )
| ~ relstr_element_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f846]) ).
fof(f1727,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_element_smaller(X0,X1,X2)
| ? [X3] :
( ~ related(X0,X2,X3)
& in(X3,X1)
& element(X3,the_carrier(X0)) ) )
& ( ! [X4] :
( related(X0,X2,X4)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0)) )
| ~ relstr_element_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(rectify,[],[f1726]) ).
fof(f1728,plain,
! [X0] :
( ! [X1,X2] :
( ( ( relstr_element_smaller(X0,X1,X2)
| ( ~ related(X0,X2,sK155(X0,X1,X2))
& in(sK155(X0,X1,X2),X1)
& element(sK155(X0,X1,X2),the_carrier(X0)) ) )
& ( ! [X4] :
( related(X0,X2,X4)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0)) )
| ~ relstr_element_smaller(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK155]),skolemize(X3,sK155(X0,X1,X2))],[f1727]) ).
fof(f1819,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,[],[f1092]) ).
fof(f1820,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,[],[f1094]) ).
fof(f2098,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_set_smaller(X1,X2,X0) )
& ( relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_set_smaller(X1,X2,X0) )
& element(X2,the_carrier(X1)) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(nnf_transformation,[],[f1295]) ).
fof(f2099,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_set_smaller(X1,X2,X0) )
& ( relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_set_smaller(X1,X2,X0) )
& element(X2,the_carrier(X1)) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(flattening,[],[f2098]) ).
fof(f2100,plain,
( ( ~ relstr_element_smaller(poset_of_lattice(sK476),sK475,cast_to_el_of_LattPOSet(sK476,sK477))
| ~ latt_set_smaller(sK476,sK477,sK475) )
& ( relstr_element_smaller(poset_of_lattice(sK476),sK475,cast_to_el_of_LattPOSet(sK476,sK477))
| latt_set_smaller(sK476,sK477,sK475) )
& element(sK477,the_carrier(sK476))
& ~ empty_carrier(sK476)
& lattice(sK476)
& latt_str(sK476) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK475,sK476,sK477]),skolemize(X0,sK475),skolemize(X1,sK476),skolemize(X2,sK477)],[f2099]) ).
fof(f2155,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,[],[f1412]) ).
fof(f2191,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| join_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f714]) ).
fof(f2192,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_absorbing(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f714]) ).
fof(f2194,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| meet_commutative(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f714]) ).
fof(f2308,plain,
! [X2,X0,X1,X4] :
( ~ latt_set_smaller(X0,X1,X2)
| ~ in(X4,X2)
| ~ element(X4,the_carrier(X0))
| below(X0,X1,X4)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1559]) ).
fof(f2309,plain,
! [X2,X0,X1] :
( element(sK76(X0,X1,X2),the_carrier(X0))
| latt_set_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1559]) ).
fof(f2310,plain,
! [X2,X0,X1] :
( in(sK76(X0,X1,X2),X2)
| latt_set_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1559]) ).
fof(f2311,plain,
! [X2,X0,X1] :
( ~ below(X0,X1,sK76(X0,X1,X2))
| latt_set_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f1559]) ).
fof(f2473,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,[],[f808]) ).
fof(f2504,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,[],[f819]) ).
fof(f2613,plain,
! [X2,X0,X1,X4] :
( ~ relstr_element_smaller(X0,X1,X2)
| ~ in(X4,X1)
| ~ element(X4,the_carrier(X0))
| related(X0,X2,X4)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1728]) ).
fof(f2614,plain,
! [X2,X0,X1] :
( element(sK155(X0,X1,X2),the_carrier(X0))
| relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1728]) ).
fof(f2615,plain,
! [X2,X0,X1] :
( in(sK155(X0,X1,X2),X1)
| relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1728]) ).
fof(f2616,plain,
! [X2,X0,X1] :
( ~ related(X0,X2,sK155(X0,X1,X2))
| relstr_element_smaller(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1728]) ).
fof(f2671,plain,
! [X0] :
( rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f883]) ).
fof(f2678,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,[],[f888]) ).
fof(f2683,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,[],[f896]) ).
fof(f2700,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f918]) ).
fof(f2877,plain,
! [X0] :
( reflexive_relstr(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f997]) ).
fof(f2879,plain,
! [X0] :
( ~ empty_carrier(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f997]) ).
fof(f3109,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,[],[f1819]) ).
fof(f3110,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,[],[f1819]) ).
fof(f3111,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,[],[f1820]) ).
fof(f3112,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,[],[f1820]) ).
fof(f3618,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f1195]) ).
fof(f3719,plain,
latt_str(sK476),
inference(cnf_transformation,[],[f2100]) ).
fof(f3720,plain,
lattice(sK476),
inference(cnf_transformation,[],[f2100]) ).
fof(f3721,plain,
~ empty_carrier(sK476),
inference(cnf_transformation,[],[f2100]) ).
fof(f3722,plain,
element(sK477,the_carrier(sK476)),
inference(cnf_transformation,[],[f2100]) ).
fof(f3723,plain,
( relstr_element_smaller(poset_of_lattice(sK476),sK475,cast_to_el_of_LattPOSet(sK476,sK477))
| latt_set_smaller(sK476,sK477,sK475) ),
inference(cnf_transformation,[],[f2100]) ).
fof(f3724,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK476),sK475,cast_to_el_of_LattPOSet(sK476,sK477))
| ~ latt_set_smaller(sK476,sK477,sK475) ),
inference(cnf_transformation,[],[f2100]) ).
fof(f3901,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,[],[f2155]) ).
fof(f3902,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,[],[f2155]) ).
fof(f4583,definition,
sF499 = poset_of_lattice(sK476),
introduced(definition,[new_symbols(definition,[sF499])],[function_definition]) ).
fof(f4584,plain,
poset_of_lattice(sK476) = sF499,
inference(reorient_equations,[],[f4583]) ).
fof(f4585,definition,
sF500 = cast_to_el_of_LattPOSet(sK476,sK477),
introduced(definition,[new_symbols(definition,[sF500])],[function_definition]) ).
fof(f4586,plain,
cast_to_el_of_LattPOSet(sK476,sK477) = sF500,
inference(reorient_equations,[],[f4585]) ).
fof(f4587,plain,
( ~ relstr_element_smaller(sF499,sK475,sF500)
| ~ latt_set_smaller(sK476,sK477,sK475) ),
inference(definition_folding,[],[f3724,f4586,f4584]) ).
fof(f4588,plain,
( relstr_element_smaller(sF499,sK475,sF500)
| latt_set_smaller(sK476,sK477,sK475) ),
inference(definition_folding,[],[f3723,f4586,f4584]) ).
fof(f4589,definition,
sF501 = the_carrier(sK476),
introduced(definition,[new_symbols(definition,[sF501])],[function_definition]) ).
fof(f4590,plain,
the_carrier(sK476) = sF501,
inference(reorient_equations,[],[f4589]) ).
fof(f4591,plain,
element(sK477,sF501),
inference(definition_folding,[],[f3722,f4590]) ).
fof(f4631,definition,
( spl502_5
<=> latt_set_smaller(sK476,sK477,sK475) ),
introduced(definition,[new_symbols(definition,[spl502_5])],[avatar_definition]) ).
fof(f4632,plain,
( ~ latt_set_smaller(sK476,sK477,sK475)
| spl502_5 ),
inference(avatar_component_clause,[],[f4631]) ).
fof(f4633,plain,
( latt_set_smaller(sK476,sK477,sK475)
| ~ spl502_5 ),
inference(avatar_component_clause,[],[f4631]) ).
fof(f4635,definition,
( spl502_6
<=> relstr_element_smaller(sF499,sK475,sF500) ),
introduced(definition,[new_symbols(definition,[spl502_6])],[avatar_definition]) ).
fof(f4636,plain,
( ~ relstr_element_smaller(sF499,sK475,sF500)
| spl502_6 ),
inference(avatar_component_clause,[],[f4635]) ).
fof(f4637,plain,
( relstr_element_smaller(sF499,sK475,sF500)
| ~ spl502_6 ),
inference(avatar_component_clause,[],[f4635]) ).
fof(f4638,plain,
( spl502_5
| spl502_6 ),
inference(avatar_split_clause,[],[f4588,f4635,f4631]) ).
fof(f4639,plain,
( ~ spl502_5
| ~ spl502_6 ),
inference(avatar_split_clause,[],[f4587,f4635,f4631]) ).
fof(f4942,plain,
( element(sF500,the_carrier(poset_of_lattice(sK476)))
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476)) ),
inference(superposition,[],[f2678,f4586]) ).
fof(f4945,plain,
( element(sF500,the_carrier(poset_of_lattice(sK476)))
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_subsumption_resolution,[],[f4942,f3721]) ).
fof(f4947,plain,
( element(sF500,the_carrier(poset_of_lattice(sK476)))
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_subsumption_resolution,[],[f4945,f3720]) ).
fof(f4949,plain,
( element(sF500,the_carrier(poset_of_lattice(sK476)))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_subsumption_resolution,[],[f4947,f3719]) ).
fof(f4951,plain,
( element(sF500,the_carrier(sF499))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f4949,f4584]) ).
fof(f4952,plain,
( ~ element(sK477,sF501)
| element(sF500,the_carrier(sF499)) ),
inference(forward_demodulation,[],[f4951,f4590]) ).
fof(f4953,plain,
element(sF500,the_carrier(sF499)),
inference(forward_subsumption_resolution,[],[f4952,f4591]) ).
fof(f4956,plain,
! [X0] :
( ~ element(X0,sF501)
| cast_to_el_of_LattPOSet(sK476,X0) = X0
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2473,f4590]) ).
fof(f4957,plain,
! [X0] :
( ~ element(X0,sF501)
| cast_to_el_of_LattPOSet(sK476,X0) = X0
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f4956,f3721]) ).
fof(f4967,definition,
( spl502_63
<=> empty_carrier(sF499) ),
introduced(definition,[new_symbols(definition,[spl502_63])],[avatar_definition]) ).
fof(f4968,plain,
( ~ empty_carrier(sF499)
| spl502_63 ),
inference(avatar_component_clause,[],[f4967]) ).
fof(f4976,plain,
! [X0] :
( ~ element(X0,sF501)
| cast_to_el_of_LattPOSet(sK476,X0) = X0
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f4957,f3720]) ).
fof(f4977,plain,
! [X0] :
( ~ element(X0,sF501)
| cast_to_el_of_LattPOSet(sK476,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f4976,f3719]) ).
fof(f4978,plain,
sK477 = cast_to_el_of_LattPOSet(sK476,sK477),
inference(resolution,[],[f4977,f4591]) ).
fof(f4979,plain,
sK477 = sF500,
inference(forward_demodulation,[],[f4978,f4586]) ).
fof(f4980,plain,
element(sK477,the_carrier(sF499)),
inference(superposition,[],[f4953,f4979]) ).
fof(f4981,plain,
( ~ relstr_element_smaller(sF499,sK475,sK477)
| spl502_6 ),
inference(superposition,[],[f4636,f4979]) ).
fof(f4986,plain,
! [X0,X1] :
( element(sK76(sK476,X0,X1),sF501)
| latt_set_smaller(sK476,X0,X1)
| ~ element(X0,sF501)
| empty_carrier(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2309,f4590]) ).
fof(f4988,plain,
! [X0,X1] :
( element(sK76(sK476,X0,X1),sF501)
| latt_set_smaller(sK476,X0,X1)
| ~ element(X0,sF501)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f4986,f3721]) ).
fof(f4989,plain,
! [X0,X1] :
( element(sK76(sK476,X0,X1),sF501)
| latt_set_smaller(sK476,X0,X1)
| ~ element(X0,sF501) ),
inference(forward_subsumption_resolution,[],[f4988,f3719]) ).
fof(f4990,plain,
! [X0,X1] :
( latt_set_smaller(sK476,X0,X1)
| ~ element(X0,sF501)
| sK76(sK476,X0,X1) = cast_to_el_of_LattPOSet(sK476,sK76(sK476,X0,X1)) ),
inference(resolution,[],[f4989,f4977]) ).
fof(f4991,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sK476))
| below(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ latt_str(sK476) )
| ~ spl502_5 ),
inference(resolution,[],[f2308,f4633]) ).
fof(f4992,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sK476))
| below(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476))
| ~ latt_str(sK476) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f4991,f3721]) ).
fof(f4993,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sK476))
| below(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476)) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f4992,f3719]) ).
fof(f4994,plain,
( ! [X0] :
( ~ element(X0,sF501)
| ~ in(X0,sK475)
| below(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476)) )
| ~ spl502_5 ),
inference(forward_demodulation,[],[f4993,f4590]) ).
fof(f4995,plain,
( ! [X0] :
( ~ element(sK477,sF501)
| ~ element(X0,sF501)
| ~ in(X0,sK475)
| below(sK476,sK477,X0) )
| ~ spl502_5 ),
inference(forward_demodulation,[],[f4994,f4590]) ).
fof(f4996,plain,
( ! [X0] :
( below(sK476,sK477,X0)
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f4995,f4591]) ).
fof(f5005,plain,
( ~ empty_carrier(sF499)
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2879,f4584]) ).
fof(f5006,plain,
( ~ empty_carrier(sF499)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5005,f3721]) ).
fof(f5007,plain,
( ~ empty_carrier(sF499)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5006,f3720]) ).
fof(f5008,plain,
~ empty_carrier(sF499),
inference(forward_subsumption_resolution,[],[f5007,f3719]) ).
fof(f5009,plain,
~ spl502_63,
inference(avatar_split_clause,[],[f5008,f4967]) ).
fof(f5013,plain,
! [X0] :
( ~ element(X0,the_carrier(sF499))
| cast_to_el_of_lattice(sK476,X0) = X0
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2504,f4584]) ).
fof(f5015,plain,
! [X0] :
( ~ element(X0,the_carrier(sF499))
| cast_to_el_of_lattice(sK476,X0) = X0
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5013,f3721]) ).
fof(f5017,plain,
! [X0] :
( ~ element(X0,the_carrier(sF499))
| cast_to_el_of_lattice(sK476,X0) = X0
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5015,f3720]) ).
fof(f5018,plain,
! [X0] :
( ~ element(X0,the_carrier(sF499))
| cast_to_el_of_lattice(sK476,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f5017,f3719]) ).
fof(f5026,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f3902,f4586]) ).
fof(f5029,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5026,f3721]) ).
fof(f5032,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5029,f3720]) ).
fof(f5035,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_subsumption_resolution,[],[f5032,f3719]) ).
fof(f5038,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(sK476),sK477,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5035,f4979]) ).
fof(f5041,plain,
! [X0] :
( ~ related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5038,f4584]) ).
fof(f5044,plain,
! [X0] :
( ~ element(X0,sF501)
| ~ related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5041,f4590]) ).
fof(f5046,plain,
! [X0] :
( ~ element(sK477,sF501)
| ~ element(X0,sF501)
| ~ related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| below_refl(sK476,sK477,X0) ),
inference(forward_demodulation,[],[f5044,f4590]) ).
fof(f5048,plain,
! [X0] :
( ~ related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ element(X0,sF501)
| below_refl(sK476,sK477,X0) ),
inference(forward_subsumption_resolution,[],[f5046,f4591]) ).
fof(f5080,definition,
( spl502_69
<=> rel_str(sF499) ),
introduced(definition,[new_symbols(definition,[spl502_69])],[avatar_definition]) ).
fof(f5081,plain,
( rel_str(sF499)
| ~ spl502_69 ),
inference(avatar_component_clause,[],[f5080]) ).
fof(f5082,plain,
( ~ rel_str(sF499)
| spl502_69 ),
inference(avatar_component_clause,[],[f5080]) ).
fof(f5108,plain,
( reflexive_relstr(sF499)
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2877,f4584]) ).
fof(f5109,plain,
( reflexive_relstr(sF499)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5108,f3721]) ).
fof(f5110,plain,
( reflexive_relstr(sF499)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5109,f3720]) ).
fof(f5111,plain,
reflexive_relstr(sF499),
inference(forward_subsumption_resolution,[],[f5110,f3719]) ).
fof(f5141,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f3901,f4586]) ).
fof(f5145,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5141,f3721]) ).
fof(f5149,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476))
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5145,f3720]) ).
fof(f5153,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK476),sF500,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_subsumption_resolution,[],[f5149,f3719]) ).
fof(f5157,plain,
! [X0] :
( related_reflexive(poset_of_lattice(sK476),sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5153,f4979]) ).
fof(f5161,plain,
! [X0] :
( related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(X0,the_carrier(sK476))
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5157,f4584]) ).
fof(f5165,plain,
! [X0] :
( ~ element(X0,sF501)
| related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0)
| ~ element(sK477,the_carrier(sK476)) ),
inference(forward_demodulation,[],[f5161,f4590]) ).
fof(f5167,plain,
! [X0] :
( ~ element(sK477,sF501)
| ~ element(X0,sF501)
| related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ below_refl(sK476,sK477,X0) ),
inference(forward_demodulation,[],[f5165,f4590]) ).
fof(f5169,plain,
! [X0] :
( related_reflexive(sF499,sK477,cast_to_el_of_LattPOSet(sK476,X0))
| ~ element(X0,sF501)
| ~ below_refl(sK476,sK477,X0) ),
inference(forward_subsumption_resolution,[],[f5167,f4591]) ).
fof(f5191,plain,
( rel_str(sF499)
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476) ),
inference(superposition,[],[f2671,f4584]) ).
fof(f5192,plain,
( empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476)
| spl502_69 ),
inference(forward_subsumption_resolution,[],[f5191,f5082]) ).
fof(f5193,plain,
( ~ lattice(sK476)
| ~ latt_str(sK476)
| spl502_69 ),
inference(forward_subsumption_resolution,[],[f5192,f3721]) ).
fof(f5194,plain,
( ~ latt_str(sK476)
| spl502_69 ),
inference(forward_subsumption_resolution,[],[f5193,f3720]) ).
fof(f5195,plain,
( $false
| spl502_69 ),
inference(forward_subsumption_resolution,[],[f5194,f3719]) ).
fof(f5196,plain,
spl502_69,
inference(avatar_contradiction_clause,[],[f5195]) ).
fof(f5221,plain,
( ! [X0] :
( below_refl(sK476,sK477,X0)
| empty_carrier(sK476)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(X0,the_carrier(sK476))
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(resolution,[],[f3110,f4996]) ).
fof(f5222,plain,
( ! [X0] :
( below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(X0,the_carrier(sK476))
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f5221,f3721]) ).
fof(f5223,plain,
( ! [X0] :
( below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(X0,the_carrier(sK476))
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f5222,f3719]) ).
fof(f5224,plain,
( ! [X0] :
( ~ element(sK477,sF501)
| below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ element(X0,the_carrier(sK476))
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_demodulation,[],[f5223,f4590]) ).
fof(f5225,plain,
( ! [X0] :
( below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ element(X0,the_carrier(sK476))
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_subsumption_resolution,[],[f5224,f4591]) ).
fof(f5226,plain,
( ! [X0] :
( ~ element(X0,sF501)
| below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_5 ),
inference(forward_demodulation,[],[f5225,f4590]) ).
fof(f5227,plain,
( ! [X0] :
( ~ element(X0,sF501)
| below_refl(sK476,sK477,X0)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ in(X0,sK475) )
| ~ spl502_5 ),
inference(duplicate_literal_removal,[],[f5226]) ).
fof(f5229,definition,
( spl502_71
<=> join_absorbing(sK476) ),
introduced(definition,[new_symbols(definition,[spl502_71])],[avatar_definition]) ).
fof(f5230,plain,
( join_absorbing(sK476)
| ~ spl502_71 ),
inference(avatar_component_clause,[],[f5229]) ).
fof(f5231,plain,
( ~ join_absorbing(sK476)
| spl502_71 ),
inference(avatar_component_clause,[],[f5229]) ).
fof(f5233,definition,
( spl502_72
<=> meet_absorbing(sK476) ),
introduced(definition,[new_symbols(definition,[spl502_72])],[avatar_definition]) ).
fof(f5234,plain,
( meet_absorbing(sK476)
| ~ spl502_72 ),
inference(avatar_component_clause,[],[f5233]) ).
fof(f5235,plain,
( ~ meet_absorbing(sK476)
| spl502_72 ),
inference(avatar_component_clause,[],[f5233]) ).
fof(f5237,definition,
( spl502_73
<=> meet_commutative(sK476) ),
introduced(definition,[new_symbols(definition,[spl502_73])],[avatar_definition]) ).
fof(f5238,plain,
( meet_commutative(sK476)
| ~ spl502_73 ),
inference(avatar_component_clause,[],[f5237]) ).
fof(f5241,definition,
( spl502_74
<=> ! [X0] :
( ~ element(X0,sF501)
| ~ in(X0,sK475)
| below_refl(sK476,sK477,X0) ) ),
introduced(definition,[new_symbols(definition,[spl502_74])],[avatar_definition]) ).
fof(f5242,plain,
( ! [X0] :
( below_refl(sK476,sK477,X0)
| ~ in(X0,sK475)
| ~ element(X0,sF501) )
| ~ spl502_74 ),
inference(avatar_component_clause,[],[f5241]) ).
fof(f5243,plain,
( ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| spl502_74
| ~ spl502_5 ),
inference(avatar_split_clause,[],[f5227,f4631,f5241,f5237,f5233,f5229]) ).
fof(f5319,definition,
( spl502_77
<=> element(sK155(sF499,sK475,sK477),the_carrier(sF499)) ),
introduced(definition,[new_symbols(definition,[spl502_77])],[avatar_definition]) ).
fof(f5320,plain,
( element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| ~ spl502_77 ),
inference(avatar_component_clause,[],[f5319]) ).
fof(f5321,plain,
( ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| spl502_77 ),
inference(avatar_component_clause,[],[f5319]) ).
fof(f5323,definition,
( spl502_78
<=> element(sK155(sF499,sK475,sK477),sF501) ),
introduced(definition,[new_symbols(definition,[spl502_78])],[avatar_definition]) ).
fof(f5324,plain,
( ~ element(sK155(sF499,sK475,sK477),sF501)
| spl502_78 ),
inference(avatar_component_clause,[],[f5323]) ).
fof(f5325,plain,
( element(sK155(sF499,sK475,sK477),sF501)
| ~ spl502_78 ),
inference(avatar_component_clause,[],[f5323]) ).
fof(f5332,plain,
( relstr_element_smaller(sF499,sK475,sK477)
| ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| spl502_77 ),
inference(resolution,[],[f5321,f2614]) ).
fof(f5333,plain,
( ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| spl502_6
| spl502_77 ),
inference(forward_subsumption_resolution,[],[f5332,f4981]) ).
fof(f5334,plain,
( ~ rel_str(sF499)
| spl502_6
| spl502_77 ),
inference(forward_subsumption_resolution,[],[f5333,f4980]) ).
fof(f5335,plain,
( $false
| spl502_6
| ~ spl502_69
| spl502_77 ),
inference(forward_subsumption_resolution,[],[f5334,f5081]) ).
fof(f5336,plain,
( spl502_6
| ~ spl502_69
| spl502_77 ),
inference(avatar_contradiction_clause,[],[f5335]) ).
fof(f5337,plain,
( relstr_element_smaller(sF499,sK475,sK477)
| ~ spl502_6 ),
inference(forward_demodulation,[],[f4637,f4979]) ).
fof(f5342,plain,
( ~ element(sK477,sF501)
| sK76(sK476,sK477,sK475) = cast_to_el_of_LattPOSet(sK476,sK76(sK476,sK477,sK475))
| spl502_5 ),
inference(resolution,[],[f4632,f4990]) ).
fof(f5343,plain,
( sK76(sK476,sK477,sK475) = cast_to_el_of_LattPOSet(sK476,sK76(sK476,sK477,sK475))
| spl502_5 ),
inference(forward_subsumption_resolution,[],[f5342,f4591]) ).
fof(f5357,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(poset_of_lattice(sK476)))
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| spl502_5 ),
inference(superposition,[],[f2678,f5343]) ).
fof(f5358,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(poset_of_lattice(sK476)))
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| spl502_5 ),
inference(forward_subsumption_resolution,[],[f5357,f3721]) ).
fof(f5364,definition,
( spl502_79
<=> below_refl(sK476,sK477,sK76(sK476,sK477,sK475)) ),
introduced(definition,[new_symbols(definition,[spl502_79])],[avatar_definition]) ).
fof(f5365,plain,
( below_refl(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_79 ),
inference(avatar_component_clause,[],[f5364]) ).
fof(f5368,definition,
( spl502_80
<=> element(sK76(sK476,sK477,sK475),sF501) ),
introduced(definition,[new_symbols(definition,[spl502_80])],[avatar_definition]) ).
fof(f5369,plain,
( element(sK76(sK476,sK477,sK475),sF501)
| ~ spl502_80 ),
inference(avatar_component_clause,[],[f5368]) ).
fof(f5370,plain,
( ~ element(sK76(sK476,sK477,sK475),sF501)
| spl502_80 ),
inference(avatar_component_clause,[],[f5368]) ).
fof(f5372,definition,
( spl502_81
<=> related_reflexive(sF499,sK477,sK76(sK476,sK477,sK475)) ),
introduced(definition,[new_symbols(definition,[spl502_81])],[avatar_definition]) ).
fof(f5373,plain,
( ~ related_reflexive(sF499,sK477,sK76(sK476,sK477,sK475))
| spl502_81 ),
inference(avatar_component_clause,[],[f5372]) ).
fof(f5404,definition,
( spl502_88
<=> element(sK76(sK476,sK477,sK475),the_carrier(sF499)) ),
introduced(definition,[new_symbols(definition,[spl502_88])],[avatar_definition]) ).
fof(f5406,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| ~ spl502_88 ),
inference(avatar_component_clause,[],[f5404]) ).
fof(f5408,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(poset_of_lattice(sK476)))
| ~ latt_str(sK476)
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| spl502_5 ),
inference(forward_subsumption_resolution,[],[f5358,f3720]) ).
fof(f5413,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(poset_of_lattice(sK476)))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| spl502_5 ),
inference(forward_subsumption_resolution,[],[f5408,f3719]) ).
fof(f5418,plain,
( element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| spl502_5 ),
inference(forward_demodulation,[],[f5413,f4584]) ).
fof(f5423,plain,
( ~ element(sK76(sK476,sK477,sK475),sF501)
| element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_5 ),
inference(forward_demodulation,[],[f5418,f4590]) ).
fof(f5428,plain,
( spl502_88
| ~ spl502_80
| spl502_5 ),
inference(avatar_split_clause,[],[f5423,f4631,f5368,f5404]) ).
fof(f5446,plain,
( latt_set_smaller(sK476,sK477,sK475)
| ~ element(sK477,sF501)
| spl502_80 ),
inference(resolution,[],[f5370,f4989]) ).
fof(f5447,plain,
( ~ element(sK477,sF501)
| spl502_5
| spl502_80 ),
inference(forward_subsumption_resolution,[],[f5446,f4632]) ).
fof(f5448,plain,
( $false
| spl502_5
| spl502_80 ),
inference(forward_subsumption_resolution,[],[f5447,f4591]) ).
fof(f5449,plain,
( spl502_5
| spl502_80 ),
inference(avatar_contradiction_clause,[],[f5448]) ).
fof(f5471,plain,
( sK155(sF499,sK475,sK477) = cast_to_el_of_lattice(sK476,sK155(sF499,sK475,sK477))
| ~ spl502_77 ),
inference(resolution,[],[f5320,f5018]) ).
fof(f5476,plain,
( sK155(sF499,sK475,sK477) = cast_to_el_of_LattPOSet(sK476,sK155(sF499,sK475,sK477))
| ~ spl502_78 ),
inference(resolution,[],[f5325,f4977]) ).
fof(f5486,plain,
( related_reflexive(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ element(sK155(sF499,sK475,sK477),sF501)
| ~ below_refl(sK476,sK477,sK155(sF499,sK475,sK477))
| ~ spl502_78 ),
inference(superposition,[],[f5169,f5476]) ).
fof(f5497,plain,
( related_reflexive(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ below_refl(sK476,sK477,sK155(sF499,sK475,sK477))
| ~ spl502_78 ),
inference(forward_subsumption_resolution,[],[f5486,f5325]) ).
fof(f5511,definition,
( spl502_89
<=> below_refl(sK476,sK477,sK155(sF499,sK475,sK477)) ),
introduced(definition,[new_symbols(definition,[spl502_89])],[avatar_definition]) ).
fof(f5513,plain,
( ~ below_refl(sK476,sK477,sK155(sF499,sK475,sK477))
| spl502_89 ),
inference(avatar_component_clause,[],[f5511]) ).
fof(f5515,definition,
( spl502_90
<=> related_reflexive(sF499,sK477,sK155(sF499,sK475,sK477)) ),
introduced(definition,[new_symbols(definition,[spl502_90])],[avatar_definition]) ).
fof(f5517,plain,
( related_reflexive(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ spl502_90 ),
inference(avatar_component_clause,[],[f5515]) ).
fof(f5518,plain,
( ~ spl502_89
| spl502_90
| ~ spl502_78 ),
inference(avatar_split_clause,[],[f5497,f5323,f5515,f5511]) ).
fof(f5656,plain,
( one_sorted_str(sF499)
| ~ spl502_69 ),
inference(resolution,[],[f2700,f5081]) ).
fof(f5657,plain,
( the_carrier(sF499) = cast_as_carrier_subset(sF499)
| ~ spl502_69 ),
inference(resolution,[],[f5656,f3618]) ).
fof(f5753,plain,
( empty_carrier(sK476)
| join_absorbing(sK476)
| ~ latt_str(sK476) ),
inference(resolution,[],[f2191,f3720]) ).
fof(f5754,plain,
( join_absorbing(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5753,f3721]) ).
fof(f5755,plain,
( ~ latt_str(sK476)
| spl502_71 ),
inference(forward_subsumption_resolution,[],[f5754,f5231]) ).
fof(f5756,plain,
( $false
| spl502_71 ),
inference(forward_subsumption_resolution,[],[f5755,f3719]) ).
fof(f5757,plain,
spl502_71,
inference(avatar_contradiction_clause,[],[f5756]) ).
fof(f5898,plain,
( empty_carrier(sK476)
| meet_commutative(sK476)
| ~ latt_str(sK476) ),
inference(resolution,[],[f2194,f3720]) ).
fof(f5899,plain,
( meet_commutative(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5898,f3721]) ).
fof(f5900,plain,
meet_commutative(sK476),
inference(forward_subsumption_resolution,[],[f5899,f3719]) ).
fof(f5901,plain,
spl502_73,
inference(avatar_split_clause,[],[f5900,f5237]) ).
fof(f5912,plain,
( element(sK155(sF499,sK475,sK477),cast_as_carrier_subset(sF499))
| ~ spl502_69
| ~ spl502_77 ),
inference(superposition,[],[f5320,f5657]) ).
fof(f5941,plain,
( empty_carrier(sK476)
| meet_absorbing(sK476)
| ~ latt_str(sK476) ),
inference(resolution,[],[f2192,f3720]) ).
fof(f5942,plain,
( meet_absorbing(sK476)
| ~ latt_str(sK476) ),
inference(forward_subsumption_resolution,[],[f5941,f3721]) ).
fof(f5943,plain,
( ~ latt_str(sK476)
| spl502_72 ),
inference(forward_subsumption_resolution,[],[f5942,f5235]) ).
fof(f5944,plain,
( $false
| spl502_72 ),
inference(forward_subsumption_resolution,[],[f5943,f3719]) ).
fof(f5945,plain,
spl502_72,
inference(avatar_contradiction_clause,[],[f5944]) ).
fof(f5957,plain,
( ~ in(sK155(sF499,sK475,sK477),sK475)
| ~ element(sK155(sF499,sK475,sK477),sF501)
| ~ spl502_74
| spl502_89 ),
inference(resolution,[],[f5242,f5513]) ).
fof(f5966,plain,
( element(sK76(sK476,sK477,sK475),cast_as_carrier_subset(sF499))
| ~ spl502_69
| ~ spl502_88 ),
inference(forward_demodulation,[],[f5406,f5657]) ).
fof(f5968,definition,
( spl502_103
<=> in(sK155(sF499,sK475,sK477),sK475) ),
introduced(definition,[new_symbols(definition,[spl502_103])],[avatar_definition]) ).
fof(f5970,plain,
( ~ in(sK155(sF499,sK475,sK477),sK475)
| spl502_103 ),
inference(avatar_component_clause,[],[f5968]) ).
fof(f5971,plain,
( ~ spl502_78
| ~ spl502_103
| ~ spl502_74
| spl502_89 ),
inference(avatar_split_clause,[],[f5957,f5511,f5241,f5968,f5323]) ).
fof(f5981,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sF499))
| related(sF499,sK477,X0)
| ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499) )
| ~ spl502_6 ),
inference(resolution,[],[f5337,f2613]) ).
fof(f5982,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sF499))
| related(sF499,sK477,X0)
| ~ rel_str(sF499) )
| ~ spl502_6 ),
inference(forward_subsumption_resolution,[],[f5981,f4980]) ).
fof(f5983,plain,
( ! [X0] :
( ~ in(X0,sK475)
| ~ element(X0,the_carrier(sF499))
| related(sF499,sK477,X0) )
| ~ spl502_6
| ~ spl502_69 ),
inference(forward_subsumption_resolution,[],[f5982,f5081]) ).
fof(f5984,plain,
( ! [X0] :
( ~ element(X0,cast_as_carrier_subset(sF499))
| ~ in(X0,sK475)
| related(sF499,sK477,X0) )
| ~ spl502_6
| ~ spl502_69 ),
inference(forward_demodulation,[],[f5983,f5657]) ).
fof(f6034,plain,
( sK76(sK476,sK477,sK475) = cast_to_el_of_LattPOSet(sK476,sK76(sK476,sK477,sK475))
| ~ spl502_80 ),
inference(resolution,[],[f5369,f4977]) ).
fof(f6063,definition,
( spl502_104
<=> related(sF499,sK477,sK155(sF499,sK475,sK477)) ),
introduced(definition,[new_symbols(definition,[spl502_104])],[avatar_definition]) ).
fof(f6065,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ spl502_104 ),
inference(avatar_component_clause,[],[f6063]) ).
fof(f6067,plain,
( relstr_element_smaller(sF499,sK475,sK477)
| ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| spl502_103 ),
inference(resolution,[],[f5970,f2615]) ).
fof(f6075,plain,
( element(sK155(sF499,sK475,sK477),the_carrier(sK476))
| empty_carrier(sK476)
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77 ),
inference(superposition,[],[f2683,f5471]) ).
fof(f6076,plain,
( element(sK155(sF499,sK475,sK477),the_carrier(sK476))
| ~ lattice(sK476)
| ~ latt_str(sK476)
| ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77 ),
inference(forward_subsumption_resolution,[],[f6075,f3721]) ).
fof(f6078,plain,
( element(sK155(sF499,sK475,sK477),the_carrier(sK476))
| ~ latt_str(sK476)
| ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77 ),
inference(forward_subsumption_resolution,[],[f6076,f3720]) ).
fof(f6081,plain,
( element(sK155(sF499,sK475,sK477),the_carrier(sK476))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77 ),
inference(forward_subsumption_resolution,[],[f6078,f3719]) ).
fof(f6082,plain,
( element(sK155(sF499,sK475,sK477),sF501)
| ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77 ),
inference(forward_demodulation,[],[f6081,f4590]) ).
fof(f6083,plain,
( ~ element(sK155(sF499,sK475,sK477),the_carrier(poset_of_lattice(sK476)))
| ~ spl502_77
| spl502_78 ),
inference(forward_subsumption_resolution,[],[f6082,f5324]) ).
fof(f6084,plain,
( ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| ~ spl502_77
| spl502_78 ),
inference(forward_demodulation,[],[f6083,f4584]) ).
fof(f6085,plain,
( $false
| ~ spl502_77
| spl502_78 ),
inference(forward_subsumption_resolution,[],[f6084,f5320]) ).
fof(f6086,plain,
( ~ spl502_77
| spl502_78 ),
inference(avatar_contradiction_clause,[],[f6085]) ).
fof(f6088,plain,
( ~ in(sK76(sK476,sK477,sK475),sK475)
| related(sF499,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_6
| ~ spl502_69
| ~ spl502_88 ),
inference(resolution,[],[f5966,f5984]) ).
fof(f6091,definition,
( spl502_105
<=> related(sF499,sK477,sK76(sK476,sK477,sK475)) ),
introduced(definition,[new_symbols(definition,[spl502_105])],[avatar_definition]) ).
fof(f6093,plain,
( related(sF499,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_105 ),
inference(avatar_component_clause,[],[f6091]) ).
fof(f6095,definition,
( spl502_106
<=> in(sK76(sK476,sK477,sK475),sK475) ),
introduced(definition,[new_symbols(definition,[spl502_106])],[avatar_definition]) ).
fof(f6097,plain,
( ~ in(sK76(sK476,sK477,sK475),sK475)
| spl502_106 ),
inference(avatar_component_clause,[],[f6095]) ).
fof(f6098,plain,
( spl502_105
| ~ spl502_106
| ~ spl502_6
| ~ spl502_69
| ~ spl502_88 ),
inference(avatar_split_clause,[],[f6088,f5404,f5080,f4635,f6095,f6091]) ).
fof(f6099,plain,
( latt_set_smaller(sK476,sK477,sK475)
| ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ latt_str(sK476)
| spl502_106 ),
inference(resolution,[],[f6097,f2310]) ).
fof(f6100,plain,
( ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ latt_str(sK476)
| spl502_5
| spl502_106 ),
inference(forward_subsumption_resolution,[],[f6099,f4632]) ).
fof(f6101,plain,
( ~ element(sK477,the_carrier(sK476))
| ~ latt_str(sK476)
| spl502_5
| spl502_106 ),
inference(forward_subsumption_resolution,[],[f6100,f3721]) ).
fof(f6102,plain,
( ~ element(sK477,the_carrier(sK476))
| spl502_5
| spl502_106 ),
inference(forward_subsumption_resolution,[],[f6101,f3719]) ).
fof(f6103,plain,
( ~ element(sK477,sF501)
| spl502_5
| spl502_106 ),
inference(forward_demodulation,[],[f6102,f4590]) ).
fof(f6104,plain,
( $false
| spl502_5
| spl502_106 ),
inference(forward_subsumption_resolution,[],[f6103,f4591]) ).
fof(f6105,plain,
( spl502_5
| spl502_106 ),
inference(avatar_contradiction_clause,[],[f6104]) ).
fof(f6107,plain,
( related_reflexive(sF499,sK477,sK76(sK476,sK477,sK475))
| empty_carrier(sF499)
| ~ reflexive_relstr(sF499)
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| ~ spl502_105 ),
inference(resolution,[],[f6093,f3112]) ).
fof(f6108,plain,
( empty_carrier(sF499)
| ~ reflexive_relstr(sF499)
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_81
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6107,f5373]) ).
fof(f6109,plain,
( ~ reflexive_relstr(sF499)
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_63
| spl502_81
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6108,f4968]) ).
fof(f6110,plain,
( ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_63
| spl502_81
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6109,f5111]) ).
fof(f6111,plain,
( ~ element(sK477,the_carrier(sF499))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6110,f5081]) ).
fof(f6112,plain,
( ~ element(sK76(sK476,sK477,sK475),the_carrier(sF499))
| spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6111,f4980]) ).
fof(f6113,plain,
( ~ element(sK76(sK476,sK477,sK475),cast_as_carrier_subset(sF499))
| spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_105 ),
inference(forward_demodulation,[],[f6112,f5657]) ).
fof(f6114,plain,
( $false
| spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_88
| ~ spl502_105 ),
inference(forward_subsumption_resolution,[],[f6113,f5966]) ).
fof(f6115,plain,
( spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_88
| ~ spl502_105 ),
inference(avatar_contradiction_clause,[],[f6114]) ).
fof(f6117,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| empty_carrier(sK476)
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_79 ),
inference(resolution,[],[f5365,f3109]) ).
fof(f6118,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ meet_commutative(sK476)
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6117,f3721]) ).
fof(f6119,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ meet_absorbing(sK476)
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6118,f5238]) ).
fof(f6120,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ join_absorbing(sK476)
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6119,f5234]) ).
fof(f6121,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ latt_str(sK476)
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6120,f5230]) ).
fof(f6122,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ element(sK477,the_carrier(sK476))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6121,f3719]) ).
fof(f6123,plain,
( ~ element(sK477,sF501)
| below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_demodulation,[],[f6122,f4590]) ).
fof(f6124,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ element(sK76(sK476,sK477,sK475),the_carrier(sK476))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_subsumption_resolution,[],[f6123,f4591]) ).
fof(f6125,plain,
( ~ element(sK76(sK476,sK477,sK475),sF501)
| below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79 ),
inference(forward_demodulation,[],[f6124,f4590]) ).
fof(f6126,plain,
( below(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6125,f5369]) ).
fof(f6127,plain,
( latt_set_smaller(sK476,sK477,sK475)
| ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ latt_str(sK476)
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(resolution,[],[f6126,f2311]) ).
fof(f6130,plain,
( ~ element(sK477,the_carrier(sK476))
| empty_carrier(sK476)
| ~ latt_str(sK476)
| spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6127,f4632]) ).
fof(f6131,plain,
( ~ element(sK477,the_carrier(sK476))
| ~ latt_str(sK476)
| spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6130,f3721]) ).
fof(f6132,plain,
( ~ element(sK477,the_carrier(sK476))
| spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6131,f3719]) ).
fof(f6133,plain,
( ~ element(sK477,sF501)
| spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_demodulation,[],[f6132,f4590]) ).
fof(f6134,plain,
( $false
| spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6133,f4591]) ).
fof(f6135,plain,
( spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(avatar_contradiction_clause,[],[f6134]) ).
fof(f6142,plain,
( ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| spl502_6
| spl502_103 ),
inference(forward_subsumption_resolution,[],[f6067,f4981]) ).
fof(f6143,plain,
( ~ rel_str(sF499)
| spl502_6
| spl502_103 ),
inference(forward_subsumption_resolution,[],[f6142,f4980]) ).
fof(f6144,plain,
( $false
| spl502_6
| ~ spl502_69
| spl502_103 ),
inference(forward_subsumption_resolution,[],[f6143,f5081]) ).
fof(f6145,plain,
( spl502_6
| ~ spl502_69
| spl502_103 ),
inference(avatar_contradiction_clause,[],[f6144]) ).
fof(f6154,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| empty_carrier(sF499)
| ~ reflexive_relstr(sF499)
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| ~ spl502_90 ),
inference(resolution,[],[f5517,f3111]) ).
fof(f6155,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ reflexive_relstr(sF499)
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| spl502_63
| ~ spl502_90 ),
inference(forward_subsumption_resolution,[],[f6154,f4968]) ).
fof(f6156,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ rel_str(sF499)
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| spl502_63
| ~ spl502_90 ),
inference(forward_subsumption_resolution,[],[f6155,f5111]) ).
fof(f6157,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ element(sK477,the_carrier(sF499))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| spl502_63
| ~ spl502_69
| ~ spl502_90 ),
inference(forward_subsumption_resolution,[],[f6156,f5081]) ).
fof(f6158,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| ~ element(sK155(sF499,sK475,sK477),the_carrier(sF499))
| spl502_63
| ~ spl502_69
| ~ spl502_90 ),
inference(forward_subsumption_resolution,[],[f6157,f4980]) ).
fof(f6159,plain,
( ~ element(sK155(sF499,sK475,sK477),cast_as_carrier_subset(sF499))
| related(sF499,sK477,sK155(sF499,sK475,sK477))
| spl502_63
| ~ spl502_69
| ~ spl502_90 ),
inference(forward_demodulation,[],[f6158,f5657]) ).
fof(f6160,plain,
( related(sF499,sK477,sK155(sF499,sK475,sK477))
| spl502_63
| ~ spl502_69
| ~ spl502_77
| ~ spl502_90 ),
inference(forward_subsumption_resolution,[],[f6159,f5912]) ).
fof(f6161,plain,
( spl502_104
| spl502_63
| ~ spl502_69
| ~ spl502_77
| ~ spl502_90 ),
inference(avatar_split_clause,[],[f6160,f5515,f5319,f5080,f4967,f6063]) ).
fof(f6170,plain,
( ~ related_reflexive(sF499,sK477,sK76(sK476,sK477,sK475))
| ~ element(sK76(sK476,sK477,sK475),sF501)
| below_refl(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_80 ),
inference(superposition,[],[f5048,f6034]) ).
fof(f6187,plain,
( ~ related_reflexive(sF499,sK477,sK76(sK476,sK477,sK475))
| below_refl(sK476,sK477,sK76(sK476,sK477,sK475))
| ~ spl502_80 ),
inference(forward_subsumption_resolution,[],[f6170,f5369]) ).
fof(f6195,plain,
( spl502_79
| ~ spl502_81
| ~ spl502_80 ),
inference(avatar_split_clause,[],[f6187,f5368,f5372,f5364]) ).
fof(f6297,plain,
( relstr_element_smaller(sF499,sK475,sK477)
| ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| ~ spl502_104 ),
inference(resolution,[],[f6065,f2616]) ).
fof(f6299,plain,
( ~ element(sK477,the_carrier(sF499))
| ~ rel_str(sF499)
| spl502_6
| ~ spl502_104 ),
inference(forward_subsumption_resolution,[],[f6297,f4981]) ).
fof(f6300,plain,
( ~ rel_str(sF499)
| spl502_6
| ~ spl502_104 ),
inference(forward_subsumption_resolution,[],[f6299,f4980]) ).
fof(f6301,plain,
( $false
| spl502_6
| ~ spl502_69
| ~ spl502_104 ),
inference(forward_subsumption_resolution,[],[f6300,f5081]) ).
fof(f6302,plain,
( spl502_6
| ~ spl502_69
| ~ spl502_104 ),
inference(avatar_contradiction_clause,[],[f6301]) ).
cnf(s3,plain,
( spl502_5
| spl502_6 ),
inference(sat_conversion,[],[f4638]) ).
cnf(s4,plain,
( ~ spl502_5
| ~ spl502_6 ),
inference(sat_conversion,[],[f4639]) ).
cnf(s52,plain,
~ spl502_63,
inference(sat_conversion,[],[f5009]) ).
cnf(s57,plain,
spl502_69,
inference(sat_conversion,[],[f5196]) ).
cnf(s58,plain,
( ~ spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| spl502_74 ),
inference(sat_conversion,[],[f5243]) ).
cnf(s64,plain,
( spl502_6
| ~ spl502_69
| spl502_77 ),
inference(sat_conversion,[],[f5336]) ).
cnf(s74,plain,
( spl502_5
| ~ spl502_80
| spl502_88 ),
inference(sat_conversion,[],[f5428]) ).
cnf(s79,plain,
( spl502_5
| spl502_80 ),
inference(sat_conversion,[],[f5449]) ).
cnf(s82,plain,
( ~ spl502_78
| ~ spl502_89
| spl502_90 ),
inference(sat_conversion,[],[f5518]) ).
cnf(s92,plain,
spl502_71,
inference(sat_conversion,[],[f5757]) ).
cnf(s96,plain,
spl502_73,
inference(sat_conversion,[],[f5901]) ).
cnf(s97,plain,
spl502_72,
inference(sat_conversion,[],[f5945]) ).
cnf(s99,plain,
( ~ spl502_74
| ~ spl502_78
| spl502_89
| ~ spl502_103 ),
inference(sat_conversion,[],[f5971]) ).
cnf(s103,plain,
( ~ spl502_77
| spl502_78 ),
inference(sat_conversion,[],[f6086]) ).
cnf(s104,plain,
( ~ spl502_6
| ~ spl502_69
| ~ spl502_88
| spl502_105
| ~ spl502_106 ),
inference(sat_conversion,[],[f6098]) ).
cnf(s105,plain,
( spl502_5
| spl502_106 ),
inference(sat_conversion,[],[f6105]) ).
cnf(s106,plain,
( spl502_63
| ~ spl502_69
| spl502_81
| ~ spl502_88
| ~ spl502_105 ),
inference(sat_conversion,[],[f6115]) ).
cnf(s107,plain,
( spl502_5
| ~ spl502_71
| ~ spl502_72
| ~ spl502_73
| ~ spl502_79
| ~ spl502_80 ),
inference(sat_conversion,[],[f6135]) ).
cnf(s108,plain,
( spl502_6
| ~ spl502_69
| spl502_103 ),
inference(sat_conversion,[],[f6145]) ).
cnf(s109,plain,
( spl502_63
| ~ spl502_69
| ~ spl502_77
| ~ spl502_90
| spl502_104 ),
inference(sat_conversion,[],[f6161]) ).
cnf(s111,plain,
( spl502_79
| ~ spl502_80
| ~ spl502_81 ),
inference(sat_conversion,[],[f6195]) ).
cnf(s113,plain,
( spl502_6
| ~ spl502_69
| ~ spl502_104 ),
inference(sat_conversion,[],[f6302]) ).
cnf(s115,plain,
( ~ spl502_5
| spl502_74 ),
inference(rat,[],[s58,s96,s97,s92]) ).
cnf(s120,plain,
spl502_5,
inference(rat,[],[s111,s106,s104,s107,s74,s3,s79,s105,s57,s52,s97,s96,s92]) ).
cnf(s121,plain,
spl502_74,
inference(rat,[],[s115,s120]) ).
cnf(s122,plain,
~ spl502_6,
inference(rat,[],[s4,s120]) ).
cnf(s123,plain,
~ spl502_104,
inference(rat,[],[s113,s57,s122]) ).
cnf(s124,plain,
spl502_103,
inference(rat,[],[s108,s57,s122]) ).
cnf(s125,plain,
spl502_77,
inference(rat,[],[s64,s57,s122]) ).
cnf(s126,plain,
spl502_78,
inference(rat,[],[s103,s125]) ).
cnf(s127,plain,
~ spl502_90,
inference(rat,[],[s109,s123,s52,s57,s125]) ).
cnf(s128,plain,
spl502_89,
inference(rat,[],[s99,s124,s121,s126]) ).
cnf(s129,plain,
$false,
inference(rat,[],[s82,s127,s128,s126]) ).
fof(f6303,plain,
$false,
inference(avatar_sat_refutation,[],[s129]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU347+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n002.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 04:52:07 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 10.23/3.52 % (4154770)Detected formulas, will run a generic FOF schedule.
% 10.23/3.52 % (4154826)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1387724363:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.23/3.52 % (4154828)dis-21_1_sil=8000:lcm=predicate:random_seed=949051004: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)
% 10.23/3.52 % (4154826)Instruction limit reached!
% 10.23/3.52 % (4154826)------------------------------
% 10.23/3.52 % (4154826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154826)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154826)Termination reason: Instruction limit
% 10.23/3.52 % (4154826)Termination phase: Saturation
% 10.23/3.52 % (4154826)Time elapsed: 0.052 s
% 10.23/3.52 % (4154826)Peak memory usage: 91 MB
% 10.23/3.52 % (4154826)Instructions burned: 120 (million)
% 10.23/3.52 % (4154823)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=210143823:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.23/3.52 % (4154824)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=1189013151:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.23/3.52 % (4154822)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=531214731:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.23/3.52 % (4154827)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=465741649:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.23/3.52 % (4154825)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1851790004:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.23/3.52 % (4154828)Instruction limit reached!
% 10.23/3.52 % (4154828)------------------------------
% 10.23/3.52 % (4154828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154828)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154828)Termination reason: Instruction limit
% 10.23/3.52 % (4154828)Termination phase: Saturation
% 10.23/3.52 % (4154828)Time elapsed: 0.118 s
% 10.23/3.52 % (4154828)Peak memory usage: 91 MB
% 10.23/3.52 % (4154828)Instructions burned: 130 (million)
% 10.23/3.52 % (4154825)Instruction limit reached!
% 10.23/3.52 % (4154825)------------------------------
% 10.23/3.52 % (4154825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154825)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154825)Termination reason: Instruction limit
% 10.23/3.52 % (4154825)Termination phase: Saturation
% 10.23/3.52 % (4154825)Time elapsed: 0.086 s
% 10.23/3.52 % (4154825)Peak memory usage: 91 MB
% 10.23/3.52 % (4154825)Instructions burned: 110 (million)
% 10.23/3.52 % (4154827)Instruction limit reached!
% 10.23/3.52 % (4154827)------------------------------
% 10.23/3.52 % (4154827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154827)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154827)Termination reason: Instruction limit
% 10.23/3.52 % (4154827)Termination phase: Saturation
% 10.23/3.52 % (4154827)Time elapsed: 0.145 s
% 10.23/3.52 % (4154827)Peak memory usage: 92 MB
% 10.23/3.52 % (4154827)Instructions burned: 140 (million)
% 10.23/3.52 % (4154840)lrs+10_1_sil=8000:sp=occurrence:random_seed=2660052452:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.23/3.52 % (4154846)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2348529508:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.23/3.52 % (4154840)Instruction limit reached!
% 10.23/3.52 % (4154840)------------------------------
% 10.23/3.52 % (4154840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154840)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154840)Termination reason: Instruction limit
% 10.23/3.52 % (4154840)Termination phase: Saturation
% 10.23/3.52 % (4154840)Time elapsed: 0.163 s
% 10.23/3.52 % (4154840)Peak memory usage: 95 MB
% 10.23/3.52 % (4154840)Instructions burned: 287 (million)
% 10.23/3.52 % (4154846)Refutation not found, incomplete strategy
% 10.23/3.52 % (4154846)------------------------------
% 10.23/3.52 % (4154846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154846)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154846)Termination reason: Refutation not found, incomplete strategy
% 10.23/3.52 % (4154846)Time elapsed: 0.030 s
% 10.23/3.52 % (4154846)Peak memory usage: 90 MB
% 10.23/3.52 % (4154846)Instructions burned: 25 (million)
% 10.23/3.52 % (4154847)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2438179491:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 10.23/3.52 % (4154848)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=270879020:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.23/3.52 % (4154852)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2529174654:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.23/3.52 % (4154848)Instruction limit reached!
% 10.23/3.52 % (4154848)------------------------------
% 10.23/3.52 % (4154848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154848)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154848)Termination reason: Instruction limit
% 10.23/3.52 % (4154848)Termination phase: Saturation
% 10.23/3.52 % (4154848)Time elapsed: 0.234 s
% 10.23/3.52 % (4154848)Peak memory usage: 94 MB
% 10.23/3.52 % (4154848)Instructions burned: 248 (million)
% 10.23/3.52 % (4154852)Instruction limit reached!
% 10.23/3.52 % (4154852)------------------------------
% 10.23/3.52 % (4154852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154852)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154852)Termination reason: Instruction limit
% 10.23/3.52 % (4154852)Termination phase: Saturation
% 10.23/3.52 % (4154852)Time elapsed: 0.163 s
% 10.23/3.52 % (4154852)Peak memory usage: 93 MB
% 10.23/3.52 % (4154852)Instructions burned: 296 (million)
% 10.23/3.52 % (4154846)------------------------------
% 10.23/3.52 % (4154846)------------------------------
% 10.23/3.52 % (4154847)Instruction limit reached!
% 10.23/3.52 % (4154847)------------------------------
% 10.23/3.52 % (4154847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154847)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154847)Termination reason: Instruction limit
% 10.23/3.52 % (4154847)Termination phase: Saturation
% 10.23/3.52 % (4154847)Time elapsed: 0.369 s
% 10.23/3.52 % (4154847)Peak memory usage: 95 MB
% 10.23/3.52 % (4154847)Instructions burned: 325 (million)
% 10.23/3.52 % (4154862)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=761959806:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 10.23/3.52 % (4154861)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2911455227:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 10.23/3.52 % (4154862)Instruction limit reached!
% 10.23/3.52 % (4154862)------------------------------
% 10.23/3.52 % (4154862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154862)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154862)Termination reason: Instruction limit
% 10.23/3.52 % (4154862)Termination phase: Saturation
% 10.23/3.52 % (4154862)Time elapsed: 0.039 s
% 10.23/3.52 % (4154862)Peak memory usage: 92 MB
% 10.23/3.52 % (4154862)Instructions burned: 115 (million)
% 10.23/3.52 % (4154864)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1810003416:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 10.23/3.52 % (4154863)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1917334541:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 10.23/3.52 % (4154869)lrs+10_1_sil=8000:sp=occurrence:random_seed=2790419859:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 10.23/3.52 % (4154864)Instruction limit reached!
% 10.23/3.52 % (4154864)------------------------------
% 10.23/3.52 % (4154864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154864)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154864)Termination reason: Instruction limit
% 10.23/3.52 % (4154864)Termination phase: Saturation
% 10.23/3.52 % (4154864)Time elapsed: 0.113 s
% 10.23/3.52 % (4154864)Peak memory usage: 90 MB
% 10.23/3.52 % (4154864)Instructions burned: 115 (million)
% 10.23/3.52 % (4154863)Instruction limit reached!
% 10.23/3.52 % (4154863)------------------------------
% 10.23/3.52 % (4154863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154863)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154863)Termination reason: Instruction limit
% 10.23/3.52 % (4154863)Termination phase: Saturation
% 10.23/3.52 % (4154863)Time elapsed: 0.124 s
% 10.23/3.52 % (4154863)Peak memory usage: 91 MB
% 10.23/3.52 % (4154863)Instructions burned: 130 (million)
% 10.23/3.52 % (4154877)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1661690406:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 10.23/3.52 % (4154878)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1819110711:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 10.23/3.52 % (4154869)Instruction limit reached!
% 10.23/3.52 % (4154869)------------------------------
% 10.23/3.52 % (4154869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154869)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154869)Termination reason: Instruction limit
% 10.23/3.52 % (4154869)Termination phase: Saturation
% 10.23/3.52 % (4154869)Time elapsed: 0.499 s
% 10.23/3.52 % (4154869)Peak memory usage: 105 MB
% 10.23/3.52 % (4154869)Instructions burned: 908 (million)
% 10.23/3.52 % (4154877)Instruction limit reached!
% 10.23/3.52 % (4154877)------------------------------
% 10.23/3.52 % (4154877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154877)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154877)Termination reason: Instruction limit
% 10.23/3.52 % (4154877)Termination phase: Saturation
% 10.23/3.52 % (4154877)Time elapsed: 0.429 s
% 10.23/3.52 % (4154877)Peak memory usage: 95 MB
% 10.23/3.52 % (4154877)Instructions burned: 437 (million)
% 10.23/3.52 % (4154885)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3652248868:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 10.23/3.52 % (4154822)First to succeed.
% 10.23/3.52 % (4154885)Instruction limit reached!
% 10.23/3.52 % (4154885)------------------------------
% 10.23/3.52 % (4154885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/3.52 % (4154885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/3.52 % (4154885)CaDiCaL version: 2.1.3
% 10.23/3.52 % (4154885)Termination reason: Instruction limit
% 10.23/3.52 % (4154885)Termination phase: Saturation
% 10.23/3.52 % (4154885)Time elapsed: 0.065 s
% 10.23/3.52 % (4154885)Peak memory usage: 92 MB
% 10.23/3.52 % (4154885)Instructions burned: 135 (million)
% 10.23/3.52 % (4154822)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4154770"
% 10.23/3.52 % (4154823)Also succeeded, but the first one will report.
% 10.23/3.52 % (4154886)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2074989488:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 10.23/3.52 % (4154890)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=264494207:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 10.23/3.52 % (4154822)Refutation found. Thanks to Tanya!
% 10.23/3.52 % SZS status Theorem for theBenchmark
% 10.23/3.52 % SZS output start Proof for theBenchmark
% See solution above
% 19.07/3.73 % (4154822)------------------------------
% 19.07/3.73 % (4154822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.07/3.73 % (4154822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.07/3.73 % (4154822)CaDiCaL version: 2.1.3
% 19.07/3.73 % (4154822)Termination reason: Refutation
% 19.07/3.73 % (4154822)Time elapsed: 1.911 s
% 19.07/3.73 % (4154822)Peak memory usage: 154 MB
% 19.07/3.73 % (4154822)Instructions burned: 1827 (million)
% 19.07/3.73 % (4154822)------------------------------
% 19.07/3.73 % (4154822)------------------------------
% 19.07/3.73 % (4154770)Success in time 2.647 s
% 19.07/3.73 % Vampire exiting
%------------------------------------------------------------------------------