%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 02:20:15 PM UTC 2026
% Result : Theorem 2.89s 0.86s
% Output : CNFRefutation 2.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 31
% Syntax : Number of formulae : 141 ( 17 unt; 23 def)
% Number of atoms : 516 ( 21 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 624 ( 249 ~; 272 |; 60 &)
% ( 29 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 24 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 115 ( 104 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> cast_to_el_of_LattPOSet(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(poset_of_lattice(A)))
=> cast_to_el_of_lattice(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,axiom,
! [A,B] :
( ( element(B,the_carrier(poset_of_lattice(A)))
& latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> element(cast_to_el_of_lattice(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f369,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f372,axiom,
? [A] :
( lattice(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f524,lemma,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_element_smaller(poset_of_lattice(B),A,C)
<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f532,lemma,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(B))
=> ( latt_element_smaller(B,C,A)
<=> relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f535,conjecture,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_set_smaller(poset_of_lattice(B),A,C)
<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f536,negated_conjecture,
~ ! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(B) )
=> ! [C] :
( element(C,the_carrier(poset_of_lattice(B)))
=> ( relstr_set_smaller(poset_of_lattice(B),A,C)
<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f535]) ).
fof(f1163,plain,
! [A] :
( ! [B] :
( cast_to_el_of_LattPOSet(A,B) = B
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f1164,plain,
! [X0,X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f1163]) ).
fof(f1219,plain,
! [A] :
( ! [B] :
( cast_to_el_of_lattice(A,B) = B
| ~ element(B,the_carrier(poset_of_lattice(A))) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f1220,plain,
! [X0,X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f1219]) ).
fof(f1521,plain,
! [A,B] :
( element(cast_to_el_of_lattice(A,B),the_carrier(A))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f191]) ).
fof(f1522,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f1521]) ).
fof(f2131,plain,
( strict_latt_str(sK166_skl)
& ~ empty_carrier(sK166_skl)
& latt_str(sK166_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK166_skl]),skolemize(A,sK166_skl)],[f369]) ).
fof(f2133,plain,
~ empty_carrier(sK166_skl),
inference(cnf_transformation,[status(thm)],[f2131]) ).
fof(f2144,plain,
( lattice(sK169_skl)
& join_absorbing(sK169_skl)
& meet_absorbing(sK169_skl)
& meet_associative(sK169_skl)
& meet_commutative(sK169_skl)
& join_associative(sK169_skl)
& join_commutative(sK169_skl)
& strict_latt_str(sK169_skl)
& ~ empty_carrier(sK169_skl)
& latt_str(sK169_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK169_skl]),skolemize(A,sK169_skl)],[f372]) ).
fof(f2145,plain,
latt_str(sK169_skl),
inference(cnf_transformation,[status(thm)],[f2144]) ).
fof(f2146,plain,
~ empty_carrier(sK169_skl),
inference(cnf_transformation,[status(thm)],[f2144]) ).
fof(f2154,plain,
lattice(sK169_skl),
inference(cnf_transformation,[status(thm)],[f2144]) ).
fof(f2963,plain,
! [A,B] :
( ! [C] :
( ( relstr_element_smaller(poset_of_lattice(B),A,C)
<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) )
| ~ element(C,the_carrier(poset_of_lattice(B))) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(pre_NNF_transformation,[status(thm)],[f524]) ).
fof(f2964,plain,
! [A,B] :
( ! [C] :
( ( ( ~ latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
| relstr_element_smaller(poset_of_lattice(B),A,C) )
& ( latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
| ~ relstr_element_smaller(poset_of_lattice(B),A,C) ) )
| ~ element(C,the_carrier(poset_of_lattice(B))) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(NNF_transformation,[status(thm)],[f2963]) ).
fof(f2965,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ~ latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
| relstr_element_smaller(poset_of_lattice(B),A,C) )
& ! [A] :
( latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)
| ~ relstr_element_smaller(poset_of_lattice(B),A,C) ) )
| ~ element(C,the_carrier(poset_of_lattice(B))) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(miniscoping,[status(thm)],[f2964]) ).
fof(f2967,plain,
! [X0,X1,X2] :
( ~ latt_set_smaller(X0,cast_to_el_of_lattice(X0,X1),X2)
| relstr_element_smaller(poset_of_lattice(X0),X2,X1)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f2965]) ).
fof(f2986,plain,
! [A,B] :
( ! [C] :
( ( latt_element_smaller(B,C,A)
<=> relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) )
| ~ element(C,the_carrier(B)) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(pre_NNF_transformation,[status(thm)],[f532]) ).
fof(f2987,plain,
! [A,B] :
( ! [C] :
( ( ( ~ relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_element_smaller(B,C,A) )
& ( relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_element_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B)) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(NNF_transformation,[status(thm)],[f2986]) ).
fof(f2988,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ~ relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| latt_element_smaller(B,C,A) )
& ! [A] :
( relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))
| ~ latt_element_smaller(B,C,A) ) )
| ~ element(C,the_carrier(B)) )
| ~ latt_str(B)
| ~ lattice(B)
| empty_carrier(B) ),
inference(miniscoping,[status(thm)],[f2987]) ).
fof(f2989,plain,
! [X0,X1,X2] :
( relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| ~ latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f2988]) ).
fof(f2990,plain,
! [X0,X1,X2] :
( ~ relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))
| latt_element_smaller(X0,X1,X2)
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f2988]) ).
fof(f2999,plain,
? [A,B] :
( ? [C] :
( ( relstr_set_smaller(poset_of_lattice(B),A,C)
<~> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) )
& element(C,the_carrier(poset_of_lattice(B))) )
& latt_str(B)
& lattice(B)
& ~ empty_carrier(B) ),
inference(pre_NNF_transformation,[status(thm)],[f536]) ).
fof(f3000,plain,
? [A,B] :
( ? [C] :
( ( ~ latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
| ~ relstr_set_smaller(poset_of_lattice(B),A,C) )
& ( latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
| relstr_set_smaller(poset_of_lattice(B),A,C) )
& element(C,the_carrier(poset_of_lattice(B))) )
& latt_str(B)
& lattice(B)
& ~ empty_carrier(B) ),
inference(NNF_transformation,[status(thm)],[f2999]) ).
fof(f3001,plain,
? [B] :
( ? [C] :
( ? [A] :
( ( ~ latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
| ~ relstr_set_smaller(poset_of_lattice(B),A,C) )
& ( latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)
| relstr_set_smaller(poset_of_lattice(B),A,C) ) )
& element(C,the_carrier(poset_of_lattice(B))) )
& latt_str(B)
& lattice(B)
& ~ empty_carrier(B) ),
inference(miniscoping,[status(thm)],[f3000]) ).
fof(f3002,plain,
( ( ~ latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) )
& ( latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)
| relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) )
& element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))
& latt_str(sK362_skl)
& lattice(sK362_skl)
& ~ empty_carrier(sK362_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK362_skl,sK363_skl,sK364_skl]),skolemize(B,sK362_skl),skolemize(C,sK363_skl),skolemize(A,sK364_skl)],[f3001]) ).
fof(f3003,plain,
~ empty_carrier(sK362_skl),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f3004,plain,
lattice(sK362_skl),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f3005,plain,
latt_str(sK362_skl),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f3006,plain,
element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl))),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f3007,plain,
( latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)
| relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) ),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f3008,plain,
( ~ latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) ),
inference(cnf_transformation,[status(thm)],[f3002]) ).
fof(f4023,definition,
( sQ31_spl
<=> relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f4025,plain,
( sQ31_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) ),
inference(component_clause,[status(thm)],[f4023]) ).
fof(f4026,definition,
( sQ32_spl
<=> latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f4027,plain,
( ~ sQ32_spl
| latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl) ),
inference(component_clause,[status(thm)],[f4026]) ).
fof(f4028,plain,
( sQ32_spl
| ~ latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl) ),
inference(component_clause,[status(thm)],[f4026]) ).
fof(f4029,plain,
( sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f3007,f4023,f4026]) ).
fof(f4030,plain,
( ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3008,f4023,f4026]) ).
fof(f4478,plain,
! [X0] :
( cast_to_el_of_lattice(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl)))
| ~ latt_str(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f1220,f3004]) ).
fof(f4480,definition,
( sQ63_spl
<=> empty_carrier(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4481,plain,
( ~ sQ63_spl
| empty_carrier(sK362_skl) ),
inference(component_clause,[status(thm)],[f4480]) ).
fof(f4483,definition,
( sQ64_spl
<=> latt_str(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f4485,plain,
( sQ64_spl
| ~ latt_str(sK362_skl) ),
inference(component_clause,[status(thm)],[f4483]) ).
fof(f4486,definition,
! [X0] :
( sQ65_spl
<=> ( cast_to_el_of_lattice(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f4487,plain,
! [X0] :
( ~ sQ65_spl
| cast_to_el_of_lattice(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4486]) ).
fof(f4489,plain,
( sQ65_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4478,f4480,f4483,f4486]) ).
fof(f4490,definition,
( sQ66_spl
<=> lattice(sK362_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f4492,plain,
( sQ66_spl
| ~ lattice(sK362_skl) ),
inference(component_clause,[status(thm)],[f4490]) ).
fof(f4496,plain,
( ~ sQ65_spl
| cast_to_el_of_lattice(sK362_skl,sK363_skl) = sK363_skl ),
inference(resolution,[status(thm)],[f4487,f3006]) ).
fof(f4498,plain,
! [X0] :
( element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl))
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl)))
| ~ latt_str(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f1522,f3004]) ).
fof(f4500,definition,
! [X0] :
( sQ67_spl
<=> ( element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl))
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f4501,plain,
! [X0] :
( ~ sQ67_spl
| element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl))
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4500]) ).
fof(f4503,plain,
( sQ67_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4498,f4480,f4483,f4500]) ).
fof(f4505,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4481,f3003]) ).
fof(f4506,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f4505]) ).
fof(f4507,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4485,f3005]) ).
fof(f4508,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f4507]) ).
fof(f4526,plain,
( sQ32_spl
| ~ sQ65_spl
| ~ latt_element_smaller(sK362_skl,sK363_skl,sK364_skl) ),
inference(forward_demodulation,[status(thm)],[f4496,f4028]) ).
fof(f4528,plain,
! [X0,X1] :
( ~ latt_set_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0),X1)
| relstr_element_smaller(poset_of_lattice(sK362_skl),X1,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl)))
| ~ latt_str(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f2967,f3004]) ).
fof(f4529,definition,
! [X0,X1] :
( sQ72_spl
<=> ( ~ latt_set_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0),X1)
| relstr_element_smaller(poset_of_lattice(sK362_skl),X1,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4532,plain,
( sQ72_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4528,f4480,f4483,f4529]) ).
fof(f4533,plain,
! [X0,X1] :
( ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0))
| latt_element_smaller(sK362_skl,X0,X1)
| ~ element(X0,the_carrier(sK362_skl))
| ~ latt_str(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f2990,f3004]) ).
fof(f4534,definition,
! [X0,X1] :
( sQ73_spl
<=> ( ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0))
| latt_element_smaller(sK362_skl,X0,X1)
| ~ element(X0,the_carrier(sK362_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4535,plain,
! [X0,X1] :
( ~ sQ73_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0))
| latt_element_smaller(sK362_skl,X0,X1)
| ~ element(X0,the_carrier(sK362_skl)) ),
inference(component_clause,[status(thm)],[f4534]) ).
fof(f4537,plain,
( sQ73_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4533,f4480,f4483,f4534]) ).
fof(f4555,plain,
( ~ sQ65_spl
| ~ sQ67_spl
| element(sK363_skl,the_carrier(sK362_skl))
| ~ element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl))) ),
inference(paramodulation,[status(thm)],[f4496,f4501]) ).
fof(f4556,definition,
( sQ78_spl
<=> element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl))) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f4558,plain,
( sQ78_spl
| ~ element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl))) ),
inference(component_clause,[status(thm)],[f4556]) ).
fof(f4559,definition,
( sQ79_spl
<=> element(sK363_skl,the_carrier(sK362_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f4562,plain,
( ~ sQ65_spl
| ~ sQ67_spl
| sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f4555,f4556,f4559,f4500,f4486]) ).
fof(f4563,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4558,f3006]) ).
fof(f4564,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f4563]) ).
fof(f4567,plain,
! [X0,X1] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl)))
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0)))
| latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0),X1) ),
inference(resolution,[status(thm)],[f4535,f4501]) ).
fof(f4570,definition,
( sQ80_spl
<=> empty_carrier(sK166_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f4571,plain,
( ~ sQ80_spl
| empty_carrier(sK166_skl) ),
inference(component_clause,[status(thm)],[f4570]) ).
fof(f4585,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl)))
| latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),X0) ),
inference(resolution,[status(thm)],[f4567,f3006]) ).
fof(f4586,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl)))
| latt_element_smaller(sK362_skl,sK363_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f4496,f4585]) ).
fof(f4587,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,sK363_skl))
| latt_element_smaller(sK362_skl,sK363_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f4496,f4586]) ).
fof(f4588,plain,
( ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4571,f2133]) ).
fof(f4589,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f4588]) ).
fof(f4590,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ latt_element_smaller(sK362_skl,sK363_skl,X0)
| ~ element(sK363_skl,the_carrier(sK362_skl))
| ~ latt_str(sK362_skl)
| ~ lattice(sK362_skl)
| empty_carrier(sK362_skl)
| latt_element_smaller(sK362_skl,sK363_skl,X0) ),
inference(resolution,[status(thm)],[f4587,f2989]) ).
fof(f4591,definition,
! [X0] :
( sQ84_spl
<=> ( ~ latt_element_smaller(sK362_skl,sK363_skl,X0)
| latt_element_smaller(sK362_skl,sK363_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f4594,plain,
( ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ sQ79_spl
| ~ sQ64_spl
| ~ sQ66_spl
| sQ63_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f4590,f4591,f4480,f4490,f4483,f4559,f4486,f4534,f4500]) ).
fof(f4595,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4492,f3004]) ).
fof(f4596,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f4595]) ).
fof(f4599,definition,
( sQ85_spl
<=> empty_carrier(sK169_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f4600,plain,
( ~ sQ85_spl
| empty_carrier(sK169_skl) ),
inference(component_clause,[status(thm)],[f4599]) ).
fof(f4602,definition,
( sQ86_spl
<=> lattice(sK169_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4604,plain,
( sQ86_spl
| ~ lattice(sK169_skl) ),
inference(component_clause,[status(thm)],[f4602]) ).
fof(f4605,definition,
! [X0] :
( sQ87_spl
<=> ( element(cast_to_el_of_lattice(sK169_skl,X0),the_carrier(sK169_skl))
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4609,definition,
! [X0] :
( sQ88_spl
<=> ( cast_to_el_of_lattice(sK169_skl,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f4613,plain,
! [X0,X1] :
( ~ relstr_set_smaller(poset_of_lattice(sK169_skl),X1,cast_to_el_of_LattPOSet(sK169_skl,X0))
| latt_element_smaller(sK169_skl,X0,X1)
| ~ element(X0,the_carrier(sK169_skl))
| ~ latt_str(sK169_skl)
| empty_carrier(sK169_skl) ),
inference(resolution,[status(thm)],[f2154,f2990]) ).
fof(f4614,plain,
! [X0,X1] :
( ~ latt_set_smaller(sK169_skl,cast_to_el_of_lattice(sK169_skl,X0),X1)
| relstr_element_smaller(poset_of_lattice(sK169_skl),X1,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl)))
| ~ latt_str(sK169_skl)
| empty_carrier(sK169_skl) ),
inference(resolution,[status(thm)],[f2154,f2967]) ).
fof(f4615,plain,
! [X0] :
( element(cast_to_el_of_lattice(sK169_skl,X0),the_carrier(sK169_skl))
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl)))
| ~ latt_str(sK169_skl)
| empty_carrier(sK169_skl) ),
inference(resolution,[status(thm)],[f2154,f1522]) ).
fof(f4616,plain,
! [X0] :
( cast_to_el_of_lattice(sK169_skl,X0) = X0
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl)))
| ~ latt_str(sK169_skl)
| empty_carrier(sK169_skl) ),
inference(resolution,[status(thm)],[f2154,f1220]) ).
fof(f4617,definition,
( sQ89_spl
<=> latt_str(sK169_skl) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f4619,plain,
( sQ89_spl
| ~ latt_str(sK169_skl) ),
inference(component_clause,[status(thm)],[f4617]) ).
fof(f4620,definition,
! [X0,X1] :
( sQ90_spl
<=> ( ~ relstr_set_smaller(poset_of_lattice(sK169_skl),X1,cast_to_el_of_LattPOSet(sK169_skl,X0))
| latt_element_smaller(sK169_skl,X0,X1)
| ~ element(X0,the_carrier(sK169_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f4623,plain,
( sQ90_spl
| ~ sQ89_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4613,f4599,f4617,f4620]) ).
fof(f4624,definition,
! [X0,X1] :
( sQ91_spl
<=> ( ~ latt_set_smaller(sK169_skl,cast_to_el_of_lattice(sK169_skl,X0),X1)
| relstr_element_smaller(poset_of_lattice(sK169_skl),X1,X0)
| ~ element(X0,the_carrier(poset_of_lattice(sK169_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f4627,plain,
( sQ91_spl
| ~ sQ89_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4614,f4599,f4617,f4624]) ).
fof(f4628,plain,
( sQ87_spl
| ~ sQ89_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4615,f4599,f4617,f4605]) ).
fof(f4629,plain,
( sQ88_spl
| ~ sQ89_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4616,f4599,f4617,f4609]) ).
fof(f4630,plain,
( sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4619,f2145]) ).
fof(f4631,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f4630]) ).
fof(f4632,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4604,f2154]) ).
fof(f4633,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f4632]) ).
fof(f4634,plain,
( ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4600,f2146]) ).
fof(f4635,plain,
~ sQ85_spl,
inference(contradiction_clause,[status(thm)],[f4634]) ).
fof(f4662,plain,
! [X0] :
( cast_to_el_of_LattPOSet(sK169_skl,X0) = X0
| ~ element(X0,the_carrier(sK169_skl))
| ~ latt_str(sK169_skl)
| empty_carrier(sK169_skl) ),
inference(resolution,[status(thm)],[f1164,f2154]) ).
fof(f4663,plain,
! [X0] :
( cast_to_el_of_LattPOSet(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(sK362_skl))
| ~ latt_str(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(resolution,[status(thm)],[f1164,f3004]) ).
fof(f4665,definition,
! [X0] :
( sQ92_spl
<=> ( cast_to_el_of_LattPOSet(sK169_skl,X0) = X0
| ~ element(X0,the_carrier(sK169_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f4668,plain,
( sQ92_spl
| ~ sQ89_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f4662,f4599,f4617,f4665]) ).
fof(f4669,definition,
! [X0] :
( sQ93_spl
<=> ( cast_to_el_of_LattPOSet(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(sK362_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f4670,plain,
! [X0] :
( ~ sQ93_spl
| cast_to_el_of_LattPOSet(sK362_skl,X0) = X0
| ~ element(X0,the_carrier(sK362_skl)) ),
inference(component_clause,[status(thm)],[f4669]) ).
fof(f4672,plain,
( sQ93_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4663,f4480,f4483,f4669]) ).
fof(f4677,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ93_spl
| ~ element(X0,the_carrier(poset_of_lattice(sK362_skl)))
| cast_to_el_of_LattPOSet(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0)) = cast_to_el_of_lattice(sK362_skl,X0) ),
inference(resolution,[status(thm)],[f4670,f4501]) ).
fof(f4679,plain,
( ~ sQ67_spl
| ~ sQ93_spl
| cast_to_el_of_LattPOSet(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl)) = cast_to_el_of_lattice(sK362_skl,sK363_skl) ),
inference(resolution,[status(thm)],[f4677,f3006]) ).
fof(f4680,plain,
( ~ sQ67_spl
| ~ sQ93_spl
| ~ sQ65_spl
| cast_to_el_of_LattPOSet(sK362_skl,sK363_skl) = cast_to_el_of_lattice(sK362_skl,sK363_skl) ),
inference(forward_demodulation,[status(thm)],[f4496,f4679]) ).
fof(f4681,plain,
( ~ sQ67_spl
| ~ sQ93_spl
| ~ sQ65_spl
| cast_to_el_of_LattPOSet(sK362_skl,sK363_skl) = sK363_skl ),
inference(forward_demodulation,[status(thm)],[f4496,f4680]) ).
fof(f4682,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ sQ93_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)
| latt_element_smaller(sK362_skl,sK363_skl,X0) ),
inference(backward_demodulation,[status(thm)],[f4681,f4587]) ).
fof(f4683,plain,
! [X0] :
( ~ sQ67_spl
| ~ sQ93_spl
| ~ sQ65_spl
| relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)
| ~ latt_element_smaller(sK362_skl,sK363_skl,X0)
| ~ element(sK363_skl,the_carrier(sK362_skl))
| ~ latt_str(sK362_skl)
| ~ lattice(sK362_skl)
| empty_carrier(sK362_skl) ),
inference(paramodulation,[status(thm)],[f4681,f2989]) ).
fof(f4684,definition,
! [X0] :
( sQ94_spl
<=> ( relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)
| ~ latt_element_smaller(sK362_skl,sK363_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f4685,plain,
! [X0] :
( ~ sQ94_spl
| relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)
| ~ latt_element_smaller(sK362_skl,sK363_skl,X0) ),
inference(component_clause,[status(thm)],[f4684]) ).
fof(f4687,plain,
( ~ sQ67_spl
| ~ sQ93_spl
| ~ sQ65_spl
| sQ94_spl
| ~ sQ79_spl
| ~ sQ64_spl
| ~ sQ66_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4683,f4480,f4490,f4483,f4559,f4684,f4486,f4669,f4500]) ).
fof(f4688,plain,
( sQ32_spl
| ~ sQ65_spl
| ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ93_spl
| ~ relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl) ),
inference(resolution,[status(thm)],[f4682,f4526]) ).
fof(f4689,plain,
( sQ32_spl
| ~ sQ65_spl
| ~ sQ67_spl
| ~ sQ73_spl
| ~ sQ93_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f4688,f4023,f4669,f4534,f4500,f4486,f4026]) ).
fof(f4690,plain,
( ~ sQ32_spl
| ~ sQ65_spl
| latt_element_smaller(sK362_skl,sK363_skl,sK364_skl) ),
inference(forward_demodulation,[status(thm)],[f4496,f4027]) ).
fof(f4691,plain,
( ~ sQ94_spl
| sQ31_spl
| ~ latt_element_smaller(sK362_skl,sK363_skl,sK364_skl) ),
inference(resolution,[status(thm)],[f4025,f4685]) ).
fof(f4692,plain,
( ~ sQ94_spl
| sQ31_spl
| ~ sQ32_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4691,f4690]) ).
fof(f4693,plain,
( ~ sQ94_spl
| sQ31_spl
| ~ sQ32_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f4692]) ).
fof(f4694,plain,
$false,
inference(sat_refutation,[status(thm)],[f4029,f4030,f4489,f4503,f4506,f4508,f4532,f4537,f4562,f4564,f4589,f4594,f4596,f4623,f4627,f4628,f4629,f4631,f4633,f4635,f4668,f4672,f4687,f4689,f4693]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:17:51 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 2.89/0.86 % Refutation found
% 2.89/0.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.89/0.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.89/0.89 % Elapsed time: 0.513109 seconds
% 2.89/0.89 % CPU time: 3.476302 seconds
% 2.89/0.89 % Total memory used: 236.079 MB
% 2.89/0.89 % Net memory used: 232.686 MB
%------------------------------------------------------------------------------