%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:52 AM UTC 2026
% Result : Theorem 10.40s 5.96s
% Output : CNFRefutation 10.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 70 ( 19 unt; 0 def)
% Number of atoms : 215 ( 31 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 239 ( 94 ~; 86 |; 44 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 30 ( 28 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 61 ( 7 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(antisymmetry_r2_hidden,axiom,
! [X0,X1] :
( in(X0,X1)
=> ~ in(X1,X0) ) ).
fof(dt_k3_yellow_1,axiom,
! [X0] :
( 'rel$ustr'('boole$uPOSet'(X0))
& 'strict$urel$ustr'('boole$uPOSet'(X0)) ) ).
fof(dt_l1_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> 'one$usorted$ustr'(X0) ) ).
fof(fc12_relat_1,axiom,
( 'relation$uempty$uyielding'('empty$uset')
& relation('empty$uset')
& empty('empty$uset') ) ).
fof(fc1_struct_0,axiom,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ~ empty('the$ucarrier'(X0)) ) ).
fof(fc1_waybel_7,axiom,
! [X0] :
( 'complete$urelstr'('boole$uPOSet'(X0))
& 'with$uinfima$urelstr'('boole$uPOSet'(X0))
& 'with$usuprema$urelstr'('boole$uPOSet'(X0))
& 'boolean$urelstr'('boole$uPOSet'(X0))
& 'complemented$urelstr'('boole$uPOSet'(X0))
& 'heyting$urelstr'('boole$uPOSet'(X0))
& 'distributive$urelstr'('boole$uPOSet'(X0))
& ~ 'v1$uyellow$u3'('boole$uPOSet'(X0))
& 'join$ucomplete$urelstr'('boole$uPOSet'(X0))
& 'up$ucomplete$urelstr'('boole$uPOSet'(X0))
& 'bounded$urelstr'('boole$uPOSet'(X0))
& 'upper$ubounded$urelstr'('boole$uPOSet'(X0))
& 'lower$ubounded$urelstr'('boole$uPOSet'(X0))
& 'antisymmetric$urelstr'('boole$uPOSet'(X0))
& 'transitive$urelstr'('boole$uPOSet'(X0))
& 'reflexive$urelstr'('boole$uPOSet'(X0))
& 'strict$urel$ustr'('boole$uPOSet'(X0))
& ~ 'empty$ucarrier'('boole$uPOSet'(X0)) ) ).
fof(fc2_pre_topc,axiom,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ~ empty('cast$uas$ucarrier$usubset'(X0)) ) ).
fof(t14_yellow19,axiom,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( ( element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
& 'upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& 'filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& ~ empty(X1) )
=> 'set$udifference'(X1,singleton('empty$uset')) = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1)) ) ) ).
fof(t2_subset,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(X1) ) ) ).
fof(t2_yellow19,axiom,
! [X0] :
( ~ empty(X0)
=> ! [X1] :
( ( element(X1,powerset('the$ucarrier'('boole$uPOSet'(X0))))
& 'proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'(X0))))
& 'upper$urelstr$usubset'(X1,'boole$uPOSet'(X0))
& 'filtered$usubset'(X1,'boole$uPOSet'(X0))
& ~ empty(X1) )
=> ! [X2] :
~ ( empty(X2)
& in(X2,X1) ) ) ) ).
fof(t4_subset,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X2))
& in(X0,X1) )
=> element(X0,X2) ) ).
fof(t5_subset,axiom,
! [X0,X1,X2] :
~ ( empty(X2)
& element(X1,powerset(X2))
& in(X0,X1) ) ).
fof(t65_zfmisc_1,axiom,
! [X0,X1] :
( 'set$udifference'(X0,singleton(X1)) = X0
<=> ~ in(X1,X0) ) ).
fof(t15_yellow19,conjecture,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( ( element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
& 'proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
& 'upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& 'filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& ~ empty(X1) )
=> X1 = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1)) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( ( element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
& 'proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
& 'upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& 'filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
& ~ empty(X1) )
=> X1 = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1)) ) ),
inference(negate_conjecture,[status(cth)],[t15_yellow19]) ).
cnf(c2,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[antisymmetry_r2_hidden]) ).
cnf(c69,plain,
'rel$ustr'('boole$uPOSet'(X0)),
inference(clausification,[status(esa)],[dt_k3_yellow_1]) ).
cnf(c70,plain,
( 'one$usorted$ustr'(X0)
| ~ 'rel$ustr'(X0) ),
inference(clausification,[status(esa)],[dt_l1_orders_2]) ).
cnf(c84,plain,
empty('empty$uset'),
inference(clausification,[status(esa)],[fc12_relat_1]) ).
cnf(c97,plain,
( ~ empty('the$ucarrier'(X0))
| ~ 'one$usorted$ustr'(X0)
| 'empty$ucarrier'(X0) ),
inference(clausification,[status(esa)],[fc1_struct_0]) ).
cnf(c99,plain,
~ 'empty$ucarrier'('boole$uPOSet'(X0)),
inference(clausification,[status(esa)],[fc1_waybel_7]) ).
cnf(c120,plain,
( ~ empty('cast$uas$ucarrier$usubset'(X0))
| ~ 'one$usorted$ustr'(X0)
| 'empty$ucarrier'(X0) ),
inference(clausification,[status(esa)],[fc2_pre_topc]) ).
cnf(c371,plain,
( 'set$udifference'(X1,singleton('empty$uset')) = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1))
| 'empty$ucarrier'(X0)
| ~ 'upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
| empty(X1)
| ~ 'filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))
| ~ element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0)))))
| ~ 'one$usorted$ustr'(X0) ),
inference(clausification,[status(esa)],[t14_yellow19]) ).
cnf(c373,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(clausification,[status(esa)],[t2_subset]) ).
cnf(c378,plain,
( ~ empty(X0)
| empty(X2)
| ~ 'upper$urelstr$usubset'(X1,'boole$uPOSet'(X2))
| ~ 'filtered$usubset'(X1,'boole$uPOSet'(X2))
| empty(X1)
| ~ 'proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'(X2))))
| ~ element(X1,powerset('the$ucarrier'('boole$uPOSet'(X2))))
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t2_yellow19]) ).
cnf(c383,plain,
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t4_subset]) ).
cnf(c384,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t5_subset]) ).
cnf(c386,plain,
( in(X1,X0)
| 'set$udifference'(X0,singleton(X1)) = X0 ),
inference(clausification,[status(esa)],[t65_zfmisc_1]) ).
cnf(c390,plain,
~ 'empty$ucarrier'(sK211),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c391,plain,
'one$usorted$ustr'(sK211),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c392,plain,
~ empty(sK212),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c393,plain,
'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c394,plain,
'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c395,plain,
'proper$uelement'(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c396,plain,
element(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c397,plain,
sK212 != 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ element(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))))
| ~ empty(X0)
| empty(sK212)
| empty('cast$uas$ucarrier$usubset'(sK211))
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c378,c395]) ).
cnf(d1,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ element(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))))
| empty('cast$uas$ucarrier$usubset'(sK211))
| ~ empty(X0)
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c392,d0]) ).
cnf(d2,plain,
( ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ element(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))))
| empty('cast$uas$ucarrier$usubset'(sK211))
| ~ empty(X0)
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c393,d1]) ).
cnf(d3,plain,
( ~ element(sK212,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))))
| empty('cast$uas$ucarrier$usubset'(sK211))
| ~ empty(X0)
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c394,d2]) ).
cnf(d4,plain,
( empty('cast$uas$ucarrier$usubset'(sK211))
| ~ empty(X0)
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c396,d3]) ).
cnf(d5,plain,
( 'set$udifference'(sK212,singleton(X0)) = sK212
| empty('cast$uas$ucarrier$usubset'(sK211))
| ~ empty(X0) ),
inference(resolution,[status(thm)],[d4,c386]) ).
cnf(d6,plain,
( empty('cast$uas$ucarrier$usubset'(sK211))
| 'set$udifference'(sK212,singleton('empty$uset')) = sK212 ),
inference(resolution,[status(thm)],[d5,c84]) ).
cnf(d7,plain,
( 'empty$ucarrier'(sK211)
| ~ 'one$usorted$ustr'(sK211)
| 'set$udifference'(sK212,singleton('empty$uset')) = sK212 ),
inference(resolution,[status(thm)],[d6,c120]) ).
cnf(d8,plain,
( ~ 'one$usorted$ustr'(sK211)
| 'set$udifference'(sK212,singleton('empty$uset')) = sK212 ),
inference(resolution,[status(thm)],[c390,d7]) ).
cnf(d9,plain,
'set$udifference'(sK212,singleton('empty$uset')) = sK212,
inference(resolution,[status(thm)],[c391,d8]) ).
cnf(d10,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| empty(sK212)
| 'empty$ucarrier'(sK211)
| ~ 'one$usorted$ustr'(sK211)
| 'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)) ),
inference(resolution,[status(thm)],[c371,c396]) ).
cnf(d11,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| empty(sK212)
| ~ 'one$usorted$ustr'(sK211)
| 'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)) ),
inference(resolution,[status(thm)],[c390,d10]) ).
cnf(d12,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| empty(sK212)
| 'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)) ),
inference(resolution,[status(thm)],[c391,d11]) ).
cnf(d13,plain,
( ~ 'filtered$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| 'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)) ),
inference(resolution,[status(thm)],[c392,d12]) ).
cnf(d14,plain,
( ~ 'upper$urelstr$usubset'(sK212,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| 'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)) ),
inference(resolution,[status(thm)],[c393,d13]) ).
cnf(d15,plain,
'set$udifference'(sK212,singleton('empty$uset')) = 'filter$uof$unet$ustr'(sK211,'net$uof$ubool$ufilter'(sK211,'cast$uas$ucarrier$usubset'(sK211),sK212)),
inference(resolution,[status(thm)],[c394,d14]) ).
cnf(d16,plain,
sK212 != 'set$udifference'(sK212,singleton('empty$uset')),
inference(demodulation,[status(thm)],[c397,d15]) ).
cnf(d17,plain,
sK212 != sK212,
inference(demodulation,[status(thm)],[d16,d9]) ).
cnf(d18,plain,
( ~ empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c384,c396]) ).
cnf(d19,plain,
( element(X0,'the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[c383,c396]) ).
cnf(d20,plain,
( empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| in(X0,'the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[d19,c373]) ).
cnf(d21,plain,
( ~ in('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))),X0)
| empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in(X0,sK212) ),
inference(resolution,[status(thm)],[d20,c2]) ).
cnf(d22,plain,
( empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))),sK212)
| empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))
| ~ in('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))),sK212) ),
inference(resolution,[status(thm)],[d21,d20]) ).
cnf(d23,plain,
( 'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212
| empty('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))) ),
inference(resolution,[status(thm)],[d22,c386]) ).
cnf(d24,plain,
( ~ in(X0,sK212)
| 'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212 ),
inference(resolution,[status(thm)],[d23,d18]) ).
cnf(d25,plain,
( 'set$udifference'(sK212,singleton(X0)) = sK212
| 'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212 ),
inference(resolution,[status(thm)],[d24,c386]) ).
cnf(d26,plain,
( 'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212
| sK212 != sK212 ),
inference(superposition,[status(thm)],[d25,d16]) ).
cnf(d27,plain,
'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212,
inference(equality_resolution,[status(thm)],[d26]) ).
cnf(d28,plain,
( 'empty$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'one$usorted$ustr'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| 'set$udifference'(sK212,singleton('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211))))) = sK212 ),
inference(resolution,[status(thm)],[d23,c97]) ).
cnf(d29,plain,
( 'empty$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| ~ 'one$usorted$ustr'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| sK212 = sK212 ),
inference(demodulation,[status(thm)],[d28,d27]) ).
cnf(d30,plain,
( ~ 'one$usorted$ustr'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK211)))
| sK212 = sK212 ),
inference(resolution,[status(thm)],[c99,d29]) ).
cnf(d31,plain,
'one$usorted$ustr'('boole$uPOSet'(X0)),
inference(resolution,[status(thm)],[c70,c69]) ).
cnf(d32,plain,
sK212 = sK212,
inference(resolution,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
$false,
inference(resolution,[status(thm)],[d32,d17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n003.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sat Sep 26 09:27:25 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.40/5.96 % SZS status Theorem for theBenchmark.p
% 10.40/5.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------