%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU346+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:52:57 PM UTC 2026
% Result : Theorem 70.77s 10.60s
% Output : Refutation 71.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 47
% Syntax : Number of formulae : 371 ( 47 unt; 18 def)
% Number of atoms : 1392 ( 91 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1730 ( 709 ~; 815 |; 138 &)
% ( 29 <=>; 37 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 19 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 3 con; 0-4 aty)
% Number of variables : 338 ( 0 sgn 323 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( rel_str(X0)
=> ( strict_rel_str(X0)
=> X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v1_orders_2) ).
fof(f4,axiom,
! [X0] :
( latt_str(X0)
=> ( ( ~ empty_carrier(X0)
& lattice(X0) )
=> ( ~ empty_carrier(X0)
& join_commutative(X0)
& join_associative(X0)
& meet_commutative(X0)
& meet_associative(X0)
& meet_absorbing(X0)
& join_absorbing(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f7,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f8,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> poset_of_lattice(X0) = rel_str_of(the_carrier(X0),k2_lattice3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattice3) ).
fof(f9,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(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f11,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( related(X0,X1,X2)
<=> in(ordered_pair(X1,X2),the_InternalRel(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_orders_2) ).
fof(f19,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ( reflexive(k2_lattice3(X0))
& antisymmetric(k2_lattice3(X0))
& transitive(k2_lattice3(X0))
& v1_partfun1(k2_lattice3(X0),the_carrier(X0),the_carrier(X0))
& relation_of2_as_subset(k2_lattice3(X0),the_carrier(X0),the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_lattice3) ).
fof(f22,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(f23,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(f27,axiom,
! [X0] :
( meet_semilatt_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_lattices) ).
fof(f31,axiom,
! [X0] :
( latt_str(X0)
=> ( meet_semilatt_str(X0)
& join_semilatt_str(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f45,axiom,
! [X0] :
? [X1] : element(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f48,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f59,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(f62,axiom,
! [X0,X1] :
( relation_of2(X1,X0,X0)
=> ! [X2,X3] :
( rel_str_of(X0,X1) = rel_str_of(X2,X3)
=> ( X0 = X2
& X1 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g1_orders_2) ).
fof(f65,axiom,
! [X0] :
( ~ empty(X0)
=> ? [X1] :
( element(X1,powerset(X0))
& ~ empty(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(f75,axiom,
! [X0,X1,X2,X3] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0)
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1)
& element(X2,the_carrier(X0))
& element(X3,the_carrier(X1)) )
=> k10_filter_1(X0,X1,X2,X3) = ordered_pair(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k10_filter_1) ).
fof(f76,axiom,
! [X0,X1,X2,X3] :
( ( ~ empty(X0)
& ~ empty(X1)
& element(X2,X0)
& element(X3,X1) )
=> ordered_pair_as_product_element(X0,X1,X2,X3) = ordered_pair(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_domain_1) ).
fof(f77,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> k2_lattice3(X0) = relation_of_lattice(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_lattice3) ).
fof(f78,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
<=> relation_of2(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f80,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(f82,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,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r3_lattices) ).
fof(f84,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f85,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f86,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
<=> below_refl(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_filter_1) ).
fof(f88,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f91,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f92,conjecture,
! [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(f93,negated_conjecture,
~ ! [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)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f92]) ).
fof(f108,plain,
! [X0] :
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f109,plain,
! [X0] :
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f108]) ).
fof(f113,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,[],[f4]) ).
fof(f114,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,[],[f113]) ).
fof(f117,plain,
! [X0] :
( poset_of_lattice(X0) = rel_str_of(the_carrier(X0),k2_lattice3(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f118,plain,
! [X0] :
( poset_of_lattice(X0) = rel_str_of(the_carrier(X0),k2_lattice3(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f117]) ).
fof(f119,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,[],[f9]) ).
fof(f120,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,[],[f119]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( related(X0,X1,X2)
<=> in(ordered_pair(X1,X2),the_InternalRel(X0)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f129,plain,
! [X0] :
( ( reflexive(k2_lattice3(X0))
& antisymmetric(k2_lattice3(X0))
& transitive(k2_lattice3(X0))
& v1_partfun1(k2_lattice3(X0),the_carrier(X0),the_carrier(X0))
& relation_of2_as_subset(k2_lattice3(X0),the_carrier(X0),the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f130,plain,
! [X0] :
( ( reflexive(k2_lattice3(X0))
& antisymmetric(k2_lattice3(X0))
& transitive(k2_lattice3(X0))
& v1_partfun1(k2_lattice3(X0),the_carrier(X0),the_carrier(X0))
& relation_of2_as_subset(k2_lattice3(X0),the_carrier(X0),the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f129]) ).
fof(f131,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,[],[f22]) ).
fof(f132,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,[],[f131]) ).
fof(f133,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,[],[f23]) ).
fof(f134,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,[],[f133]) ).
fof(f137,plain,
! [X0] :
( one_sorted_str(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f140,plain,
! [X0] :
( ( meet_semilatt_str(X0)
& join_semilatt_str(X0) )
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f147,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f148,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f147]) ).
fof(f161,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,[],[f59]) ).
fof(f162,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,[],[f161]) ).
fof(f167,plain,
! [X0,X1] :
( ! [X2,X3] :
( ( X0 = X2
& X1 = X3 )
| rel_str_of(X0,X1) != rel_str_of(X2,X3) )
| ~ relation_of2(X1,X0,X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f170,plain,
! [X0] :
( ? [X1] :
( element(X1,powerset(X0))
& ~ empty(X1) )
| empty(X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( k10_filter_1(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X3,the_carrier(X1)) ),
inference(ennf_transformation,[],[f75]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( k10_filter_1(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X3,the_carrier(X1)) ),
inference(flattening,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ordered_pair_as_product_element(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty(X0)
| empty(X1)
| ~ element(X2,X0)
| ~ element(X3,X1) ),
inference(ennf_transformation,[],[f76]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ordered_pair_as_product_element(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty(X0)
| empty(X1)
| ~ element(X2,X0)
| ~ element(X3,X1) ),
inference(flattening,[],[f175]) ).
fof(f177,plain,
! [X0] :
( k2_lattice3(X0) = relation_of_lattice(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f77]) ).
fof(f178,plain,
! [X0] :
( k2_lattice3(X0) = relation_of_lattice(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f177]) ).
fof(f181,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,[],[f80]) ).
fof(f182,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,[],[f181]) ).
fof(f183,plain,
! [X0,X1,X2] :
( below_refl(X0,X1,X1)
| 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,[],[f82]) ).
fof(f184,plain,
! [X0,X1,X2] :
( below_refl(X0,X1,X1)
| 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,[],[f183]) ).
fof(f187,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f84]) ).
fof(f188,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f85]) ).
fof(f189,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f188]) ).
fof(f190,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
<=> below_refl(X0,X1,X2) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f86]) ).
fof(f191,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
<=> below_refl(X0,X1,X2) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f190]) ).
fof(f193,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f88]) ).
fof(f194,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f193]) ).
fof(f197,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f91]) ).
fof(f198,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,[],[f93]) ).
fof(f199,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,[],[f198]) ).
fof(f201,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( related(X0,X1,X2)
| ~ in(ordered_pair(X1,X2),the_InternalRel(X0)) )
& ( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f121]) ).
fof(f208,plain,
! [X0] : element(sK6(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X1,sK6(X0))],[f45]) ).
fof(f211,plain,
! [X0] :
( ( element(sK9(X0),powerset(X0))
& ~ empty(sK9(X0)) )
| empty(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X1,sK9(X0))],[f170]) ).
fof(f221,plain,
! [X0,X1,X2] :
( ( relation_of2_as_subset(X2,X0,X1)
| ~ relation_of2(X2,X0,X1) )
& ( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f78]) ).
fof(f223,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,[],[f182]) ).
fof(f224,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
| ~ below_refl(X0,X1,X2) )
& ( below_refl(X0,X1,X2)
| ~ in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0)) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f191]) ).
fof(f225,plain,
? [X0] :
( ? [X1] :
( ? [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) )
& ( 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,[],[f199]) ).
fof(f226,plain,
? [X0] :
( ? [X1] :
( ? [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) )
& ( 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(flattening,[],[f225]) ).
fof(f227,plain,
( ( ~ related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| ~ below_refl(sK19,sK20,sK21) )
& ( related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| below_refl(sK19,sK20,sK21) )
& element(sK21,the_carrier(sK19))
& element(sK20,the_carrier(sK19))
& ~ empty_carrier(sK19)
& lattice(sK19)
& latt_str(sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21]),skolemize(X0,sK19),skolemize(X1,sK20),skolemize(X2,sK21)],[f226]) ).
fof(f228,plain,
! [X0] :
( ~ strict_rel_str(X0)
| rel_str_of(the_carrier(X0),the_InternalRel(X0)) = X0
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f109]) ).
fof(f231,plain,
! [X0] :
( join_absorbing(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f232,plain,
! [X0] :
( meet_absorbing(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f234,plain,
! [X0] :
( meet_commutative(X0)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f240,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f7]) ).
fof(f241,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| poset_of_lattice(X0) = rel_str_of(the_carrier(X0),k2_lattice3(X0))
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f242,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,[],[f120]) ).
fof(f243,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f244,plain,
! [X2,X0,X1] :
( in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f245,plain,
! [X2,X0,X1] :
( related(X0,X1,X2)
| ~ in(ordered_pair(X1,X2),the_InternalRel(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f201]) ).
fof(f252,plain,
! [X0] :
( relation_of2_as_subset(k2_lattice3(X0),the_carrier(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f257,plain,
! [X0] :
( rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f260,plain,
! [X0] :
( reflexive_relstr(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f261,plain,
! [X0] :
( strict_rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f262,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,[],[f134]) ).
fof(f265,plain,
! [X0] :
( one_sorted_str(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f269,plain,
! [X0] :
( meet_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f284,plain,
! [X0] : element(sK6(X0),X0),
inference(cnf_transformation,[],[f208]) ).
fof(f288,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f316,plain,
! [X0] :
( ~ empty_carrier(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f162]) ).
fof(f321,plain,
! [X2,X3,X0,X1] :
( ~ relation_of2(X1,X0,X0)
| rel_str_of(X0,X1) != rel_str_of(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f167]) ).
fof(f328,plain,
! [X0] :
( ~ empty(sK9(X0))
| empty(X0) ),
inference(cnf_transformation,[],[f211]) ).
fof(f329,plain,
! [X0] :
( element(sK9(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[],[f211]) ).
fof(f359,plain,
! [X2,X3,X0,X1] :
( k10_filter_1(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X3,the_carrier(X1)) ),
inference(cnf_transformation,[],[f174]) ).
fof(f360,plain,
! [X2,X3,X0,X1] :
( ordered_pair_as_product_element(X0,X1,X2,X3) = ordered_pair(X2,X3)
| empty(X0)
| empty(X1)
| ~ element(X2,X0)
| ~ element(X3,X1) ),
inference(cnf_transformation,[],[f176]) ).
fof(f361,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| k2_lattice3(X0) = relation_of_lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f178]) ).
fof(f362,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f221]) ).
fof(f366,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,[],[f223]) ).
fof(f367,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,[],[f223]) ).
fof(f369,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| below_refl(X0,X1,X1) ),
inference(cnf_transformation,[],[f184]) ).
fof(f371,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f187]) ).
fof(f372,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[],[f189]) ).
fof(f373,plain,
! [X2,X0,X1] :
( ~ in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
| 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,[],[f224]) ).
fof(f374,plain,
! [X2,X0,X1] :
( in(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
| ~ 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,[],[f224]) ).
fof(f376,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f194]) ).
fof(f379,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f197]) ).
fof(f380,plain,
latt_str(sK19),
inference(cnf_transformation,[],[f227]) ).
fof(f381,plain,
lattice(sK19),
inference(cnf_transformation,[],[f227]) ).
fof(f382,plain,
~ empty_carrier(sK19),
inference(cnf_transformation,[],[f227]) ).
fof(f383,plain,
element(sK20,the_carrier(sK19)),
inference(cnf_transformation,[],[f227]) ).
fof(f384,plain,
element(sK21,the_carrier(sK19)),
inference(cnf_transformation,[],[f227]) ).
fof(f385,plain,
( related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| below_refl(sK19,sK20,sK21) ),
inference(cnf_transformation,[],[f227]) ).
fof(f386,plain,
( ~ related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| ~ below_refl(sK19,sK20,sK21) ),
inference(cnf_transformation,[],[f227]) ).
fof(f388,plain,
! [X2,X0,X1] :
( related(X0,X1,X2)
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),the_InternalRel(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(definition_unfolding,[],[f245,f243]) ).
fof(f389,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(definition_unfolding,[],[f244,f243]) ).
fof(f390,plain,
! [X2,X3,X0,X1] :
( k10_filter_1(X0,X1,X2,X3) = unordered_pair(unordered_pair(X2,X3),singleton(X2))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X0))
| ~ element(X3,the_carrier(X1)) ),
inference(definition_unfolding,[],[f359,f243]) ).
fof(f391,plain,
! [X2,X3,X0,X1] :
( ordered_pair_as_product_element(X0,X1,X2,X3) = unordered_pair(unordered_pair(X2,X3),singleton(X2))
| empty(X0)
| empty(X1)
| ~ element(X2,X0)
| ~ element(X3,X1) ),
inference(definition_unfolding,[],[f360,f243]) ).
fof(f393,definition,
( spl22_1
<=> below_refl(sK19,sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f395,plain,
( below_refl(sK19,sK20,sK21)
| ~ spl22_1 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f397,definition,
( spl22_2
<=> related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21)) ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f398,plain,
( ~ related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| spl22_2 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f399,plain,
( related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),cast_to_el_of_LattPOSet(sK19,sK21))
| ~ spl22_2 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f400,plain,
( spl22_1
| spl22_2 ),
inference(avatar_split_clause,[],[f385,f397,f393]) ).
fof(f401,plain,
( ~ spl22_1
| ~ spl22_2 ),
inference(avatar_split_clause,[],[f386,f397,f393]) ).
fof(f455,plain,
! [X0,X1] :
( ~ in(X0,sK9(X1))
| element(X0,X1)
| empty(X1) ),
inference(resolution,[],[f376,f329]) ).
fof(f463,plain,
! [X0] :
( poset_of_lattice(X0) = rel_str_of(the_carrier(poset_of_lattice(X0)),the_InternalRel(poset_of_lattice(X0)))
| ~ rel_str(poset_of_lattice(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(resolution,[],[f228,f261]) ).
fof(f468,plain,
! [X0] :
( ~ lattice(X0)
| empty_carrier(X0)
| poset_of_lattice(X0) = rel_str_of(the_carrier(poset_of_lattice(X0)),the_InternalRel(poset_of_lattice(X0)))
| ~ latt_str(X0) ),
inference(forward_subsumption_resolution,[],[f463,f257]) ).
fof(f472,plain,
( empty_carrier(sK19)
| k2_lattice3(sK19) = relation_of_lattice(sK19)
| ~ latt_str(sK19) ),
inference(resolution,[],[f361,f381]) ).
fof(f475,plain,
( k2_lattice3(sK19) = relation_of_lattice(sK19)
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f472,f382]) ).
fof(f477,plain,
k2_lattice3(sK19) = relation_of_lattice(sK19),
inference(forward_subsumption_resolution,[],[f475,f380]) ).
fof(f488,plain,
! [X0,X1] :
( element(X0,X1)
| empty(X1)
| empty(sK9(X1))
| ~ element(X0,sK9(X1)) ),
inference(resolution,[],[f455,f372]) ).
fof(f489,plain,
! [X0,X1] :
( ~ element(X0,sK9(X1))
| empty(X1)
| element(X0,X1) ),
inference(forward_subsumption_resolution,[],[f488,f328]) ).
fof(f499,plain,
! [X0] :
( relation_of2(k2_lattice3(X0),the_carrier(X0),the_carrier(X0))
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X0) ),
inference(resolution,[],[f252,f362]) ).
fof(f500,plain,
( empty_carrier(sK19)
| poset_of_lattice(sK19) = rel_str_of(the_carrier(sK19),k2_lattice3(sK19))
| ~ latt_str(sK19) ),
inference(resolution,[],[f241,f381]) ).
fof(f503,plain,
( poset_of_lattice(sK19) = rel_str_of(the_carrier(sK19),k2_lattice3(sK19))
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f500,f382]) ).
fof(f505,plain,
poset_of_lattice(sK19) = rel_str_of(the_carrier(sK19),k2_lattice3(sK19)),
inference(forward_subsumption_resolution,[],[f503,f380]) ).
fof(f512,plain,
! [X0] :
( element(sK6(sK9(X0)),X0)
| empty(X0) ),
inference(resolution,[],[f489,f284]) ).
fof(f513,plain,
( sK20 = cast_to_el_of_LattPOSet(sK19,sK20)
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19) ),
inference(resolution,[],[f242,f383]) ).
fof(f514,plain,
( sK21 = cast_to_el_of_LattPOSet(sK19,sK21)
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19) ),
inference(resolution,[],[f242,f384]) ).
fof(f516,plain,
( sK21 = cast_to_el_of_LattPOSet(sK19,sK21)
| ~ lattice(sK19)
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f514,f382]) ).
fof(f517,plain,
( sK20 = cast_to_el_of_LattPOSet(sK19,sK20)
| ~ lattice(sK19)
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f513,f382]) ).
fof(f518,plain,
( sK21 = cast_to_el_of_LattPOSet(sK19,sK21)
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f516,f381]) ).
fof(f519,plain,
( sK20 = cast_to_el_of_LattPOSet(sK19,sK20)
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f517,f381]) ).
fof(f520,plain,
sK21 = cast_to_el_of_LattPOSet(sK19,sK21),
inference(forward_subsumption_resolution,[],[f518,f380]) ).
fof(f521,plain,
sK20 = cast_to_el_of_LattPOSet(sK19,sK20),
inference(forward_subsumption_resolution,[],[f519,f380]) ).
fof(f551,plain,
( element(sK21,the_carrier(poset_of_lattice(sK19)))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(sK21,the_carrier(sK19)) ),
inference(superposition,[],[f262,f520]) ).
fof(f552,plain,
( element(sK20,the_carrier(poset_of_lattice(sK19)))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(sK20,the_carrier(sK19)) ),
inference(superposition,[],[f262,f521]) ).
fof(f553,plain,
( element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(sK20,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f552,f382]) ).
fof(f554,plain,
( element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(sK21,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f551,f382]) ).
fof(f556,plain,
( element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ latt_str(sK19)
| ~ element(sK20,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f553,f381]) ).
fof(f557,plain,
( element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ latt_str(sK19)
| ~ element(sK21,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f554,f381]) ).
fof(f558,plain,
( element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK20,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f556,f380]) ).
fof(f559,plain,
( element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(sK19)) ),
inference(forward_subsumption_resolution,[],[f557,f380]) ).
fof(f560,plain,
element(sK20,the_carrier(poset_of_lattice(sK19))),
inference(forward_subsumption_resolution,[],[f558,f383]) ).
fof(f561,plain,
element(sK21,the_carrier(poset_of_lattice(sK19))),
inference(forward_subsumption_resolution,[],[f559,f384]) ).
fof(f572,definition,
( spl22_7
<=> empty_carrier(poset_of_lattice(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f573,plain,
( ~ empty_carrier(poset_of_lattice(sK19))
| spl22_7 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f574,plain,
( empty_carrier(poset_of_lattice(sK19))
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f603,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ spl22_7 ),
inference(resolution,[],[f574,f316]) ).
fof(f604,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f603,f382]) ).
fof(f605,plain,
( ~ latt_str(sK19)
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f604,f381]) ).
fof(f606,plain,
( $false
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f605,f380]) ).
fof(f607,plain,
~ spl22_7,
inference(avatar_contradiction_clause,[],[f606]) ).
fof(f639,definition,
( spl22_12
<=> rel_str(poset_of_lattice(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f640,plain,
( rel_str(poset_of_lattice(sK19))
| ~ spl22_12 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f641,plain,
( ~ rel_str(poset_of_lattice(sK19))
| spl22_12 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,definition,
( spl22_13
<=> reflexive_relstr(poset_of_lattice(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f644,plain,
( reflexive_relstr(poset_of_lattice(sK19))
| ~ spl22_13 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( ~ reflexive_relstr(poset_of_lattice(sK19))
| spl22_13 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f665,plain,
! [X0] :
( empty_carrier(sK19)
| ~ meet_commutative(sK19)
| ~ meet_absorbing(sK19)
| ~ join_absorbing(sK19)
| ~ latt_str(sK19)
| ~ element(X0,the_carrier(sK19))
| below_refl(sK19,X0,X0) ),
inference(resolution,[],[f369,f383]) ).
fof(f678,plain,
! [X0] :
( ~ meet_commutative(sK19)
| ~ meet_absorbing(sK19)
| ~ join_absorbing(sK19)
| ~ latt_str(sK19)
| ~ element(X0,the_carrier(sK19))
| below_refl(sK19,X0,X0) ),
inference(forward_subsumption_resolution,[],[f665,f382]) ).
fof(f682,plain,
! [X0] :
( ~ meet_commutative(sK19)
| ~ meet_absorbing(sK19)
| ~ join_absorbing(sK19)
| ~ element(X0,the_carrier(sK19))
| below_refl(sK19,X0,X0) ),
inference(forward_subsumption_resolution,[],[f678,f380]) ).
fof(f701,definition,
( spl22_21
<=> ! [X0] :
( ~ element(X0,the_carrier(sK19))
| below_refl(sK19,X0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f702,plain,
( ! [X0] :
( below_refl(sK19,X0,X0)
| ~ element(X0,the_carrier(sK19)) )
| ~ spl22_21 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f704,definition,
( spl22_22
<=> join_absorbing(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f706,plain,
( ~ join_absorbing(sK19)
| spl22_22 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f708,definition,
( spl22_23
<=> meet_absorbing(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition]) ).
fof(f710,plain,
( ~ meet_absorbing(sK19)
| spl22_23 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f712,definition,
( spl22_24
<=> meet_commutative(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f714,plain,
( ~ meet_commutative(sK19)
| spl22_24 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f716,plain,
( spl22_21
| ~ spl22_22
| ~ spl22_23
| ~ spl22_24 ),
inference(avatar_split_clause,[],[f682,f712,f708,f704,f701]) ).
fof(f718,plain,
! [X2,X3,X0,X1] :
( ~ element(X3,X1)
| empty(X0)
| empty(X1)
| ~ element(X2,X0)
| ordered_pair_as_product_element(X0,X1,X2,X3) = unordered_pair(singleton(X2),unordered_pair(X2,X3)) ),
inference(forward_demodulation,[],[f391,f240]) ).
fof(f724,plain,
! [X0,X1] :
( empty(X0)
| empty(the_carrier(sK19))
| ~ element(X1,X0)
| ordered_pair_as_product_element(X0,the_carrier(sK19),X1,sK21) = unordered_pair(singleton(X1),unordered_pair(X1,sK21)) ),
inference(resolution,[],[f718,f384]) ).
fof(f758,definition,
( spl22_28
<=> empty(the_carrier(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f759,plain,
( ~ empty(the_carrier(sK19))
| spl22_28 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f760,plain,
( empty(the_carrier(sK19))
| ~ spl22_28 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f762,definition,
( spl22_29
<=> ! [X0,X1] :
( empty(X0)
| ordered_pair_as_product_element(X0,the_carrier(sK19),X1,sK21) = unordered_pair(singleton(X1),unordered_pair(X1,sK21))
| ~ element(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f763,plain,
( ! [X0,X1] :
( ~ element(X1,X0)
| ordered_pair_as_product_element(X0,the_carrier(sK19),X1,sK21) = unordered_pair(singleton(X1),unordered_pair(X1,sK21))
| empty(X0) )
| ~ spl22_29 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f764,plain,
( spl22_28
| spl22_29 ),
inference(avatar_split_clause,[],[f724,f762,f758]) ).
fof(f770,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),the_InternalRel(X0))
| related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(forward_demodulation,[],[f388,f240]) ).
fof(f771,plain,
( empty_carrier(sK19)
| ~ one_sorted_str(sK19)
| ~ spl22_28 ),
inference(resolution,[],[f760,f288]) ).
fof(f774,plain,
( ~ one_sorted_str(sK19)
| ~ spl22_28 ),
inference(forward_subsumption_resolution,[],[f771,f382]) ).
fof(f775,plain,
! [X2,X0,X1] :
( in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),the_InternalRel(X0))
| ~ related(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0) ),
inference(forward_demodulation,[],[f389,f240]) ).
fof(f778,plain,
( ~ meet_semilatt_str(sK19)
| ~ spl22_28 ),
inference(resolution,[],[f774,f265]) ).
fof(f781,plain,
! [X2,X0,X1] :
( ~ element(unordered_pair(singleton(X1),unordered_pair(X1,X2)),the_InternalRel(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| empty(the_InternalRel(X0))
| related(X0,X1,X2) ),
inference(resolution,[],[f770,f372]) ).
fof(f811,plain,
! [X2,X0,X1] :
( element(ordered_pair_as_product_element(the_carrier(X0),the_carrier(X0),X1,X2),relation_of_lattice(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ below_refl(X0,X1,X2) ),
inference(resolution,[],[f374,f371]) ).
fof(f813,plain,
! [X2,X0,X1] :
( ~ below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ empty(relation_of_lattice(X0)) ),
inference(resolution,[],[f374,f379]) ).
fof(f834,plain,
! [X2,X3,X0,X1] :
( ~ element(X3,the_carrier(X1))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X0))
| k10_filter_1(X0,X1,X2,X3) = unordered_pair(singleton(X2),unordered_pair(X2,X3)) ),
inference(forward_demodulation,[],[f390,f240]) ).
fof(f841,plain,
! [X0,X1] :
( empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(X1,the_carrier(X0))
| unordered_pair(singleton(X1),unordered_pair(X1,sK21)) = k10_filter_1(X0,sK19,X1,sK21) ),
inference(resolution,[],[f834,f384]) ).
fof(f854,plain,
! [X0,X1] :
( empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ element(X1,the_carrier(X0))
| unordered_pair(singleton(X1),unordered_pair(X1,sK21)) = k10_filter_1(X0,sK19,X1,sK21) ),
inference(forward_subsumption_resolution,[],[f841,f382]) ).
fof(f858,plain,
! [X0,X1] :
( empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ latt_str(sK19)
| ~ element(X1,the_carrier(X0))
| unordered_pair(singleton(X1),unordered_pair(X1,sK21)) = k10_filter_1(X0,sK19,X1,sK21) ),
inference(forward_subsumption_resolution,[],[f854,f381]) ).
fof(f862,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(X0))
| ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| unordered_pair(singleton(X1),unordered_pair(X1,sK21)) = k10_filter_1(X0,sK19,X1,sK21) ),
inference(forward_subsumption_resolution,[],[f858,f380]) ).
fof(f1090,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = unordered_pair(singleton(sK20),unordered_pair(sK20,sK21))
| empty(the_carrier(sK19))
| ~ spl22_29 ),
inference(resolution,[],[f763,f383]) ).
fof(f1124,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = unordered_pair(singleton(sK20),unordered_pair(sK20,sK21))
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f1090,f759]) ).
fof(f1190,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| empty_carrier(sK19)
| unordered_pair(singleton(sK20),unordered_pair(sK20,sK21)) = k10_filter_1(sK19,sK19,sK20,sK21) ),
inference(resolution,[],[f862,f383]) ).
fof(f1211,plain,
( ~ latt_str(sK19)
| empty_carrier(sK19)
| unordered_pair(singleton(sK20),unordered_pair(sK20,sK21)) = k10_filter_1(sK19,sK19,sK20,sK21) ),
inference(forward_subsumption_resolution,[],[f1190,f381]) ).
fof(f1218,plain,
( empty_carrier(sK19)
| unordered_pair(singleton(sK20),unordered_pair(sK20,sK21)) = k10_filter_1(sK19,sK19,sK20,sK21) ),
inference(forward_subsumption_resolution,[],[f1211,f380]) ).
fof(f1223,plain,
unordered_pair(singleton(sK20),unordered_pair(sK20,sK21)) = k10_filter_1(sK19,sK19,sK20,sK21),
inference(forward_subsumption_resolution,[],[f1218,f382]) ).
fof(f1361,plain,
! [X2,X0,X1] :
( ~ lattice(X0)
| ~ latt_str(X0)
| empty_carrier(X0)
| rel_str_of(the_carrier(X0),k2_lattice3(X0)) != rel_str_of(X1,X2)
| k2_lattice3(X0) = X2 ),
inference(resolution,[],[f499,f321]) ).
fof(f1502,plain,
( empty_carrier(sK19)
| poset_of_lattice(sK19) = rel_str_of(the_carrier(poset_of_lattice(sK19)),the_InternalRel(poset_of_lattice(sK19)))
| ~ latt_str(sK19) ),
inference(resolution,[],[f468,f381]) ).
fof(f1511,plain,
( poset_of_lattice(sK19) = rel_str_of(the_carrier(poset_of_lattice(sK19)),the_InternalRel(poset_of_lattice(sK19)))
| ~ latt_str(sK19) ),
inference(forward_subsumption_resolution,[],[f1502,f382]) ).
fof(f1516,plain,
poset_of_lattice(sK19) = rel_str_of(the_carrier(poset_of_lattice(sK19)),the_InternalRel(poset_of_lattice(sK19))),
inference(forward_subsumption_resolution,[],[f1511,f380]) ).
fof(f1613,definition,
( spl22_100
<=> ! [X0] : ~ element(X0,the_carrier(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_100])],[avatar_definition]) ).
fof(f1614,plain,
( ! [X0] : ~ element(X0,the_carrier(sK19))
| ~ spl22_100 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1641,plain,
( empty(the_carrier(sK19))
| ~ spl22_100 ),
inference(resolution,[],[f1614,f512]) ).
fof(f1651,plain,
( $false
| spl22_28
| ~ spl22_100 ),
inference(forward_subsumption_resolution,[],[f1641,f759]) ).
fof(f1652,plain,
( spl22_28
| ~ spl22_100 ),
inference(avatar_contradiction_clause,[],[f1651]) ).
fof(f1692,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK19))
| ~ element(X0,the_carrier(sK19))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ empty(relation_of_lattice(sK19))
| ~ element(X0,the_carrier(sK19)) )
| ~ spl22_21 ),
inference(resolution,[],[f813,f702]) ).
fof(f1695,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK19))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ empty(relation_of_lattice(sK19)) )
| ~ spl22_21 ),
inference(duplicate_literal_removal,[],[f1692]) ).
fof(f1697,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK19))
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ empty(relation_of_lattice(sK19)) )
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f1695,f382]) ).
fof(f1700,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK19))
| ~ latt_str(sK19)
| ~ empty(relation_of_lattice(sK19)) )
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f1697,f381]) ).
fof(f1703,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK19))
| ~ empty(relation_of_lattice(sK19)) )
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f1700,f380]) ).
fof(f1705,plain,
( ! [X0] :
( ~ empty(k2_lattice3(sK19))
| ~ element(X0,the_carrier(sK19)) )
| ~ spl22_21 ),
inference(forward_demodulation,[],[f1703,f477]) ).
fof(f1708,definition,
( spl22_106
<=> empty(k2_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_106])],[avatar_definition]) ).
fof(f1710,plain,
( ~ empty(k2_lattice3(sK19))
| spl22_106 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1711,plain,
( spl22_100
| ~ spl22_106
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f1705,f701,f1708,f1613]) ).
fof(f2098,plain,
! [X0,X1] :
( element(ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),X0,X1),k2_lattice3(sK19))
| ~ element(X1,the_carrier(sK19))
| ~ element(X0,the_carrier(sK19))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ below_refl(sK19,X0,X1) ),
inference(superposition,[],[f811,f477]) ).
fof(f2103,plain,
! [X0,X1] :
( element(ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),X0,X1),k2_lattice3(sK19))
| ~ element(X1,the_carrier(sK19))
| ~ element(X0,the_carrier(sK19))
| ~ lattice(sK19)
| ~ latt_str(sK19)
| ~ below_refl(sK19,X0,X1) ),
inference(forward_subsumption_resolution,[],[f2098,f382]) ).
fof(f2113,plain,
! [X0,X1] :
( element(ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),X0,X1),k2_lattice3(sK19))
| ~ element(X1,the_carrier(sK19))
| ~ element(X0,the_carrier(sK19))
| ~ latt_str(sK19)
| ~ below_refl(sK19,X0,X1) ),
inference(forward_subsumption_resolution,[],[f2103,f381]) ).
fof(f2119,plain,
! [X0,X1] :
( element(ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),X0,X1),k2_lattice3(sK19))
| ~ element(X1,the_carrier(sK19))
| ~ element(X0,the_carrier(sK19))
| ~ below_refl(sK19,X0,X1) ),
inference(forward_subsumption_resolution,[],[f2113,f380]) ).
fof(f2726,plain,
! [X0] :
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),the_InternalRel(X0))
| ~ element(sK21,the_carrier(X0))
| ~ element(sK20,the_carrier(X0))
| ~ rel_str(X0)
| empty(the_InternalRel(X0))
| related(X0,sK20,sK21) ),
inference(superposition,[],[f781,f1223]) ).
fof(f2729,plain,
! [X0] :
( in(k10_filter_1(sK19,sK19,sK20,sK21),the_InternalRel(X0))
| ~ related(X0,sK20,sK21)
| ~ element(sK21,the_carrier(X0))
| ~ element(sK20,the_carrier(X0))
| ~ rel_str(X0) ),
inference(superposition,[],[f775,f1223]) ).
fof(f2951,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = k10_filter_1(sK19,sK19,sK20,sK21)
| spl22_28
| ~ spl22_29 ),
inference(forward_demodulation,[],[f1124,f1223]) ).
fof(f2956,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| ~ element(sK21,the_carrier(sK19))
| ~ element(sK20,the_carrier(sK19))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_28
| ~ spl22_29 ),
inference(superposition,[],[f373,f2951]) ).
fof(f7494,plain,
! [X0,X1] :
( ~ latt_str(sK19)
| empty_carrier(sK19)
| rel_str_of(X0,X1) != rel_str_of(the_carrier(sK19),k2_lattice3(sK19))
| k2_lattice3(sK19) = X1 ),
inference(resolution,[],[f1361,f381]) ).
fof(f7495,plain,
! [X0,X1] :
( empty_carrier(sK19)
| rel_str_of(X0,X1) != rel_str_of(the_carrier(sK19),k2_lattice3(sK19))
| k2_lattice3(sK19) = X1 ),
inference(forward_subsumption_resolution,[],[f7494,f380]) ).
fof(f7503,plain,
! [X0,X1] :
( rel_str_of(X0,X1) != rel_str_of(the_carrier(sK19),k2_lattice3(sK19))
| k2_lattice3(sK19) = X1 ),
inference(forward_subsumption_resolution,[],[f7495,f382]) ).
fof(f7514,plain,
! [X0,X1] :
( rel_str_of(X0,X1) != poset_of_lattice(sK19)
| k2_lattice3(sK19) = X1 ),
inference(forward_demodulation,[],[f7503,f505]) ).
fof(f14440,plain,
( poset_of_lattice(sK19) != poset_of_lattice(sK19)
| k2_lattice3(sK19) = the_InternalRel(poset_of_lattice(sK19)) ),
inference(superposition,[],[f7514,f1516]) ).
fof(f14446,plain,
k2_lattice3(sK19) = the_InternalRel(poset_of_lattice(sK19)),
inference(trivial_inequality_removal,[],[f14440]) ).
fof(f23435,definition,
( spl22_1384
<=> meet_semilatt_str(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_1384])],[avatar_definition]) ).
fof(f23436,plain,
( meet_semilatt_str(sK19)
| ~ spl22_1384 ),
inference(avatar_component_clause,[],[f23435]) ).
fof(f23437,plain,
( ~ meet_semilatt_str(sK19)
| spl22_1384 ),
inference(avatar_component_clause,[],[f23435]) ).
fof(f39806,plain,
( related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),sK21)
| ~ spl22_2 ),
inference(forward_demodulation,[],[f399,f520]) ).
fof(f40403,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| ~ element(sK20,the_carrier(sK19))
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f2956,f384]) ).
fof(f40414,plain,
( related_reflexive(poset_of_lattice(sK19),sK20,sK21)
| ~ spl22_2 ),
inference(forward_demodulation,[],[f39806,f521]) ).
fof(f40718,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f40403,f383]) ).
fof(f40722,definition,
( spl22_2088
<=> element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_2088])],[avatar_definition]) ).
fof(f40830,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f40718,f382]) ).
fof(f40834,definition,
( spl22_2101
<=> in(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19)) ),
introduced(definition,[new_symbols(definition,[spl22_2101])],[avatar_definition]) ).
fof(f40836,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| spl22_2101 ),
inference(avatar_component_clause,[],[f40834]) ).
fof(f40918,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| ~ latt_str(sK19)
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f40830,f381]) ).
fof(f40945,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),relation_of_lattice(sK19))
| below_refl(sK19,sK20,sK21)
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f40918,f380]) ).
fof(f40960,plain,
( ~ in(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| below_refl(sK19,sK20,sK21)
| spl22_28
| ~ spl22_29 ),
inference(forward_demodulation,[],[f40945,f477]) ).
fof(f40978,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_22 ),
inference(resolution,[],[f706,f231]) ).
fof(f40979,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_22 ),
inference(forward_subsumption_resolution,[],[f40978,f382]) ).
fof(f40980,plain,
( ~ latt_str(sK19)
| spl22_22 ),
inference(forward_subsumption_resolution,[],[f40979,f381]) ).
fof(f40981,plain,
( $false
| spl22_22 ),
inference(forward_subsumption_resolution,[],[f40980,f380]) ).
fof(f40982,plain,
spl22_22,
inference(avatar_contradiction_clause,[],[f40981]) ).
fof(f40984,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_23 ),
inference(resolution,[],[f710,f232]) ).
fof(f40985,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_23 ),
inference(forward_subsumption_resolution,[],[f40984,f382]) ).
fof(f40986,plain,
( ~ latt_str(sK19)
| spl22_23 ),
inference(forward_subsumption_resolution,[],[f40985,f381]) ).
fof(f40987,plain,
( $false
| spl22_23 ),
inference(forward_subsumption_resolution,[],[f40986,f380]) ).
fof(f40988,plain,
spl22_23,
inference(avatar_contradiction_clause,[],[f40987]) ).
fof(f40989,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_24 ),
inference(resolution,[],[f714,f234]) ).
fof(f40990,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_24 ),
inference(forward_subsumption_resolution,[],[f40989,f382]) ).
fof(f40991,plain,
( ~ latt_str(sK19)
| spl22_24 ),
inference(forward_subsumption_resolution,[],[f40990,f381]) ).
fof(f40992,plain,
( $false
| spl22_24 ),
inference(forward_subsumption_resolution,[],[f40991,f380]) ).
fof(f40993,plain,
spl22_24,
inference(avatar_contradiction_clause,[],[f40992]) ).
fof(f41597,plain,
( ~ latt_str(sK19)
| spl22_1384 ),
inference(resolution,[],[f23437,f269]) ).
fof(f41598,plain,
( $false
| spl22_1384 ),
inference(forward_subsumption_resolution,[],[f41597,f380]) ).
fof(f41599,plain,
spl22_1384,
inference(avatar_contradiction_clause,[],[f41598]) ).
fof(f41735,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_12 ),
inference(resolution,[],[f641,f257]) ).
fof(f41736,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_12 ),
inference(forward_subsumption_resolution,[],[f41735,f382]) ).
fof(f41737,plain,
( ~ latt_str(sK19)
| spl22_12 ),
inference(forward_subsumption_resolution,[],[f41736,f381]) ).
fof(f41738,plain,
( $false
| spl22_12 ),
inference(forward_subsumption_resolution,[],[f41737,f380]) ).
fof(f41739,plain,
spl22_12,
inference(avatar_contradiction_clause,[],[f41738]) ).
fof(f41763,plain,
( empty_carrier(sK19)
| ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_13 ),
inference(resolution,[],[f645,f260]) ).
fof(f41764,plain,
( ~ lattice(sK19)
| ~ latt_str(sK19)
| spl22_13 ),
inference(forward_subsumption_resolution,[],[f41763,f382]) ).
fof(f41765,plain,
( ~ latt_str(sK19)
| spl22_13 ),
inference(forward_subsumption_resolution,[],[f41764,f381]) ).
fof(f41766,plain,
( $false
| spl22_13 ),
inference(forward_subsumption_resolution,[],[f41765,f380]) ).
fof(f41767,plain,
spl22_13,
inference(avatar_contradiction_clause,[],[f41766]) ).
fof(f50722,plain,
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ rel_str(poset_of_lattice(sK19))
| empty(k2_lattice3(sK19))
| related(poset_of_lattice(sK19),sK20,sK21) ),
inference(superposition,[],[f2726,f14446]) ).
fof(f50725,plain,
( in(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ related(poset_of_lattice(sK19),sK20,sK21)
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ rel_str(poset_of_lattice(sK19)) ),
inference(superposition,[],[f2729,f14446]) ).
fof(f50823,plain,
( ~ related(poset_of_lattice(sK19),sK20,sK21)
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ rel_str(poset_of_lattice(sK19))
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f50725,f40836]) ).
fof(f51075,plain,
( ~ related(poset_of_lattice(sK19),sK20,sK21)
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ rel_str(poset_of_lattice(sK19))
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f50823,f561]) ).
fof(f51143,plain,
( ~ related(poset_of_lattice(sK19),sK20,sK21)
| ~ rel_str(poset_of_lattice(sK19))
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51075,f560]) ).
fof(f51168,plain,
( ~ related(poset_of_lattice(sK19),sK20,sK21)
| ~ spl22_12
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51143,f640]) ).
fof(f51937,plain,
( ~ related_reflexive(poset_of_lattice(sK19),sK20,sK21)
| empty_carrier(poset_of_lattice(sK19))
| ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_12
| spl22_2101 ),
inference(resolution,[],[f51168,f366]) ).
fof(f51938,plain,
( empty_carrier(poset_of_lattice(sK19))
| ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2
| ~ spl22_12
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51937,f40414]) ).
fof(f51939,plain,
( ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2
| spl22_7
| ~ spl22_12
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51938,f573]) ).
fof(f51940,plain,
( ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51939,f644]) ).
fof(f51941,plain,
( ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51940,f640]) ).
fof(f51942,plain,
( ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51941,f560]) ).
fof(f51943,plain,
( $false
| ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(forward_subsumption_resolution,[],[f51942,f561]) ).
fof(f51944,plain,
( ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(avatar_contradiction_clause,[],[f51943]) ).
fof(f51945,plain,
( ~ related_reflexive(poset_of_lattice(sK19),cast_to_el_of_LattPOSet(sK19,sK20),sK21)
| spl22_2 ),
inference(forward_demodulation,[],[f398,f520]) ).
fof(f51946,plain,
( $false
| ~ spl22_28
| ~ spl22_1384 ),
inference(forward_subsumption_resolution,[],[f778,f23436]) ).
fof(f51947,plain,
( ~ spl22_28
| ~ spl22_1384 ),
inference(avatar_contradiction_clause,[],[f51946]) ).
fof(f52235,plain,
( ~ related_reflexive(poset_of_lattice(sK19),sK20,sK21)
| spl22_2 ),
inference(forward_demodulation,[],[f51945,f521]) ).
fof(f52333,plain,
( spl22_1
| ~ spl22_2101
| spl22_28
| ~ spl22_29 ),
inference(avatar_split_clause,[],[f40960,f762,f758,f40834,f393]) ).
fof(f52414,plain,
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ rel_str(poset_of_lattice(sK19))
| empty(k2_lattice3(sK19))
| related(poset_of_lattice(sK19),sK20,sK21) ),
inference(forward_subsumption_resolution,[],[f50722,f561]) ).
fof(f52423,definition,
( spl22_2418
<=> ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = k10_filter_1(sK19,sK19,sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl22_2418])],[avatar_definition]) ).
fof(f52425,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = k10_filter_1(sK19,sK19,sK20,sK21)
| ~ spl22_2418 ),
inference(avatar_component_clause,[],[f52423]) ).
fof(f52441,plain,
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| empty(k2_lattice3(sK19))
| related(poset_of_lattice(sK19),sK20,sK21) ),
inference(forward_subsumption_resolution,[],[f52414,f560]) ).
fof(f52450,plain,
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| empty(k2_lattice3(sK19))
| related(poset_of_lattice(sK19),sK20,sK21)
| ~ spl22_12 ),
inference(forward_subsumption_resolution,[],[f52441,f640]) ).
fof(f52452,definition,
( spl22_2422
<=> related(poset_of_lattice(sK19),sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl22_2422])],[avatar_definition]) ).
fof(f52454,plain,
( related(poset_of_lattice(sK19),sK20,sK21)
| ~ spl22_2422 ),
inference(avatar_component_clause,[],[f52452]) ).
fof(f52458,plain,
( ~ element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| related(poset_of_lattice(sK19),sK20,sK21)
| ~ spl22_12
| spl22_106 ),
inference(forward_subsumption_resolution,[],[f52450,f1710]) ).
fof(f52459,plain,
( spl22_2422
| ~ spl22_2088
| ~ spl22_12
| spl22_106 ),
inference(avatar_split_clause,[],[f52458,f1708,f639,f40722,f52452]) ).
fof(f52542,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = unordered_pair(singleton(sK20),unordered_pair(sK20,sK21))
| empty(the_carrier(sK19))
| ~ spl22_29 ),
inference(resolution,[],[f763,f383]) ).
fof(f52602,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = unordered_pair(singleton(sK20),unordered_pair(sK20,sK21))
| spl22_28
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f52542,f759]) ).
fof(f52634,plain,
( ordered_pair_as_product_element(the_carrier(sK19),the_carrier(sK19),sK20,sK21) = k10_filter_1(sK19,sK19,sK20,sK21)
| spl22_28
| ~ spl22_29 ),
inference(forward_demodulation,[],[f52602,f1223]) ).
fof(f52640,plain,
( spl22_2418
| spl22_28
| ~ spl22_29 ),
inference(avatar_split_clause,[],[f52634,f762,f758,f52423]) ).
fof(f52872,plain,
( element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ element(sK21,the_carrier(sK19))
| ~ element(sK20,the_carrier(sK19))
| ~ below_refl(sK19,sK20,sK21)
| ~ spl22_2418 ),
inference(superposition,[],[f2119,f52425]) ).
fof(f52889,plain,
( element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ element(sK20,the_carrier(sK19))
| ~ below_refl(sK19,sK20,sK21)
| ~ spl22_2418 ),
inference(forward_subsumption_resolution,[],[f52872,f384]) ).
fof(f52896,plain,
( element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ below_refl(sK19,sK20,sK21)
| ~ spl22_2418 ),
inference(forward_subsumption_resolution,[],[f52889,f383]) ).
fof(f52903,plain,
( element(k10_filter_1(sK19,sK19,sK20,sK21),k2_lattice3(sK19))
| ~ spl22_1
| ~ spl22_2418 ),
inference(forward_subsumption_resolution,[],[f52896,f395]) ).
fof(f52909,plain,
( spl22_2088
| ~ spl22_1
| ~ spl22_2418 ),
inference(avatar_split_clause,[],[f52903,f52423,f393,f40722]) ).
fof(f53172,plain,
( related_reflexive(poset_of_lattice(sK19),sK20,sK21)
| empty_carrier(poset_of_lattice(sK19))
| ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| ~ spl22_2422 ),
inference(resolution,[],[f52454,f367]) ).
fof(f53186,plain,
( empty_carrier(poset_of_lattice(sK19))
| ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| spl22_2
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53172,f52235]) ).
fof(f53193,plain,
( ~ reflexive_relstr(poset_of_lattice(sK19))
| ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| spl22_2
| spl22_7
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53186,f573]) ).
fof(f53200,plain,
( ~ rel_str(poset_of_lattice(sK19))
| ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| spl22_2
| spl22_7
| ~ spl22_13
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53193,f644]) ).
fof(f53207,plain,
( ~ element(sK20,the_carrier(poset_of_lattice(sK19)))
| ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53200,f640]) ).
fof(f53214,plain,
( ~ element(sK21,the_carrier(poset_of_lattice(sK19)))
| spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53207,f560]) ).
fof(f53215,plain,
( $false
| spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| ~ spl22_2422 ),
inference(forward_subsumption_resolution,[],[f53214,f561]) ).
fof(f53216,plain,
( spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| ~ spl22_2422 ),
inference(avatar_contradiction_clause,[],[f53215]) ).
cnf(s1,plain,
( spl22_1
| spl22_2 ),
inference(sat_conversion,[],[f400]) ).
cnf(s2,plain,
( ~ spl22_1
| ~ spl22_2 ),
inference(sat_conversion,[],[f401]) ).
cnf(s11,plain,
~ spl22_7,
inference(sat_conversion,[],[f607]) ).
cnf(s19,plain,
( spl22_21
| ~ spl22_22
| ~ spl22_23
| ~ spl22_24 ),
inference(sat_conversion,[],[f716]) ).
cnf(s22,plain,
( spl22_28
| spl22_29 ),
inference(sat_conversion,[],[f764]) ).
cnf(s74,plain,
( spl22_28
| ~ spl22_100 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s75,plain,
( ~ spl22_21
| spl22_100
| ~ spl22_106 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s2295,plain,
spl22_22,
inference(sat_conversion,[],[f40982]) ).
cnf(s2296,plain,
spl22_23,
inference(sat_conversion,[],[f40988]) ).
cnf(s2297,plain,
spl22_24,
inference(sat_conversion,[],[f40993]) ).
cnf(s2339,plain,
spl22_1384,
inference(sat_conversion,[],[f41599]) ).
cnf(s2347,plain,
spl22_12,
inference(sat_conversion,[],[f41739]) ).
cnf(s2351,plain,
spl22_13,
inference(sat_conversion,[],[f41767]) ).
cnf(s2855,plain,
( ~ spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| spl22_2101 ),
inference(sat_conversion,[],[f51944]) ).
cnf(s2856,plain,
( ~ spl22_28
| ~ spl22_1384 ),
inference(sat_conversion,[],[f51947]) ).
cnf(s2977,plain,
( spl22_1
| spl22_28
| ~ spl22_29
| ~ spl22_2101 ),
inference(sat_conversion,[],[f52333]) ).
cnf(s3037,plain,
( ~ spl22_12
| spl22_106
| ~ spl22_2088
| spl22_2422 ),
inference(sat_conversion,[],[f52459]) ).
cnf(s3039,plain,
( spl22_28
| ~ spl22_29
| spl22_2418 ),
inference(sat_conversion,[],[f52640]) ).
cnf(s3047,plain,
( ~ spl22_1
| spl22_2088
| ~ spl22_2418 ),
inference(sat_conversion,[],[f52909]) ).
cnf(s3058,plain,
( spl22_2
| spl22_7
| ~ spl22_12
| ~ spl22_13
| ~ spl22_2422 ),
inference(sat_conversion,[],[f53216]) ).
cnf(s3100,plain,
~ spl22_28,
inference(rat,[],[s2856,s2339]) ).
cnf(s3741,plain,
~ spl22_100,
inference(rat,[],[s74,s3100]) ).
cnf(s3812,plain,
spl22_29,
inference(rat,[],[s22,s3100]) ).
cnf(s3813,plain,
spl22_2418,
inference(rat,[],[s3039,s3100,s3812]) ).
cnf(s3873,plain,
spl22_21,
inference(rat,[],[s19,s2297,s2296,s2295]) ).
cnf(s3885,plain,
~ spl22_106,
inference(rat,[],[s75,s3741,s3873]) ).
cnf(s3907,plain,
spl22_1,
inference(rat,[],[s2855,s1,s2977,s2347,s2351,s11,s3100,s3812]) ).
cnf(s3908,plain,
spl22_2088,
inference(rat,[],[s3047,s3813,s3907]) ).
cnf(s3912,plain,
~ spl22_2,
inference(rat,[],[s2,s3907]) ).
cnf(s3913,plain,
spl22_2422,
inference(rat,[],[s3037,s3885,s2347,s3908]) ).
cnf(s3914,plain,
$false,
inference(rat,[],[s3058,s11,s2351,s2347,s3913,s3912]) ).
fof(f53217,plain,
$false,
inference(avatar_sat_refutation,[],[s3914]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU346+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.43 % Computer : n002.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 28 04:52:22 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.49 Running first-order model finding
% 0.21/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.11/4.26 % (4155312)Will run a generic schedule for satisfiability detection.
% 26.11/4.26 % (4155320)dis+10_1_sil=32000:sp=arity:random_seed=2545545649:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.11/4.26 % (4155318)% WARNING: option uhcvi not known.
% 26.11/4.26 % (4155323)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=888680649:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.11/4.26 % (4155318)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=967180146:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.11/4.26 % (4155317)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3139978886_2999 on theBenchmark for (2999ds/0Mi)
% 26.11/4.26 % (4155322)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1737356074:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.11/4.26 % (4155319)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3035728906:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.11/4.26 % (4155321)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=977374863:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.11/4.26 % TRYING [1]
% 26.11/4.26 % TRYING [2]
% 26.11/4.26 % TRYING [3]
% 26.11/4.26 % (4155320)Instruction limit reached!
% 26.11/4.26 % (4155320)------------------------------
% 26.11/4.26 % (4155320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.11/4.26 % (4155320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.26 % (4155320)CaDiCaL version: 2.1.3
% 26.11/4.26 % (4155320)Termination reason: Instruction limit
% 26.11/4.26 % (4155320)Termination phase: Saturation
% 26.11/4.26 % (4155320)Time elapsed: 0.057 s
% 26.11/4.26 % (4155320)Peak memory usage: 13 MB
% 26.11/4.26 % (4155320)Instructions burned: 105 (million)
% 26.11/4.26 % TRYING [4]
% 26.11/4.26 % (4155331)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2853229749:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 26.11/4.26 % TRYING [1]
% 26.11/4.26 % TRYING [2]
% 26.11/4.26 % TRYING [3]
% 26.11/4.26 % TRYING [4]
% 26.11/4.26 % (4155321)Instruction limit reached!
% 26.11/4.26 % (4155321)------------------------------
% 26.11/4.26 % (4155321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.11/4.26 % (4155321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.26 % (4155321)CaDiCaL version: 2.1.3
% 26.11/4.26 % (4155321)Termination reason: Instruction limit
% 26.11/4.26 % (4155321)Termination phase: Saturation
% 26.11/4.26 % (4155321)Time elapsed: 0.113 s
% 26.11/4.26 % (4155321)Peak memory usage: 13 MB
% 26.11/4.26 % (4155321)Instructions burned: 116 (million)
% 26.11/4.26 % (4155322)Instruction limit reached!
% 26.11/4.26 % (4155322)------------------------------
% 26.11/4.26 % (4155322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.11/4.26 % (4155322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.26 % (4155322)CaDiCaL version: 2.1.3
% 26.11/4.26 % (4155322)Termination reason: Instruction limit
% 26.11/4.26 % (4155322)Termination phase: Saturation
% 26.11/4.26 % (4155322)Time elapsed: 0.132 s
% 26.11/4.26 % (4155322)Peak memory usage: 14 MB
% 26.11/4.26 % (4155322)Instructions burned: 131 (million)
% 26.11/4.26 % (4155333)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4004146040:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.11/4.26 % (4155334)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1129493774:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.11/4.26 % (4155323)Instruction limit reached!
% 26.11/4.26 % (4155323)------------------------------
% 26.11/4.26 % (4155323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.11/4.26 % (4155323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.26 % (4155323)CaDiCaL version: 2.1.3
% 26.11/4.26 % (4155323)Termination reason: Instruction limit
% 26.11/4.26 % (4155323)Termination phase: Saturation
% 26.11/4.26 % (4155323)Time elapsed: 0.169 s
% 26.11/4.26 % (4155323)Peak memory usage: 14 MB
% 26.11/4.26 % (4155323)Instructions burned: 160 (million)
% 26.11/4.26 % (4155337)ott-21_1_sil=16000:fs=off:random_seed=4147899496:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.11/4.26 % TRYING [5]
% 26.11/4.26 % (4155333)Instruction limit reached!
% 26.11/4.26 % (4155333)------------------------------
% 26.11/4.26 % (4155333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155333)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155333)Termination reason: Instruction limit
% 60.36/9.11 % (4155333)Termination phase: Saturation
% 60.36/9.11 % (4155333)Time elapsed: 0.122 s
% 60.36/9.11 % (4155333)Peak memory usage: 14 MB
% 60.36/9.11 % (4155333)Instructions burned: 131 (million)
% 60.36/9.11 % (4155339)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2993091653:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 60.36/9.11 % (4155337)Instruction limit reached!
% 60.36/9.11 % (4155337)------------------------------
% 60.36/9.11 % (4155337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155337)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155337)Termination reason: Instruction limit
% 60.36/9.11 % (4155337)Termination phase: Saturation
% 60.36/9.11 % (4155337)Time elapsed: 0.108 s
% 60.36/9.11 % (4155337)Peak memory usage: 13 MB
% 60.36/9.11 % (4155337)Instructions burned: 181 (million)
% 60.36/9.11 % TRYING [5]
% 60.36/9.11 % (4155341)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=572069086:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 60.36/9.11 % TRYING [1]
% 60.36/9.11 % TRYING [2]
% 60.36/9.11 % (4155331)Instruction limit reached!
% 60.36/9.11 % (4155331)------------------------------
% 60.36/9.11 % (4155331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155331)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155331)Termination reason: Instruction limit
% 60.36/9.11 % (4155331)Termination phase: Finite model building constraint generation
% 60.36/9.11 % (4155331)Time elapsed: 0.280 s
% 60.36/9.11 % (4155331)Peak memory usage: 30 MB
% 60.36/9.11 % (4155331)Instructions burned: 715 (million)
% 60.36/9.11 % TRYING [3]
% 60.36/9.11 % (4155343)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3252286308:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 60.36/9.11 % TRYING [4]
% 60.36/9.11 % TRYING [5]
% 60.36/9.11 % (4155341)Instruction limit reached!
% 60.36/9.11 % (4155341)------------------------------
% 60.36/9.11 % (4155341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155341)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155341)Termination reason: Instruction limit
% 60.36/9.11 % (4155341)Termination phase: Finite model building constraint generation
% 60.36/9.11 % (4155341)Time elapsed: 0.343 s
% 60.36/9.11 % (4155341)Peak memory usage: 22 MB
% 60.36/9.11 % (4155341)Instructions burned: 867 (million)
% 60.36/9.11 % (4155345)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2947211703:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 60.36/9.11 % (4155334)Instruction limit reached!
% 60.36/9.11 % (4155334)------------------------------
% 60.36/9.11 % (4155334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155334)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155334)Termination reason: Instruction limit
% 60.36/9.11 % (4155334)Termination phase: Saturation
% 60.36/9.11 % (4155334)Time elapsed: 0.651 s
% 60.36/9.11 % (4155334)Peak memory usage: 20 MB
% 60.36/9.11 % (4155334)Instructions burned: 684 (million)
% 60.36/9.11 % (4155339)Instruction limit reached!
% 60.36/9.11 % (4155339)------------------------------
% 60.36/9.11 % (4155339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.36/9.11 % (4155339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.36/9.11 % (4155339)CaDiCaL version: 2.1.3
% 60.36/9.11 % (4155339)Termination reason: Instruction limit
% 60.36/9.11 % (4155339)Termination phase: Saturation
% 60.36/9.11 % (4155339)Time elapsed: 0.523 s
% 60.36/9.11 % (4155339)Peak memory usage: 15 MB
% 60.36/9.11 % (4155339)Instructions burned: 479 (million)
% 60.36/9.11 % (4155347)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1886601542:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 60.36/9.11 % (4155348)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=802945631:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 60.36/9.11 % TRYING [6]
% 60.36/9.11 % (4155345)Instruction limit reached!
% 70.77/10.60 % (4155345)------------------------------
% 70.77/10.60 % (4155345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155345)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155345)Termination reason: Instruction limit
% 70.77/10.60 % (4155345)Termination phase: Finite model building constraint generation
% 70.77/10.60 % (4155345)Time elapsed: 0.478 s
% 70.77/10.60 % (4155345)Peak memory usage: 105 MB
% 70.77/10.60 % (4155345)Instructions burned: 892 (million)
% 70.77/10.60 % (4155351)fmb+10_1_sil=64000:random_seed=2686487818:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 70.77/10.60 % TRYING [1]
% 70.77/10.60 % TRYING [2]
% 70.77/10.60 % TRYING [3]
% 70.77/10.60 % TRYING [4]
% 70.77/10.60 % (4155347)Instruction limit reached!
% 70.77/10.60 % (4155347)------------------------------
% 70.77/10.60 % (4155347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155347)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155347)Termination reason: Instruction limit
% 70.77/10.60 % (4155347)Termination phase: Saturation
% 70.77/10.60 % (4155347)Time elapsed: 0.636 s
% 70.77/10.60 % (4155347)Peak memory usage: 22 MB
% 70.77/10.60 % (4155347)Instructions burned: 693 (million)
% 70.77/10.60 % (4155353)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1745504199:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 70.77/10.60 % (4155343)Instruction limit reached!
% 70.77/10.60 % (4155343)------------------------------
% 70.77/10.60 % (4155343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155343)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155343)Termination reason: Instruction limit
% 70.77/10.60 % (4155343)Termination phase: Saturation
% 70.77/10.60 % (4155343)Time elapsed: 1.160 s
% 70.77/10.60 % (4155343)Peak memory usage: 29 MB
% 70.77/10.60 % (4155343)Instructions burned: 1180 (million)
% 70.77/10.60 % TRYING [20]
% 70.77/10.60 % (4155355)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4147727329:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 70.77/10.60 % TRYING [8]
% 70.77/10.60 % TRYING [5]
% 70.77/10.60 % (4155348)Instruction limit reached!
% 70.77/10.60 % (4155348)------------------------------
% 70.77/10.60 % (4155348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155348)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155348)Termination reason: Instruction limit
% 70.77/10.60 % (4155348)Termination phase: Saturation
% 70.77/10.60 % (4155348)Time elapsed: 0.800 s
% 70.77/10.60 % (4155348)Peak memory usage: 21 MB
% 70.77/10.60 % (4155348)Instructions burned: 880 (million)
% 70.77/10.60 % (4155359)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=41462271:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 70.77/10.60 % (4155355)Instruction limit reached!
% 70.77/10.60 % (4155355)------------------------------
% 70.77/10.60 % (4155355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155355)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155355)Termination reason: Instruction limit
% 70.77/10.60 % (4155355)Termination phase: Finite model building constraint generation
% 70.77/10.60 % (4155355)Time elapsed: 0.587 s
% 70.77/10.60 % (4155355)Peak memory usage: 45 MB
% 70.77/10.60 % (4155355)Instructions burned: 921 (million)
% 70.77/10.60 % (4155361)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3113245222:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 70.77/10.60 % (4155361)Instruction limit reached!
% 70.77/10.60 % (4155361)------------------------------
% 70.77/10.60 % (4155361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155361)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155361)Termination reason: Instruction limit
% 70.77/10.60 % (4155361)Termination phase: Saturation
% 70.77/10.60 % (4155361)Time elapsed: 1.433 s
% 70.77/10.60 % (4155361)Peak memory usage: 31 MB
% 70.77/10.60 % (4155361)Instructions burned: 1473 (million)
% 70.77/10.60 % (4155363)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=604141363:i=6324_2963 on theBenchmark for (2963ds/6324Mi)
% 70.77/10.60 % (4155363)Cannot represent all propositional literals internally
% 70.77/10.60 % (4155363)Refutation not found, incomplete strategy
% 70.77/10.60 % (4155363)------------------------------
% 70.77/10.60 % (4155363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155363)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155363)Termination reason: Refutation not found, incomplete strategy
% 70.77/10.60 % (4155363)Time elapsed: 0.021 s
% 70.77/10.60 % (4155363)Peak memory usage: 11 MB
% 70.77/10.60 % (4155363)Instructions burned: 23 (million)
% 70.77/10.60 % (4155363)------------------------------
% 70.77/10.60 % (4155363)------------------------------
% 70.77/10.60 % (4155365)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3615950016:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 70.77/10.60 % TRYING [16]
% 70.77/10.60 % TRYING [6]
% 70.77/10.60 % (4155365)Instruction limit reached!
% 70.77/10.60 % (4155365)------------------------------
% 70.77/10.60 % (4155365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155365)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155365)Termination reason: Instruction limit
% 70.77/10.60 % (4155365)Termination phase: Finite model building constraint generation
% 70.77/10.60 % (4155365)Time elapsed: 1.413 s
% 70.77/10.60 % (4155365)Peak memory usage: 122 MB
% 70.77/10.60 % (4155365)Instructions burned: 2175 (million)
% 70.77/10.60 % (4155367)ott-2_1_sil=16000:newcnf=on:random_seed=784503013:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2947 on theBenchmark for (2947ds/869Mi)
% 70.77/10.60 % (4155359)Instruction limit reached!
% 70.77/10.60 % (4155359)------------------------------
% 70.77/10.60 % (4155359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155359)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155359)Termination reason: Instruction limit
% 70.77/10.60 % (4155359)Termination phase: Saturation
% 70.77/10.60 % (4155359)Time elapsed: 4.112 s
% 70.77/10.60 % (4155359)Peak memory usage: 30 MB
% 70.77/10.60 % (4155359)Instructions burned: 5131 (million)
% 70.77/10.60 % (4155369)ott+10_1_sil=32000:tgt=ground:random_seed=2658139146:i=5114:av=off_2941 on theBenchmark for (2941ds/5114Mi)
% 70.77/10.60 % (4155367)Instruction limit reached!
% 70.77/10.60 % (4155367)------------------------------
% 70.77/10.60 % (4155367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155367)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155367)Termination reason: Instruction limit
% 70.77/10.60 % (4155367)Termination phase: Saturation
% 70.77/10.60 % (4155367)Time elapsed: 0.827 s
% 70.77/10.60 % (4155367)Peak memory usage: 22 MB
% 70.77/10.60 % (4155367)Instructions burned: 870 (million)
% 70.77/10.60 % (4155371)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3288051022:i=54282_2938 on theBenchmark for (2938ds/54282Mi)
% 70.77/10.60 % TRYING [1]
% 70.77/10.60 % TRYING [2]
% 70.77/10.60 % TRYING [3]
% 70.77/10.60 % TRYING [4]
% 70.77/10.60 % TRYING [5]
% 70.77/10.60 % TRYING [7]
% 70.77/10.60 % TRYING [6]
% 70.77/10.60 % (4155353)Instruction limit reached!
% 70.77/10.60 % (4155353)------------------------------
% 70.77/10.60 % (4155353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155353)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155353)Termination reason: Instruction limit
% 70.77/10.60 % (4155353)Termination phase: Finite model building constraint generation
% 70.77/10.60 % (4155353)Time elapsed: 5.991 s
% 70.77/10.60 % (4155353)Peak memory usage: 370 MB
% 70.77/10.60 % (4155353)Instructions burned: 9515 (million)
% 70.77/10.60 % (4155373)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3022028365:i=3512:aac=none_2923 on theBenchmark for (2923ds/3512Mi)
% 70.77/10.60 % (4155351)Instruction limit reached!
% 70.77/10.60 % (4155351)------------------------------
% 70.77/10.60 % (4155351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 70.77/10.60 % (4155351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.77/10.60 % (4155351)CaDiCaL version: 2.1.3
% 70.77/10.60 % (4155351)Termination reason: Instruction limit
% 70.77/10.60 % (4155351)Termination phase: Finite model building SAT solving
% 70.77/10.60 % (4155351)Time elapsed: 7.371 s
% 70.77/10.60 % (4155351)Peak memory usage: 133 MB
% 70.77/10.60 % (4155351)Instructions burned: 22063 (million)
% 70.77/10.60 % (4155375)dis+21_1_sil=32000:sas=cadical:random_seed=832560869:i=3773:amm=off_2913 on theBenchmark for (2913ds/3773Mi)
% 70.77/10.60 % (4155375) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4155312-4155375"...
% 70.77/10.60 % (4155375)...printing done.
% 70.77/10.60 % (4155375)Refutation found. Thanks to Tanya!
% 70.77/10.60 % SZS status Theorem for theBenchmark
% 70.77/10.60 % SZS output start Proof for theBenchmark
% See solution above
% 71.33/10.61 % (4155375)------------------------------
% 71.33/10.61 % (4155375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 71.33/10.61 % (4155375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.33/10.61 % (4155375)CaDiCaL version: 2.1.3
% 71.33/10.61 % (4155375)Termination reason: Refutation
% 71.33/10.61 % (4155375)Time elapsed: 1.379 s
% 71.33/10.61 % (4155375)Peak memory usage: 35 MB
% 71.33/10.61 % (4155375)Instructions burned: 2840 (million)
% 71.33/10.61 % (4155312)Success in time 10.097 s
% 71.33/10.61 % Vampire exiting
%------------------------------------------------------------------------------