%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU369+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 08:41:48 AM UTC 2026
% Result : Theorem 59.15s 9.10s
% Output : CNFRefutation 59.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 14
% Syntax : Number of formulae : 104 ( 23 unt; 0 def)
% Number of atoms : 358 ( 34 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 439 ( 185 ~; 199 |; 31 &)
% ( 6 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 114 ( 10 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v1_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> ( 'strict$urel$ustr'(X0)
=> X0 = 'rel$ustr$uof'('the$ucarrier'(X0),'the$uInternalRel'(X0)) ) ) ).
fof(d2_lattice3,axiom,
! [X0] :
( ( 'latt$ustr'(X0)
& lattice(X0)
& ~ 'empty$ucarrier'(X0) )
=> 'poset$uof$ulattice'(X0) = 'rel$ustr$uof'('the$ucarrier'(X0),'k2$ulattice3'(X0)) ) ).
fof(d2_yellow_1,axiom,
! [X0] : 'boole$uPOSet'(X0) = 'poset$uof$ulattice'('boole$ulattice'(X0)) ).
fof(d3_lattice3,axiom,
! [X0] :
( ( 'latt$ustr'(X0)
& lattice(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> 'cast$uto$uel$uof$uLattPOSet'(X0,X1) = X1 ) ) ).
fof(dt_k1_lattice3,axiom,
! [X0] :
( 'latt$ustr'('boole$ulattice'(X0))
& 'strict$ulatt$ustr'('boole$ulattice'(X0)) ) ).
fof(dt_k3_yellow_1,axiom,
! [X0] :
( 'rel$ustr'('boole$uPOSet'(X0))
& 'strict$urel$ustr'('boole$uPOSet'(X0)) ) ).
fof(dt_u1_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> 'relation$uof2$uas$usubset'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0)) ) ).
fof(fc1_knaster,axiom,
! [X0] :
( 'complete$ulatt$ustr'('boole$ulattice'(X0))
& 'boolean$ulattstr'('boole$ulattice'(X0))
& 'complemented$ulattstr'('boole$ulattice'(X0))
& 'bounded$ulattstr'('boole$ulattice'(X0))
& 'upper$ubounded$usemilattstr'('boole$ulattice'(X0))
& 'lower$ubounded$usemilattstr'('boole$ulattice'(X0))
& 'modular$ulattstr'('boole$ulattice'(X0))
& 'distributive$ulattstr'('boole$ulattice'(X0))
& lattice('boole$ulattice'(X0))
& 'join$uabsorbing'('boole$ulattice'(X0))
& 'meet$uabsorbing'('boole$ulattice'(X0))
& 'meet$uassociative'('boole$ulattice'(X0))
& 'meet$ucommutative'('boole$ulattice'(X0))
& 'join$uassociative'('boole$ulattice'(X0))
& 'join$ucommutative'('boole$ulattice'(X0))
& 'strict$ulatt$ustr'('boole$ulattice'(X0))
& ~ 'empty$ucarrier'('boole$ulattice'(X0)) ) ).
fof(free_g1_orders_2,axiom,
! [X0,X1] :
( 'relation$uof2'(X1,X0,X0)
=> ! [X2,X3] :
( 'rel$ustr$uof'(X0,X1) = 'rel$ustr$uof'(X2,X3)
=> ( X1 = X3
& X0 = X2 ) ) ) ).
fof(redefinition_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
<=> 'relation$uof2'(X2,X0,X1) ) ).
fof(redefinition_r3_lattices,axiom,
! [X0,X1,X2] :
( ( element(X2,'the$ucarrier'(X0))
& element(X1,'the$ucarrier'(X0))
& 'latt$ustr'(X0)
& 'join$uabsorbing'(X0)
& 'meet$uabsorbing'(X0)
& 'meet$ucommutative'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ( 'below$urefl'(X0,X1,X2)
<=> below(X0,X1,X2) ) ) ).
fof(t2_lattice3,axiom,
! [X0,X1] :
( element(X1,'the$ucarrier'('boole$ulattice'(X0)))
=> ! [X2] :
( element(X2,'the$ucarrier'('boole$ulattice'(X0)))
=> ( below('boole$ulattice'(X0),X1,X2)
<=> subset(X1,X2) ) ) ) ).
fof(t7_lattice3,axiom,
! [X0] :
( ( 'latt$ustr'(X0)
& lattice(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> ! [X2] :
( element(X2,'the$ucarrier'(X0))
=> ( 'below$urefl'(X0,X1,X2)
<=> 'related$ureflexive'('poset$uof$ulattice'(X0),'cast$uto$uel$uof$uLattPOSet'(X0,X1),'cast$uto$uel$uof$uLattPOSet'(X0,X2)) ) ) ) ) ).
fof(t2_yellow_1,conjecture,
! [X0,X1] :
( element(X1,'the$ucarrier'('boole$uPOSet'(X0)))
=> ! [X2] :
( element(X2,'the$ucarrier'('boole$uPOSet'(X0)))
=> ( 'related$ureflexive'('boole$uPOSet'(X0),X1,X2)
<=> subset(X1,X2) ) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1] :
( element(X1,'the$ucarrier'('boole$uPOSet'(X0)))
=> ! [X2] :
( element(X2,'the$ucarrier'('boole$uPOSet'(X0)))
=> ( 'related$ureflexive'('boole$uPOSet'(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
inference(negate_conjecture,[status(cth)],[t2_yellow_1]) ).
cnf(c0,plain,
( ~ 'strict$urel$ustr'(X0)
| 'rel$ustr$uof'('the$ucarrier'(X0),'the$uInternalRel'(X0)) = X0
| ~ 'rel$ustr'(X0) ),
inference(clausification,[status(esa)],[abstractness_v1_orders_2]) ).
cnf(c67,plain,
( 'rel$ustr$uof'('the$ucarrier'(X0),'k2$ulattice3'(X0)) = 'poset$uof$ulattice'(X0)
| 'empty$ucarrier'(X0)
| ~ 'latt$ustr'(X0)
| ~ lattice(X0) ),
inference(clausification,[status(esa)],[d2_lattice3]) ).
cnf(c68,plain,
'poset$uof$ulattice'('boole$ulattice'(X0)) = 'boole$uPOSet'(X0),
inference(clausification,[status(esa)],[d2_yellow_1]) ).
cnf(c69,plain,
( 'empty$ucarrier'(X1)
| ~ lattice(X1)
| 'cast$uto$uel$uof$uLattPOSet'(X1,X0) = X0
| ~ 'latt$ustr'(X1)
| ~ element(X0,'the$ucarrier'(X1)) ),
inference(clausification,[status(esa)],[d3_lattice3]) ).
cnf(c78,plain,
'latt$ustr'('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[dt_k1_lattice3]) ).
cnf(c91,plain,
'strict$urel$ustr'('boole$uPOSet'(X0)),
inference(clausification,[status(esa)],[dt_k3_yellow_1]) ).
cnf(c92,plain,
'rel$ustr'('boole$uPOSet'(X0)),
inference(clausification,[status(esa)],[dt_k3_yellow_1]) ).
cnf(c104,plain,
( 'relation$uof2$uas$usubset'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0))
| ~ 'rel$ustr'(X0) ),
inference(clausification,[status(esa)],[dt_u1_orders_2]) ).
cnf(c116,plain,
~ 'empty$ucarrier'('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[fc1_knaster]) ).
cnf(c118,plain,
'meet$ucommutative'('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[fc1_knaster]) ).
cnf(c119,plain,
'meet$uabsorbing'('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[fc1_knaster]) ).
cnf(c120,plain,
lattice('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[fc1_knaster]) ).
cnf(c129,plain,
'join$uabsorbing'('boole$ulattice'(X0)),
inference(clausification,[status(esa)],[fc1_knaster]) ).
cnf(c243,plain,
( X2 = X1
| 'rel$ustr$uof'(X2,X3) != 'rel$ustr$uof'(X1,X0)
| ~ 'relation$uof2'(X0,X1,X1) ),
inference(clausification,[status(esa)],[free_g1_orders_2]) ).
cnf(c379,plain,
( 'relation$uof2'(X0,X1,X2)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c381,plain,
( ~ 'latt$ustr'(X0)
| ~ 'below$urefl'(X0,X2,X1)
| below(X0,X2,X1)
| 'empty$ucarrier'(X0)
| ~ element(X2,'the$ucarrier'(X0))
| ~ 'join$uabsorbing'(X0)
| ~ 'meet$ucommutative'(X0)
| ~ element(X1,'the$ucarrier'(X0))
| ~ 'meet$uabsorbing'(X0) ),
inference(clausification,[status(esa)],[redefinition_r3_lattices]) ).
cnf(c382,plain,
( 'below$urefl'(X0,X2,X1)
| ~ 'meet$uabsorbing'(X0)
| ~ element(X2,'the$ucarrier'(X0))
| ~ 'join$uabsorbing'(X0)
| ~ 'latt$ustr'(X0)
| ~ below(X0,X2,X1)
| ~ 'meet$ucommutative'(X0)
| ~ element(X1,'the$ucarrier'(X0))
| 'empty$ucarrier'(X0) ),
inference(clausification,[status(esa)],[redefinition_r3_lattices]) ).
cnf(c389,plain,
( subset(X0,X2)
| ~ below('boole$ulattice'(X1),X0,X2)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X1)))
| ~ element(X0,'the$ucarrier'('boole$ulattice'(X1))) ),
inference(clausification,[status(esa)],[t2_lattice3]) ).
cnf(c390,plain,
( ~ subset(X0,X2)
| below('boole$ulattice'(X1),X0,X2)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X1)))
| ~ element(X0,'the$ucarrier'('boole$ulattice'(X1))) ),
inference(clausification,[status(esa)],[t2_lattice3]) ).
cnf(c398,plain,
( ~ 'below$urefl'(X0,X1,X2)
| ~ element(X2,'the$ucarrier'(X0))
| 'empty$ucarrier'(X0)
| ~ element(X1,'the$ucarrier'(X0))
| ~ lattice(X0)
| 'related$ureflexive'('poset$uof$ulattice'(X0),'cast$uto$uel$uof$uLattPOSet'(X0,X1),'cast$uto$uel$uof$uLattPOSet'(X0,X2))
| ~ 'latt$ustr'(X0) ),
inference(clausification,[status(esa)],[t7_lattice3]) ).
cnf(c399,plain,
( 'below$urefl'(X0,X1,X2)
| 'empty$ucarrier'(X0)
| ~ element(X1,'the$ucarrier'(X0))
| ~ element(X2,'the$ucarrier'(X0))
| ~ lattice(X0)
| ~ 'latt$ustr'(X0)
| ~ 'related$ureflexive'('poset$uof$ulattice'(X0),'cast$uto$uel$uof$uLattPOSet'(X0,X1),'cast$uto$uel$uof$uLattPOSet'(X0,X2)) ),
inference(clausification,[status(esa)],[t7_lattice3]) ).
cnf(c401,plain,
element(sK186,'the$ucarrier'('boole$uPOSet'(sK185))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c402,plain,
element(sK187,'the$ucarrier'('boole$uPOSet'(sK185))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c404,plain,
( subset(sK186,sK187)
| 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c405,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187)
| ~ subset(sK186,sK187) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( 'below$urefl'('boole$ulattice'(X0),X1,X2)
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| 'empty$ucarrier'('boole$ulattice'(X0))
| ~ lattice('boole$ulattice'(X0))
| ~ 'latt$ustr'('boole$ulattice'(X0))
| ~ 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2)) ),
inference(superposition,[status(thm)],[c68,c399]) ).
cnf(d1,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1))
| 'below$urefl'('boole$ulattice'(X0),X2,X1)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| 'empty$ucarrier'('boole$ulattice'(X0))
| ~ lattice('boole$ulattice'(X0)) ),
inference(resolution,[status(thm)],[c78,d0]) ).
cnf(d2,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2))
| 'below$urefl'('boole$ulattice'(X0),X1,X2)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| ~ lattice('boole$ulattice'(X0)) ),
inference(resolution,[status(thm)],[c116,d1]) ).
cnf(d3,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X1),X2),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X1),X0))
| 'below$urefl'('boole$ulattice'(X1),X2,X0)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X1)))
| ~ element(X0,'the$ucarrier'('boole$ulattice'(X1))) ),
inference(resolution,[status(thm)],[c120,d2]) ).
cnf(d4,plain,
( ~ 'rel$ustr'(X0)
| 'relation$uof2'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0)) ),
inference(resolution,[status(thm)],[c379,c104]) ).
cnf(d5,plain,
( ~ 'strict$urel$ustr'('boole$uPOSet'(X0))
| 'rel$ustr$uof'('the$ucarrier'('boole$uPOSet'(X0)),'the$uInternalRel'('boole$uPOSet'(X0))) = 'boole$uPOSet'(X0) ),
inference(resolution,[status(thm)],[c92,c0]) ).
cnf(d6,plain,
'rel$ustr$uof'('the$ucarrier'('boole$uPOSet'(X0)),'the$uInternalRel'('boole$uPOSet'(X0))) = 'boole$uPOSet'(X0),
inference(resolution,[status(thm)],[c91,d5]) ).
cnf(d7,plain,
( ~ 'relation$uof2'('the$uInternalRel'('boole$uPOSet'(X0)),'the$ucarrier'('boole$uPOSet'(X0)),'the$ucarrier'('boole$uPOSet'(X0)))
| X1 = 'the$ucarrier'('boole$uPOSet'(X0))
| 'rel$ustr$uof'(X1,X2) != 'boole$uPOSet'(X0) ),
inference(superposition,[status(thm)],[d6,c243]) ).
cnf(d8,plain,
( 'empty$ucarrier'('boole$ulattice'(X0))
| ~ 'latt$ustr'('boole$ulattice'(X0))
| 'rel$ustr$uof'('the$ucarrier'('boole$ulattice'(X0)),'k2$ulattice3'('boole$ulattice'(X0))) = 'poset$uof$ulattice'('boole$ulattice'(X0)) ),
inference(resolution,[status(thm)],[c67,c120]) ).
cnf(d9,plain,
( 'empty$ucarrier'('boole$ulattice'(X0))
| ~ 'latt$ustr'('boole$ulattice'(X0))
| 'rel$ustr$uof'('the$ucarrier'('boole$ulattice'(X0)),'k2$ulattice3'('boole$ulattice'(X0))) = 'boole$uPOSet'(X0) ),
inference(demodulation,[status(thm)],[d8,c68]) ).
cnf(d10,plain,
( 'empty$ucarrier'('boole$ulattice'(X0))
| 'rel$ustr$uof'('the$ucarrier'('boole$ulattice'(X0)),'k2$ulattice3'('boole$ulattice'(X0))) = 'boole$uPOSet'(X0) ),
inference(resolution,[status(thm)],[c78,d9]) ).
cnf(d11,plain,
'rel$ustr$uof'('the$ucarrier'('boole$ulattice'(X0)),'k2$ulattice3'('boole$ulattice'(X0))) = 'boole$uPOSet'(X0),
inference(resolution,[status(thm)],[c116,d10]) ).
cnf(d12,plain,
( ~ 'relation$uof2'('the$uInternalRel'('boole$uPOSet'(X1)),'the$ucarrier'('boole$uPOSet'(X1)),'the$ucarrier'('boole$uPOSet'(X1)))
| 'the$ucarrier'('boole$ulattice'(X0)) = 'the$ucarrier'('boole$uPOSet'(X1))
| 'boole$uPOSet'(X0) != 'boole$uPOSet'(X1) ),
inference(superposition,[status(thm)],[d11,d7]) ).
cnf(d13,plain,
( ~ 'relation$uof2'('the$uInternalRel'('boole$uPOSet'(X0)),'the$ucarrier'('boole$uPOSet'(X0)),'the$ucarrier'('boole$uPOSet'(X0)))
| 'the$ucarrier'('boole$ulattice'(X0)) = 'the$ucarrier'('boole$uPOSet'(X0)) ),
inference(equality_resolution,[status(thm)],[d12]) ).
cnf(d14,plain,
( ~ 'rel$ustr'('boole$uPOSet'(X0))
| 'the$ucarrier'('boole$ulattice'(X0)) = 'the$ucarrier'('boole$uPOSet'(X0)) ),
inference(resolution,[status(thm)],[d13,d4]) ).
cnf(d15,plain,
'the$ucarrier'('boole$ulattice'(X0)) = 'the$ucarrier'('boole$uPOSet'(X0)),
inference(resolution,[status(thm)],[c92,d14]) ).
cnf(d16,plain,
element(sK186,'the$ucarrier'('boole$ulattice'(sK185))),
inference(demodulation,[status(thm)],[c401,d15]) ).
cnf(d17,plain,
( 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ lattice('boole$ulattice'(sK185))
| ~ 'latt$ustr'('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK186) = sK186 ),
inference(resolution,[status(thm)],[d16,c69]) ).
cnf(d18,plain,
( 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ lattice('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK186) = sK186 ),
inference(resolution,[status(thm)],[c78,d17]) ).
cnf(d19,plain,
( ~ lattice('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK186) = sK186 ),
inference(resolution,[status(thm)],[c116,d18]) ).
cnf(d20,plain,
'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK186) = sK186,
inference(resolution,[status(thm)],[c120,d19]) ).
cnf(d21,plain,
( 'below$urefl'('boole$ulattice'(sK185),sK186,X0)
| ~ element(X0,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'related$ureflexive'('boole$uPOSet'(sK185),sK186,'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),X0)) ),
inference(superposition,[status(thm)],[d20,d3]) ).
cnf(d22,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(sK185),sK186,'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),X0))
| 'below$urefl'('boole$ulattice'(sK185),sK186,X0)
| ~ element(X0,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,d21]) ).
cnf(d23,plain,
element(sK187,'the$ucarrier'('boole$ulattice'(sK185))),
inference(demodulation,[status(thm)],[c402,d15]) ).
cnf(d24,plain,
( 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ lattice('boole$ulattice'(sK185))
| ~ 'latt$ustr'('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK187) = sK187 ),
inference(resolution,[status(thm)],[d23,c69]) ).
cnf(d25,plain,
( 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ lattice('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK187) = sK187 ),
inference(resolution,[status(thm)],[c78,d24]) ).
cnf(d26,plain,
( ~ lattice('boole$ulattice'(sK185))
| 'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK187) = sK187 ),
inference(resolution,[status(thm)],[c116,d25]) ).
cnf(d27,plain,
'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),sK187) = sK187,
inference(resolution,[status(thm)],[c120,d26]) ).
cnf(d28,plain,
( 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187) ),
inference(superposition,[status(thm)],[d27,d22]) ).
cnf(d29,plain,
( ~ 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187) ),
inference(resolution,[status(thm)],[d23,d28]) ).
cnf(d30,plain,
( subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187) ),
inference(resolution,[status(thm)],[d29,c404]) ).
cnf(d31,plain,
( ~ 'below$urefl'('boole$ulattice'(X0),X1,X2)
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| 'empty$ucarrier'('boole$ulattice'(X0))
| ~ lattice('boole$ulattice'(X0))
| ~ 'latt$ustr'('boole$ulattice'(X0))
| 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2)) ),
inference(superposition,[status(thm)],[c68,c398]) ).
cnf(d32,plain,
( 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1))
| ~ 'below$urefl'('boole$ulattice'(X0),X2,X1)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| 'empty$ucarrier'('boole$ulattice'(X0))
| ~ lattice('boole$ulattice'(X0)) ),
inference(resolution,[status(thm)],[c78,d31]) ).
cnf(d33,plain,
( 'related$ureflexive'('boole$uPOSet'(X0),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X0),X2))
| ~ 'below$urefl'('boole$ulattice'(X0),X1,X2)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X0)))
| ~ element(X1,'the$ucarrier'('boole$ulattice'(X0)))
| ~ lattice('boole$ulattice'(X0)) ),
inference(resolution,[status(thm)],[c116,d32]) ).
cnf(d34,plain,
( 'related$ureflexive'('boole$uPOSet'(X1),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X1),X2),'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(X1),X0))
| ~ 'below$urefl'('boole$ulattice'(X1),X2,X0)
| ~ element(X2,'the$ucarrier'('boole$ulattice'(X1)))
| ~ element(X0,'the$ucarrier'('boole$ulattice'(X1))) ),
inference(resolution,[status(thm)],[c120,d33]) ).
cnf(d35,plain,
( ~ 'below$urefl'('boole$ulattice'(sK185),sK186,X0)
| ~ element(X0,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| 'related$ureflexive'('boole$uPOSet'(sK185),sK186,'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),X0)) ),
inference(superposition,[status(thm)],[d20,d34]) ).
cnf(d36,plain,
( 'related$ureflexive'('boole$uPOSet'(sK185),sK186,'cast$uto$uel$uof$uLattPOSet'('boole$ulattice'(sK185),X0))
| ~ 'below$urefl'('boole$ulattice'(sK185),sK186,X0)
| ~ element(X0,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,d35]) ).
cnf(d37,plain,
( ~ 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187) ),
inference(superposition,[status(thm)],[d27,d36]) ).
cnf(d38,plain,
( 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187)
| ~ 'below$urefl'('boole$ulattice'(sK185),sK186,sK187) ),
inference(resolution,[status(thm)],[d23,d37]) ).
cnf(d39,plain,
( ~ subset(sK186,X0)
| below('boole$ulattice'(sK185),sK186,X0)
| ~ element(X0,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,c390]) ).
cnf(d40,plain,
( ~ subset(sK186,sK187)
| below('boole$ulattice'(sK185),sK186,sK187) ),
inference(resolution,[status(thm)],[d39,d23]) ).
cnf(d41,plain,
( 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185))
| 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ 'latt$ustr'('boole$ulattice'(sK185))
| ~ subset(sK186,sK187) ),
inference(resolution,[status(thm)],[d40,c382]) ).
cnf(d42,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185))
| 'empty$ucarrier'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c78,d41]) ).
cnf(d43,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c116,d42]) ).
cnf(d44,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c118,d43]) ).
cnf(d45,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c119,d44]) ).
cnf(d46,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[c129,d45]) ).
cnf(d47,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,d46]) ).
cnf(d48,plain,
( ~ subset(sK186,sK187)
| 'below$urefl'('boole$ulattice'(sK185),sK186,sK187) ),
inference(resolution,[status(thm)],[d23,d47]) ).
cnf(d49,plain,
( 'related$ureflexive'('boole$uPOSet'(sK185),sK186,sK187)
| ~ subset(sK186,sK187) ),
inference(resolution,[status(thm)],[d48,d38]) ).
cnf(d50,plain,
( ~ subset(sK186,sK187)
| ~ subset(sK186,sK187) ),
inference(resolution,[status(thm)],[d49,c405]) ).
cnf(d51,plain,
'below$urefl'('boole$ulattice'(sK185),sK186,sK187),
inference(resolution,[status(thm)],[d50,d30]) ).
cnf(d52,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185))
| 'empty$ucarrier'('boole$ulattice'(sK185))
| ~ 'latt$ustr'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[d51,c381]) ).
cnf(d53,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185))
| 'empty$ucarrier'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c78,d52]) ).
cnf(d54,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$ucommutative'('boole$ulattice'(sK185))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c116,d53]) ).
cnf(d55,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'meet$uabsorbing'('boole$ulattice'(sK185))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c118,d54]) ).
cnf(d56,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ 'join$uabsorbing'('boole$ulattice'(sK185)) ),
inference(resolution,[status(thm)],[c119,d55]) ).
cnf(d57,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[c129,d56]) ).
cnf(d58,plain,
( below('boole$ulattice'(sK185),sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,d57]) ).
cnf(d59,plain,
below('boole$ulattice'(sK185),sK186,sK187),
inference(resolution,[status(thm)],[d23,d58]) ).
cnf(d60,plain,
( subset(sK186,sK187)
| ~ element(sK186,'the$ucarrier'('boole$ulattice'(sK185)))
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d59,c389]) ).
cnf(d61,plain,
( subset(sK186,sK187)
| ~ element(sK187,'the$ucarrier'('boole$ulattice'(sK185))) ),
inference(resolution,[status(thm)],[d16,d60]) ).
cnf(d62,plain,
subset(sK186,sK187),
inference(resolution,[status(thm)],[d23,d61]) ).
cnf(d63,plain,
$false,
inference(resolution,[status(thm)],[d50,d62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU369+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n001.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 : Sat Sep 26 09:26:42 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 59.15/9.10 % SZS status Theorem for theBenchmark.p
% 59.15/9.10 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------