%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU348+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n010.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 : Fri Sep 25 02:57:00 PM UTC 2026
% Result : Theorem 2.78s 1.27s
% Output : CNFRefutation 2.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 8
% Syntax : Number of formulae : 81 ( 17 unt; 3 def)
% Number of atoms : 316 ( 34 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 368 ( 150 ~; 163 |; 37 &)
% ( 5 <=>; 11 =>; 0 <=; 2 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 4 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 96 ( 0 sgn 84 !; 12 ?; 36 :)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0] :
( ( latt_str(X0)
& lattice(X0)
& ~ empty_carrier(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(f8,axiom,
! [X0] :
( ( latt_str(X0)
& lattice(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,the_carrier(poset_of_lattice(X0)))
=> cast_to_el_of_lattice(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f16,axiom,
! [X0,X1] :
( ( element(X1,the_carrier(poset_of_lattice(X0)))
& latt_str(X0)
& lattice(X0)
& ~ empty_carrier(X0) )
=> element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f57,axiom,
! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_lattice3) ).
fof(f58,conjecture,
! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_lattice3) ).
fof(f59,negated_conjecture,
~ ! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f81,plain,
! [X0] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| cast_to_el_of_LattPOSet(X0,X1) = X1 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f82,plain,
! [X0] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| cast_to_el_of_LattPOSet(X0,X1) = X1 ) ),
inference(flattening,[],[f81]) ).
fof(f83,plain,
! [X0] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| cast_to_el_of_lattice(X0,X1) = X1 ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f84,plain,
! [X0] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| cast_to_el_of_lattice(X0,X1) = X1 ) ),
inference(flattening,[],[f83]) ).
fof(f92,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f93,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
inference(flattening,[],[f92]) ).
fof(f119,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f120,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
inference(flattening,[],[f119]) ).
fof(f121,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(ennf_transformation,[],[f59]) ).
fof(f122,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(flattening,[],[f121]) ).
fof(f149,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( ( ~ latt_set_smaller(X1,X2,X0)
| relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
& ( ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_set_smaller(X1,X2,X0) ) ) ) ),
inference(nnf_transformation,[],[f120]) ).
fof(f150,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(nnf_transformation,[],[f122]) ).
fof(f151,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(flattening,[],[f150]) ).
fof(f152,plain,
( latt_str(sK17)
& lattice(sK17)
& ~ empty_carrier(sK17)
& element(sK18,the_carrier(poset_of_lattice(sK17)))
& ( relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) )
& ( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X2,sK18)],[f151]) ).
fof(f165,plain,
! [X0,X1] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| cast_to_el_of_LattPOSet(X0,X1) = X1 ),
inference(cnf_transformation,[],[f82]) ).
fof(f166,plain,
! [X0,X1] :
( ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| cast_to_el_of_lattice(X0,X1) = X1 ),
inference(cnf_transformation,[],[f84]) ).
fof(f180,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0)
| element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f240,plain,
! [X2,X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ latt_set_smaller(X1,X2,X0)
| relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ),
inference(cnf_transformation,[],[f149]) ).
fof(f241,plain,
! [X2,X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_set_smaller(X1,X2,X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f242,plain,
latt_str(sK17),
inference(cnf_transformation,[],[f152]) ).
fof(f243,plain,
lattice(sK17),
inference(cnf_transformation,[],[f152]) ).
fof(f244,plain,
~ empty_carrier(sK17),
inference(cnf_transformation,[],[f152]) ).
fof(f245,plain,
element(sK18,the_carrier(poset_of_lattice(sK17))),
inference(cnf_transformation,[],[f152]) ).
fof(f246,plain,
( relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(cnf_transformation,[],[f152]) ).
fof(f247,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| ( cast_to_el_of_LattPOSet(X1,X0) = X0 )
| ~ latt_str(X1)
| ~ lattice(X1)
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| ( cast_to_el_of_lattice(X1,X0) = X0 )
| ~ latt_str(X1)
| ~ lattice(X1)
| ~ element(X0,the_carrier(poset_of_lattice(X1))) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| element(cast_to_el_of_lattice(X1,X0),the_carrier(X1))
| ~ latt_str(X1)
| ~ lattice(X1)
| ~ element(X0,the_carrier(poset_of_lattice(X1))) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| latt_set_smaller(X0,X2,X1)
| ~ latt_str(X0)
| ~ lattice(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(poset_of_lattice(X0),X1,cast_to_el_of_LattPOSet(X0,X2)) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| relstr_element_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| ~ latt_str(X0)
| ~ lattice(X0)
| ~ element(X1,the_carrier(X0))
| ~ latt_set_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_136,negated_conjecture,
( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_137,negated_conjecture,
( relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_138,negated_conjecture,
element(sK18,the_carrier(poset_of_lattice(sK17))),
inference(cnf_transformation,[],[f245]) ).
tcf(c_139,negated_conjecture,
~ empty_carrier(sK17),
inference(cnf_transformation,[],[f244]) ).
tcf(c_140,negated_conjecture,
lattice(sK17),
inference(cnf_transformation,[],[f243]) ).
tcf(c_141,negated_conjecture,
latt_str(sK17),
inference(cnf_transformation,[],[f242]) ).
tcf(c_223,plain,
( ~ latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16)
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18) ),
inference(prop_impl_just,[status(thm)],[c_136]) ).
tcf(c_224,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(renaming,[status(thm)],[c_223]) ).
tcf(c_225,plain,
( latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16)
| relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18) ),
inference(prop_impl_just,[status(thm)],[c_137]) ).
tcf(c_226,plain,
( relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| latt_set_smaller(sK17,cast_to_el_of_lattice(sK17,sK18),sK16) ),
inference(renaming,[status(thm)],[c_225]) ).
tcf(c_1616,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ~ latt_str(X0)
| ~ lattice(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ relstr_element_smaller(poset_of_lattice(X0),X1,cast_to_el_of_LattPOSet(X0,X2))
| ( X1 != sK16 )
| ( X0 != sK17 )
| ( cast_to_el_of_lattice(sK17,sK18) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_134,c_224]) ).
tcf(c_1617,plain,
( empty_carrier(sK17)
| ~ latt_str(sK17)
| ~ lattice(sK17)
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17))
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18))) ),
inference(unflattening,[status(thm)],[c_1616]) ).
tcf(c_1618,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18)))
| ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17))
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18) ),
inference(global_subsumption_just,[status(thm)],[c_1617,c_141,c_140,c_139,c_1617]) ).
tcf(c_1619,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17))
| ~ relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18))) ),
inference(renaming,[status(thm)],[c_1618]) ).
tcf(c_1629,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| relstr_element_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| ~ latt_str(X0)
| ~ lattice(X0)
| ~ element(X1,the_carrier(X0))
| ( X2 != sK16 )
| ( X0 != sK17 )
| ( cast_to_el_of_lattice(sK17,sK18) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_135,c_226]) ).
tcf(c_1630,plain,
( empty_carrier(sK17)
| relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18)))
| ~ latt_str(sK17)
| ~ lattice(sK17)
| ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17)) ),
inference(unflattening,[status(thm)],[c_1629]) ).
tcf(c_1631,plain,
( ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17))
| relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18)))
| relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18) ),
inference(global_subsumption_just,[status(thm)],[c_1630,c_141,c_140,c_139,c_1630]) ).
tcf(c_1632,plain,
( relstr_element_smaller(poset_of_lattice(sK17),sK16,sK18)
| relstr_element_smaller(poset_of_lattice(sK17),sK16,cast_to_el_of_LattPOSet(sK17,cast_to_el_of_lattice(sK17,sK18)))
| ~ element(cast_to_el_of_lattice(sK17,sK18),the_carrier(sK17)) ),
inference(renaming,[status(thm)],[c_1631]) ).
tcf(c_1697,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ( X0 != sK17 ) ),
inference(resolution_lifted,[status(thm)],[c_74,c_140]) ).
tcf(c_1698,plain,
! [X0: $i] :
( empty_carrier(sK17)
| element(cast_to_el_of_lattice(sK17,X0),the_carrier(sK17))
| ~ latt_str(sK17)
| ~ element(X0,the_carrier(poset_of_lattice(sK17))) ),
inference(unflattening,[status(thm)],[c_1697]) ).
tcf(c_1700,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(poset_of_lattice(sK17)))
| element(cast_to_el_of_lattice(sK17,X0),the_carrier(sK17)) ),
inference(global_subsumption_just,[status(thm)],[c_1698,c_141,c_139,c_1698]) ).
tcf(c_1701,plain,
! [X0: $i] :
( element(cast_to_el_of_lattice(sK17,X0),the_carrier(sK17))
| ~ element(X0,the_carrier(poset_of_lattice(sK17))) ),
inference(renaming,[status(thm)],[c_1700]) ).
tcf(c_1721,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| ( cast_to_el_of_lattice(X0,X1) = X1 )
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ( X0 != sK17 ) ),
inference(resolution_lifted,[status(thm)],[c_60,c_140]) ).
tcf(c_1722,plain,
! [X0: $i] :
( empty_carrier(sK17)
| ( cast_to_el_of_lattice(sK17,X0) = X0 )
| ~ latt_str(sK17)
| ~ element(X0,the_carrier(poset_of_lattice(sK17))) ),
inference(unflattening,[status(thm)],[c_1721]) ).
tcf(c_1724,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(poset_of_lattice(sK17)))
| ( cast_to_el_of_lattice(sK17,X0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_1722,c_141,c_139,c_1722]) ).
tcf(c_1725,plain,
! [X0: $i] :
( ( cast_to_el_of_lattice(sK17,X0) = X0 )
| ~ element(X0,the_carrier(poset_of_lattice(sK17))) ),
inference(renaming,[status(thm)],[c_1724]) ).
tcf(c_1733,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X0)
| ( cast_to_el_of_LattPOSet(X0,X1) = X1 )
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ( X0 != sK17 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_140]) ).
tcf(c_1734,plain,
! [X0: $i] :
( empty_carrier(sK17)
| ( cast_to_el_of_LattPOSet(sK17,X0) = X0 )
| ~ latt_str(sK17)
| ~ element(X0,the_carrier(sK17)) ),
inference(unflattening,[status(thm)],[c_1733]) ).
tcf(c_1736,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(sK17))
| ( cast_to_el_of_LattPOSet(sK17,X0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_1734,c_141,c_139,c_1734]) ).
tcf(c_1737,plain,
! [X0: $i] :
( ( cast_to_el_of_LattPOSet(sK17,X0) = X0 )
| ~ element(X0,the_carrier(sK17)) ),
inference(renaming,[status(thm)],[c_1736]) ).
tcf(c_5278,definition,
iPr_def_10 = the_carrier(sK17),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_5281,definition,
iPr_def_13 = poset_of_lattice(sK17),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_5282,definition,
iPr_def_14 = the_carrier(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_5291,plain,
! [X0: $i] :
( ( cast_to_el_of_LattPOSet(sK17,X0) = X0 )
| ~ element(X0,iPr_def_10) ),
inference(demodulation,[status(thm)],[c_1737]) ).
tcf(c_5292,plain,
! [X0: $i] :
( ( cast_to_el_of_lattice(sK17,X0) = X0 )
| ~ element(X0,iPr_def_14) ),
inference(demodulation,[status(thm)],[c_1725,c_5281,c_5282]) ).
tcf(c_5294,plain,
! [X0: $i] :
( element(cast_to_el_of_lattice(sK17,X0),iPr_def_10)
| ~ element(X0,iPr_def_14) ),
inference(demodulation,[status(thm)],[c_1701]) ).
tcf(c_5303,negated_conjecture,
element(sK18,iPr_def_14),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_6137,plain,
cast_to_el_of_lattice(sK17,sK18) = sK18,
inference(superposition,[status(thm)],[c_5303,c_5292]) ).
tcf(c_6141,plain,
( element(sK18,iPr_def_10)
| ~ element(sK18,iPr_def_14) ),
inference(superposition,[status(thm)],[c_6137,c_5294]) ).
tcf(c_6142,plain,
element(sK18,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_6141,c_5303]) ).
tcf(c_6143,plain,
cast_to_el_of_LattPOSet(sK17,sK18) = sK18,
inference(superposition,[status(thm)],[c_6142,c_5291]) ).
tcf(c_6597,plain,
( ~ element(sK18,iPr_def_10)
| ~ relstr_element_smaller(iPr_def_13,sK16,sK18) ),
inference(light_normalisation,[status(thm)],[c_1619,c_5278,c_5281,c_6137,c_6143]) ).
tcf(c_6598,plain,
~ relstr_element_smaller(iPr_def_13,sK16,sK18),
inference(forward_subsumption_resolution,[status(thm)],[c_6597,c_6142]) ).
tcf(c_6740,plain,
( relstr_element_smaller(iPr_def_13,sK16,sK18)
| ~ element(sK18,iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_1632,c_5278,c_5281,c_6137,c_6143]) ).
tcf(c_6741,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6740,c_6598,c_6142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU348+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 13:47:43 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 2.78/1.27 % SZS status Started for theBenchmark.p
% 2.78/1.27 % SZS status Theorem for theBenchmark.p
% 2.78/1.27
% 2.78/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.78/1.27
% 2.78/1.27 % ------ iProver source info
% 2.78/1.27
% 2.78/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 2.78/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.78/1.27 % git: non_committed_changes: false
% 2.78/1.27
% 2.78/1.27 % ------ Parsing...
% 2.78/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.78/1.27
% 2.78/1.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 25 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 15 0s sf_e pe_s pe_e %
% 2.78/1.27
% 2.78/1.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.78/1.27
% 2.78/1.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.78/1.27 % ------ Proving...
% 2.78/1.27 % ------ Problem Properties
% 2.78/1.27
% 2.78/1.27 %
% 2.78/1.27 % clauses 84
% 2.78/1.27 % conjectures 2
% 2.78/1.27 % EPR 28
% 2.78/1.27 % Horn 75
% 2.78/1.27 % unary 43
% 2.78/1.27 % binary 27
% 2.78/1.27 % lits 139
% 2.78/1.27 % lits eq 21
% 2.78/1.27 % fd_pure 0
% 2.78/1.27 % fd_pseudo 0
% 2.78/1.27 % fd_cond 1
% 2.78/1.27 % fd_pseudo_cond 3
% 2.78/1.27 % AC symbols 0
% 2.78/1.27
% 2.78/1.27 % ------ Schedule dynamic 5 is on
% 2.78/1.27
% 2.78/1.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.78/1.27
% 2.78/1.27
% 2.78/1.27 % ------
% 2.78/1.27 % Current options:
% 2.78/1.27 % ------
% 2.78/1.27
% 2.78/1.27
% 2.78/1.27 %
% 2.78/1.27
% 2.78/1.27 % ------ Proving...
% 2.78/1.27 %
% 2.78/1.27
% 2.78/1.27 % SZS status Theorem for theBenchmark.p
% 2.78/1.27
% 2.78/1.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.78/1.27
% 2.78/1.27
%------------------------------------------------------------------------------