%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n017.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 62.24s 25.44s
% Output : CNFRefutation 62.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 5
% Syntax : Number of formulae : 79 ( 15 unt; 0 def)
% Number of atoms : 291 ( 27 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 355 ( 143 ~; 157 |; 37 &)
% ( 5 <=>; 11 =>; 0 <=; 2 <~>)
% Maximal formula depth : 10 ( 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 : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 100 !; 12 ?; 52 :)
% Comments :
%------------------------------------------------------------------------------
fof(f97,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/sandbox/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f106,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/sandbox/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f191,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/sandbox/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f532,axiom,
! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_lattice3) ).
fof(f535,conjecture,
! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_lattice3) ).
fof(f536,negated_conjecture,
~ ! [X0,X1] :
( ( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f535]) ).
fof(f886,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
inference(ennf_transformation,[],[f532]) ).
fof(f887,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
inference(flattening,[],[f886]) ).
fof(f891,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(ennf_transformation,[],[f536]) ).
fof(f892,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(flattening,[],[f891]) ).
fof(f1226,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,[],[f97]) ).
fof(f1227,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,[],[f1226]) ).
fof(f1230,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,[],[f191]) ).
fof(f1231,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,[],[f1230]) ).
fof(f1232,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,[],[f106]) ).
fof(f1233,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,[],[f1232]) ).
fof(f1622,plain,
! [X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ! [X2] :
( ~ element(X2,the_carrier(X1))
| ( ( ~ latt_element_smaller(X1,X2,X0)
| relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
& ( ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_element_smaller(X1,X2,X0) ) ) ) ),
inference(nnf_transformation,[],[f887]) ).
fof(f1624,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(nnf_transformation,[],[f892]) ).
fof(f1625,plain,
? [X0,X1] :
( latt_str(X1)
& lattice(X1)
& ~ empty_carrier(X1)
& ? [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
& ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& ( ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2)
| ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(flattening,[],[f1624]) ).
fof(f1626,plain,
( latt_str(sK170)
& lattice(sK170)
& ~ empty_carrier(sK170)
& element(sK171,the_carrier(poset_of_lattice(sK170)))
& ( relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) )
& ( ~ relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| ~ latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK169,sK170,sK171]),skolemize(X0,sK169),skolemize(X1,sK170),skolemize(X2,sK171)],[f1625]) ).
fof(f2439,plain,
! [X2,X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ latt_element_smaller(X1,X2,X0)
| relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ),
inference(cnf_transformation,[],[f1622]) ).
fof(f2440,plain,
! [X2,X0,X1] :
( ~ latt_str(X1)
| ~ lattice(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| latt_element_smaller(X1,X2,X0) ),
inference(cnf_transformation,[],[f1622]) ).
fof(f2445,plain,
latt_str(sK170),
inference(cnf_transformation,[],[f1626]) ).
fof(f2446,plain,
lattice(sK170),
inference(cnf_transformation,[],[f1626]) ).
fof(f2447,plain,
~ empty_carrier(sK170),
inference(cnf_transformation,[],[f1626]) ).
fof(f2448,plain,
element(sK171,the_carrier(poset_of_lattice(sK170))),
inference(cnf_transformation,[],[f1626]) ).
fof(f2449,plain,
( relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) ),
inference(cnf_transformation,[],[f1626]) ).
fof(f2450,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| ~ latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) ),
inference(cnf_transformation,[],[f1626]) ).
fof(f3326,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,[],[f1227]) ).
fof(f3331,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,[],[f1231]) ).
fof(f3332,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,[],[f1233]) ).
tcf(c_448,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| latt_element_smaller(X0,X2,X1)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(poset_of_lattice(X0),X1,cast_to_el_of_LattPOSet(X0,X2)) ),
inference(cnf_transformation,[],[f2440]) ).
tcf(c_449,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ latt_element_smaller(X0,X1,X2) ),
inference(cnf_transformation,[],[f2439]) ).
tcf(c_454,negated_conjecture,
( ~ relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| ~ latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) ),
inference(cnf_transformation,[],[f2450]) ).
tcf(c_455,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171)
| latt_element_smaller(sK170,cast_to_el_of_lattice(sK170,sK171),sK169) ),
inference(cnf_transformation,[],[f2449]) ).
tcf(c_456,negated_conjecture,
element(sK171,the_carrier(poset_of_lattice(sK170))),
inference(cnf_transformation,[],[f2448]) ).
tcf(c_457,negated_conjecture,
~ empty_carrier(sK170),
inference(cnf_transformation,[],[f2447]) ).
tcf(c_458,negated_conjecture,
lattice(sK170),
inference(cnf_transformation,[],[f2446]) ).
tcf(c_459,negated_conjecture,
latt_str(sK170),
inference(cnf_transformation,[],[f2445]) ).
tcf(c_1329,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| ( cast_to_el_of_LattPOSet(X1,X0) = X0 )
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f3326]) ).
tcf(c_1334,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| element(cast_to_el_of_lattice(X1,X0),the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X0,the_carrier(poset_of_lattice(X1))) ),
inference(cnf_transformation,[],[f3331]) ).
tcf(c_1335,plain,
! [X0: $i,X1: $i] :
( empty_carrier(X1)
| ( cast_to_el_of_lattice(X1,X0) = X0 )
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X0,the_carrier(poset_of_lattice(X1))) ),
inference(cnf_transformation,[],[f3332]) ).
tcf(c_65069,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ latt_element_smaller(X0,X1,X2)
| ( X0 != sK170 ) ),
inference(resolution_lifted,[status(thm)],[c_449,c_458]) ).
tcf(c_65070,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK170)
| relstr_set_smaller(poset_of_lattice(sK170),X1,cast_to_el_of_LattPOSet(sK170,X0))
| ~ latt_str(sK170)
| ~ element(X0,the_carrier(sK170))
| ~ latt_element_smaller(sK170,X0,X1) ),
inference(unflattening,[status(thm)],[c_65069]) ).
tcf(c_65072,plain,
! [X0: $i,X1: $i] :
( ~ element(X0,the_carrier(sK170))
| ~ latt_element_smaller(sK170,X0,X1)
| relstr_set_smaller(poset_of_lattice(sK170),X1,cast_to_el_of_LattPOSet(sK170,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_65070,c_459,c_457,c_65070]) ).
tcf(c_65073,plain,
! [X0: $i,X1: $i] :
( relstr_set_smaller(poset_of_lattice(sK170),X1,cast_to_el_of_LattPOSet(sK170,X0))
| ~ element(X0,the_carrier(sK170))
| ~ latt_element_smaller(sK170,X0,X1) ),
inference(renaming,[status(thm)],[c_65072]) ).
tcf(c_65084,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| latt_element_smaller(X0,X2,X1)
| ~ latt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ relstr_set_smaller(poset_of_lattice(X0),X1,cast_to_el_of_LattPOSet(X0,X2))
| ( X0 != sK170 ) ),
inference(resolution_lifted,[status(thm)],[c_448,c_458]) ).
tcf(c_65085,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK170)
| latt_element_smaller(sK170,X1,X0)
| ~ latt_str(sK170)
| ~ element(X1,the_carrier(sK170))
| ~ relstr_set_smaller(poset_of_lattice(sK170),X0,cast_to_el_of_LattPOSet(sK170,X1)) ),
inference(unflattening,[status(thm)],[c_65084]) ).
tcf(c_65087,plain,
! [X0: $i,X1: $i] :
( ~ element(X1,the_carrier(sK170))
| ~ relstr_set_smaller(poset_of_lattice(sK170),X0,cast_to_el_of_LattPOSet(sK170,X1))
| latt_element_smaller(sK170,X1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_65085,c_459,c_457,c_65085]) ).
tcf(c_65088,plain,
! [X0: $i,X1: $i] :
( latt_element_smaller(sK170,X1,X0)
| ~ element(X1,the_carrier(sK170))
| ~ relstr_set_smaller(poset_of_lattice(sK170),X0,cast_to_el_of_LattPOSet(sK170,X1)) ),
inference(renaming,[status(thm)],[c_65087]) ).
tcf(c_65765,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 != sK170 ) ),
inference(resolution_lifted,[status(thm)],[c_458,c_1335]) ).
tcf(c_65766,plain,
! [X0: $i] :
( empty_carrier(sK170)
| ( cast_to_el_of_lattice(sK170,X0) = X0 )
| ~ latt_str(sK170)
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(unflattening,[status(thm)],[c_65765]) ).
tcf(c_65768,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(poset_of_lattice(sK170)))
| ( cast_to_el_of_lattice(sK170,X0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_65766,c_459,c_457,c_65766]) ).
tcf(c_65769,plain,
! [X0: $i] :
( ( cast_to_el_of_lattice(sK170,X0) = X0 )
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(renaming,[status(thm)],[c_65768]) ).
tcf(c_65777,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 != sK170 ) ),
inference(resolution_lifted,[status(thm)],[c_458,c_1334]) ).
tcf(c_65778,plain,
! [X0: $i] :
( empty_carrier(sK170)
| element(cast_to_el_of_lattice(sK170,X0),the_carrier(sK170))
| ~ latt_str(sK170)
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(unflattening,[status(thm)],[c_65777]) ).
tcf(c_65780,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(poset_of_lattice(sK170)))
| element(cast_to_el_of_lattice(sK170,X0),the_carrier(sK170)) ),
inference(global_subsumption_just,[status(thm)],[c_65778,c_459,c_457,c_65778]) ).
tcf(c_65781,plain,
! [X0: $i] :
( element(cast_to_el_of_lattice(sK170,X0),the_carrier(sK170))
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(renaming,[status(thm)],[c_65780]) ).
tcf(c_65789,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 != sK170 ) ),
inference(resolution_lifted,[status(thm)],[c_458,c_1329]) ).
tcf(c_65790,plain,
! [X0: $i] :
( empty_carrier(sK170)
| ( cast_to_el_of_LattPOSet(sK170,X0) = X0 )
| ~ latt_str(sK170)
| ~ element(X0,the_carrier(sK170)) ),
inference(unflattening,[status(thm)],[c_65789]) ).
tcf(c_65792,plain,
! [X0: $i] :
( ~ element(X0,the_carrier(sK170))
| ( cast_to_el_of_LattPOSet(sK170,X0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_65790,c_459,c_457,c_65790]) ).
tcf(c_65793,plain,
! [X0: $i] :
( ( cast_to_el_of_LattPOSet(sK170,X0) = X0 )
| ~ element(X0,the_carrier(sK170)) ),
inference(renaming,[status(thm)],[c_65792]) ).
tcf(c_81631,plain,
! [X0: $i] :
( ( cast_to_el_of_lattice(sK170,X0) = X0 )
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(prop_impl_just,[status(thm)],[c_65769]) ).
tcf(c_81633,plain,
! [X0: $i] :
( element(cast_to_el_of_lattice(sK170,X0),the_carrier(sK170))
| ~ element(X0,the_carrier(poset_of_lattice(sK170))) ),
inference(prop_impl_just,[status(thm)],[c_65781]) ).
tcf(c_81635,plain,
! [X0: $i] :
( ( cast_to_el_of_LattPOSet(sK170,X0) = X0 )
| ~ element(X0,the_carrier(sK170)) ),
inference(prop_impl_just,[status(thm)],[c_65793]) ).
tcf(c_219654,plain,
cast_to_el_of_lattice(sK170,sK171) = sK171,
inference(superposition,[status(thm)],[c_456,c_81631]) ).
tcf(c_219725,plain,
( ~ latt_element_smaller(sK170,sK171,sK169)
| ~ relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171) ),
inference(demodulation,[status(thm)],[c_454,c_219654]) ).
tcf(c_219726,plain,
( latt_element_smaller(sK170,sK171,sK169)
| relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171) ),
inference(demodulation,[status(thm)],[c_455,c_219654]) ).
tcf(c_219778,plain,
( element(sK171,the_carrier(sK170))
| ~ element(sK171,the_carrier(poset_of_lattice(sK170))) ),
inference(superposition,[status(thm)],[c_219654,c_81633]) ).
tcf(c_219780,plain,
element(sK171,the_carrier(sK170)),
inference(forward_subsumption_resolution,[status(thm)],[c_219778,c_456]) ).
tcf(c_219811,plain,
cast_to_el_of_LattPOSet(sK170,sK171) = sK171,
inference(superposition,[status(thm)],[c_219780,c_81635]) ).
tcf(c_221289,plain,
! [X0: $i] :
( latt_element_smaller(sK170,sK171,X0)
| ~ element(sK171,the_carrier(sK170))
| ~ relstr_set_smaller(poset_of_lattice(sK170),X0,sK171) ),
inference(superposition,[status(thm)],[c_219811,c_65088]) ).
tcf(c_221306,plain,
! [X0: $i] :
( relstr_set_smaller(poset_of_lattice(sK170),X0,sK171)
| ~ element(sK171,the_carrier(sK170))
| ~ latt_element_smaller(sK170,sK171,X0) ),
inference(superposition,[status(thm)],[c_219811,c_65073]) ).
tcf(c_221307,plain,
! [X0: $i] :
( relstr_set_smaller(poset_of_lattice(sK170),X0,sK171)
| ~ latt_element_smaller(sK170,sK171,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_221306,c_219780]) ).
tcf(c_221311,plain,
! [X0: $i] :
( latt_element_smaller(sK170,sK171,X0)
| ~ relstr_set_smaller(poset_of_lattice(sK170),X0,sK171) ),
inference(forward_subsumption_resolution,[status(thm)],[c_221289,c_219780]) ).
tcf(c_221411,plain,
relstr_set_smaller(poset_of_lattice(sK170),sK169,sK171),
inference(backward_subsumption_resolution,[status(thm)],[c_219726,c_221307]) ).
tcf(c_221412,plain,
~ latt_element_smaller(sK170,sK171,sK169),
inference(backward_subsumption_resolution,[status(thm)],[c_219725,c_221307]) ).
tcf(c_221438,plain,
latt_element_smaller(sK170,sK171,sK169),
inference(superposition,[status(thm)],[c_221411,c_221311]) ).
tcf(c_221440,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_221438,c_221412]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/10.38 % Computer : n017.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Thu Sep 24 13:43:45 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/10.42 Running first-order theorem proving
% 0.14/10.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/10.43
% 0.14/10.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/10.43
% 0.14/10.43 % Detected problem language: tptp
% 0.14/10.44 % Proving...
% 62.24/25.44 % SZS status Started for theBenchmark.p
% 62.24/25.44 % SZS status Theorem for theBenchmark.p
% 62.24/25.44
% 62.24/25.44 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 62.24/25.44
% 62.24/25.44 % ------ iProver source info
% 62.24/25.44
% 62.24/25.44 % git: date: 2026-07-19 20:42:38 +0200
% 62.24/25.44 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 62.24/25.44 % git: non_committed_changes: false
% 62.24/25.44
% 62.24/25.44 % ------ Parsing...
% 62.24/25.44 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 62.24/25.44
% 62.24/25.44 % ------ Preprocessing... sup_sim: 108 sf_s rm: 76 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 32 sf_s rm: 20 0s sf_e pe_s pe_e %
% 62.24/25.44
% 62.24/25.44 % ------ Preprocessing... gs_s sp: 18 0s gs_e snvd_s sp: 0 0s snvd_e %
% 62.24/25.44
% 62.24/25.44 % ------ Preprocessing... sf_s rm: 7 0s sf_e sf_s rm: 0 0s sf_e
% 62.24/25.44 % ------ Proving...
% 62.24/25.44 % ------ Problem Properties
% 62.24/25.44
% 62.24/25.44 %
% 62.24/25.44 % clauses 1460
% 62.24/25.44 % conjectures 5
% 62.24/25.44 % EPR 202
% 62.24/25.44 % Horn 1068
% 62.24/25.44 % unary 203
% 62.24/25.44 % binary 389
% 62.24/25.44 % lits 4515
% 62.24/25.44 % lits eq 602
% 62.24/25.44 % fd_pure 0
% 62.24/25.44 % fd_pseudo 0
% 62.24/25.44 % fd_cond 46
% 62.24/25.44 % fd_pseudo_cond 126
% 62.24/25.44 % AC symbols 0
% 62.24/25.44
% 62.24/25.44 % ------ Schedule dynamic 5 is on
% 62.24/25.44
% 62.24/25.44 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 62.24/25.44
% 62.24/25.44
% 62.24/25.44 % ------
% 62.24/25.44 % Current options:
% 62.24/25.44 % ------
% 62.24/25.44
% 62.24/25.44
% 62.24/25.44 %
% 62.24/25.44
% 62.24/25.44 % ------ Proving...
% 62.24/25.44 %
% 62.24/25.44
% 62.24/25.44 % SZS status Theorem for theBenchmark.p
% 62.24/25.44
% 62.24/25.44 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 62.24/25.44
% 62.24/25.44
%------------------------------------------------------------------------------