%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU339+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 : n011.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:43 AM UTC 2026
% Result : Theorem 47.78s 6.74s
% Output : CNFRefutation 47.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 19
% Syntax : Number of formulae : 107 ( 27 unt; 0 def)
% Number of atoms : 306 ( 19 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 365 ( 166 ~; 158 |; 15 &)
% ( 6 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 146 ( 18 sgn 45 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [X0,X1,X2] :
( element(X2,powerset('cartesian$uproduct2'(X0,X1)))
=> relation(X2) ) ).
fof(d4_relat_2,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( 'is$uantisymmetric$uin'(X0,X1)
<=> ! [X2,X3] :
( ( in('ordered$upair'(X3,X2),X0)
& in('ordered$upair'(X2,X3),X0)
& in(X3,X1)
& in(X2,X1) )
=> X2 = X3 ) ) ) ).
fof(d6_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> ( 'antisymmetric$urelstr'(X0)
<=> 'is$uantisymmetric$uin'('the$uInternalRel'(X0),'the$ucarrier'(X0)) ) ) ).
fof(d9_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> ! [X2] :
( element(X2,'the$ucarrier'(X0))
=> ( related(X0,X1,X2)
<=> in('ordered$upair'(X1,X2),'the$uInternalRel'(X0)) ) ) ) ) ).
fof(dt_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
=> element(X2,powerset('cartesian$uproduct2'(X0,X1))) ) ).
fof(dt_u1_orders_2,axiom,
! [X0] :
( 'rel$ustr'(X0)
=> 'relation$uof2$uas$usubset'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0)) ) ).
fof(existence_m1_subset_1,axiom,
! [X0] :
? [X1] : element(X1,X0) ).
fof(fc1_xboole_0,axiom,
empty('empty$uset') ).
fof(rc2_subset_1,axiom,
! [X0] :
? [X1] :
( empty(X1)
& element(X1,powerset(X0)) ) ).
fof(redefinition_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
<=> 'relation$uof2'(X2,X0,X1) ) ).
fof(t106_zfmisc_1,axiom,
! [X0,X1,X2,X3] :
( in('ordered$upair'(X0,X1),'cartesian$uproduct2'(X2,X3))
<=> ( in(X1,X3)
& in(X0,X2) ) ) ).
fof(t2_subset,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(X1) ) ) ).
fof(t3_subset,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,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(t6_boole,axiom,
! [X0] :
( empty(X0)
=> X0 = 'empty$uset' ) ).
fof(t7_boole,axiom,
! [X0,X1] :
~ ( empty(X1)
& in(X0,X1) ) ).
fof(t8_boole,axiom,
! [X0,X1] :
~ ( empty(X1)
& X0 != X1
& empty(X0) ) ).
fof(t25_orders_2,conjecture,
! [X0] :
( ( 'rel$ustr'(X0)
& 'antisymmetric$urelstr'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> ! [X2] :
( element(X2,'the$ucarrier'(X0))
=> ( ( related(X0,X2,X1)
& related(X0,X1,X2) )
=> X1 = X2 ) ) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( 'rel$ustr'(X0)
& 'antisymmetric$urelstr'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> ! [X2] :
( element(X2,'the$ucarrier'(X0))
=> ( ( related(X0,X2,X1)
& related(X0,X1,X2) )
=> X1 = X2 ) ) ) ),
inference(negate_conjecture,[status(cth)],[t25_orders_2]) ).
cnf(c1,plain,
( relation(X0)
| ~ element(X0,powerset('cartesian$uproduct2'(X1,X2))) ),
inference(clausification,[status(esa)],[cc1_relset_1]) ).
cnf(c3,plain,
( ~ in(X2,X3)
| ~ 'is$uantisymmetric$uin'(X0,X3)
| ~ in('ordered$upair'(X2,X1),X0)
| ~ in(X1,X3)
| ~ in('ordered$upair'(X1,X2),X0)
| X1 = X2
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d4_relat_2]) ).
cnf(c11,plain,
( 'is$uantisymmetric$uin'('the$uInternalRel'(X0),'the$ucarrier'(X0))
| ~ 'antisymmetric$urelstr'(X0)
| ~ 'rel$ustr'(X0) ),
inference(clausification,[status(esa)],[d6_orders_2]) ).
cnf(c13,plain,
( ~ related(X1,X0,X2)
| ~ 'rel$ustr'(X1)
| in('ordered$upair'(X0,X2),'the$uInternalRel'(X1))
| ~ element(X2,'the$ucarrier'(X1))
| ~ element(X0,'the$ucarrier'(X1)) ),
inference(clausification,[status(esa)],[d9_orders_2]) ).
cnf(c16,plain,
( element(X0,powerset('cartesian$uproduct2'(X1,X2)))
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[dt_m2_relset_1]) ).
cnf(c17,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(c21,plain,
element(sK31(X0),X0),
inference(clausification,[status(esa)],[existence_m1_subset_1]) ).
cnf(c24,plain,
empty('empty$uset'),
inference(clausification,[status(esa)],[fc1_xboole_0]) ).
cnf(c31,plain,
element(sK45(X0),powerset(X0)),
inference(clausification,[status(esa)],[rc2_subset_1]) ).
cnf(c32,plain,
empty(sK45(X0)),
inference(clausification,[status(esa)],[rc2_subset_1]) ).
cnf(c34,plain,
( 'relation$uof2'(X0,X1,X2)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c35,plain,
( ~ 'relation$uof2'(X0,X1,X2)
| 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c37,plain,
( in(X0,X2)
| ~ in('ordered$upair'(X0,X1),'cartesian$uproduct2'(X2,X3)) ),
inference(clausification,[status(esa)],[t106_zfmisc_1]) ).
cnf(c41,plain,
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(clausification,[status(esa)],[t2_subset]) ).
cnf(c42,plain,
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(clausification,[status(esa)],[t3_subset]) ).
cnf(c43,plain,
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(clausification,[status(esa)],[t3_subset]) ).
cnf(c44,plain,
( element(X2,X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(clausification,[status(esa)],[t4_subset]) ).
cnf(c45,plain,
( ~ element(X1,powerset(X2))
| ~ empty(X2)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t5_subset]) ).
cnf(c46,plain,
( X0 = 'empty$uset'
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t6_boole]) ).
cnf(c47,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t7_boole]) ).
cnf(c48,plain,
( X1 = X0
| ~ empty(X1)
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t8_boole]) ).
cnf(c49,plain,
'rel$ustr'(sK73),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c50,plain,
'antisymmetric$urelstr'(sK73),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c51,plain,
element(sK74,'the$ucarrier'(sK73)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c52,plain,
element(sK75,'the$ucarrier'(sK73)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c53,plain,
sK75 != sK74,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c54,plain,
related(sK73,sK74,sK75),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c55,plain,
related(sK73,sK75,sK74),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( empty(X0)
| in(sK31(X0),X0) ),
inference(resolution,[status(thm)],[c41,c21]) ).
cnf(d1,plain,
( ~ subset(X1,X2)
| ~ empty(X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[c45,c43]) ).
cnf(d2,plain,
( relation(X0)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(resolution,[status(thm)],[c16,c1]) ).
cnf(d3,plain,
( relation('the$uInternalRel'(X0))
| ~ 'rel$ustr'(X0) ),
inference(resolution,[status(thm)],[c17,d2]) ).
cnf(d4,plain,
( empty('the$ucarrier'(sK73))
| in(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c41,c51]) ).
cnf(d5,plain,
( empty('the$ucarrier'(sK73))
| in(sK75,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c41,c52]) ).
cnf(d6,plain,
( ~ 'is$uantisymmetric$uin'('the$uInternalRel'(X1),X3)
| ~ relation('the$uInternalRel'(X1))
| ~ in('ordered$upair'(X0,X2),'the$uInternalRel'(X1))
| ~ in(X2,X3)
| ~ in(X0,X3)
| X0 = X2
| ~ related(X1,X2,X0)
| ~ 'rel$ustr'(X1)
| ~ element(X2,'the$ucarrier'(X1))
| ~ element(X0,'the$ucarrier'(X1)) ),
inference(resolution,[status(thm)],[c13,c3]) ).
cnf(d7,plain,
( ~ related(X3,X0,X1)
| ~ 'rel$ustr'(X3)
| ~ element(X0,'the$ucarrier'(X3))
| ~ element(X1,'the$ucarrier'(X3))
| ~ related(X3,X1,X0)
| ~ 'rel$ustr'(X3)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(X3),X2)
| ~ relation('the$uInternalRel'(X3))
| ~ element(X0,'the$ucarrier'(X3))
| ~ element(X1,'the$ucarrier'(X3))
| ~ in(X0,X2)
| ~ in(X1,X2)
| X0 = X1 ),
inference(resolution,[status(thm)],[d6,c13]) ).
cnf(d8,plain,
( ~ related(sK73,sK74,sK75)
| ~ 'rel$ustr'(sK73)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73))
| ~ element(sK74,'the$ucarrier'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0)
| sK75 = sK74 ),
inference(resolution,[status(thm)],[d7,c55]) ).
cnf(d9,plain,
( ~ related(sK73,sK74,sK75)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73))
| ~ element(sK74,'the$ucarrier'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0)
| sK75 = sK74 ),
inference(resolution,[status(thm)],[c49,d8]) ).
cnf(d10,plain,
( ~ related(sK73,sK74,sK75)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73))
| ~ element(sK74,'the$ucarrier'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0) ),
inference(resolution,[status(thm)],[c53,d9]) ).
cnf(d11,plain,
( ~ related(sK73,sK74,sK75)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0) ),
inference(resolution,[status(thm)],[c51,d10]) ).
cnf(d12,plain,
( ~ related(sK73,sK74,sK75)
| ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0) ),
inference(resolution,[status(thm)],[c52,d11]) ).
cnf(d13,plain,
( ~ 'is$uantisymmetric$uin'('the$uInternalRel'(sK73),X0)
| ~ relation('the$uInternalRel'(sK73))
| ~ in(sK75,X0)
| ~ in(sK74,X0) ),
inference(resolution,[status(thm)],[c54,d12]) ).
cnf(d14,plain,
( ~ 'antisymmetric$urelstr'(sK73)
| ~ 'rel$ustr'(sK73)
| ~ relation('the$uInternalRel'(sK73))
| ~ in(sK75,'the$ucarrier'(sK73))
| ~ in(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[d13,c11]) ).
cnf(d15,plain,
( ~ 'antisymmetric$urelstr'(sK73)
| ~ relation('the$uInternalRel'(sK73))
| ~ in(sK75,'the$ucarrier'(sK73))
| ~ in(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c49,d14]) ).
cnf(d16,plain,
( ~ relation('the$uInternalRel'(sK73))
| ~ in(sK75,'the$ucarrier'(sK73))
| ~ in(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c50,d15]) ).
cnf(d17,plain,
( empty('the$ucarrier'(sK73))
| ~ relation('the$uInternalRel'(sK73))
| ~ in(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[d16,d5]) ).
cnf(d18,plain,
( empty('the$ucarrier'(sK73))
| empty('the$ucarrier'(sK73))
| ~ relation('the$uInternalRel'(sK73)) ),
inference(resolution,[status(thm)],[d17,d4]) ).
cnf(d19,plain,
( ~ 'rel$ustr'(sK73)
| empty('the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[d18,d3]) ).
cnf(d20,plain,
empty('the$ucarrier'(sK73)),
inference(resolution,[status(thm)],[c49,d19]) ).
cnf(d21,plain,
'the$ucarrier'(sK73) = 'empty$uset',
inference(resolution,[status(thm)],[d20,c46]) ).
cnf(d22,plain,
( 'relation$uof2'('the$uInternalRel'(X0),'the$ucarrier'(X0),'the$ucarrier'(X0))
| ~ 'rel$ustr'(X0) ),
inference(resolution,[status(thm)],[c17,c34]) ).
cnf(d23,plain,
( ~ 'rel$ustr'(sK73)
| 'relation$uof2'('the$uInternalRel'(sK73),'the$ucarrier'(sK73),'empty$uset') ),
inference(superposition,[status(thm)],[d21,d22]) ).
cnf(d24,plain,
( 'relation$uof2'('the$uInternalRel'(sK73),'empty$uset','empty$uset')
| ~ 'rel$ustr'(sK73) ),
inference(demodulation,[status(thm)],[d23,d21]) ).
cnf(d25,plain,
'relation$uof2'('the$uInternalRel'(sK73),'empty$uset','empty$uset'),
inference(resolution,[status(thm)],[c49,d24]) ).
cnf(d26,plain,
'relation$uof2$uas$usubset'('the$uInternalRel'(sK73),'empty$uset','empty$uset'),
inference(resolution,[status(thm)],[d25,c35]) ).
cnf(d27,plain,
( subset(X0,'cartesian$uproduct2'(X1,X2))
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(resolution,[status(thm)],[c16,c42]) ).
cnf(d28,plain,
sK45(X0) = 'empty$uset',
inference(resolution,[status(thm)],[c46,c32]) ).
cnf(d29,plain,
element('empty$uset',powerset(X0)),
inference(demodulation,[status(thm)],[c31,d28]) ).
cnf(d30,plain,
( ~ empty(X1)
| ~ in(X0,'empty$uset') ),
inference(resolution,[status(thm)],[c45,d29]) ).
cnf(d31,plain,
( ~ empty(X0)
| 'empty$uset' = X0 ),
inference(resolution,[status(thm)],[c48,c24]) ).
cnf(d32,plain,
( ~ 'relation$uof2$uas$usubset'(X1,X2,X3)
| element(X0,'cartesian$uproduct2'(X2,X3))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[c44,c16]) ).
cnf(d33,plain,
( element(X0,'cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ in(X0,'the$uInternalRel'(sK73)) ),
inference(resolution,[status(thm)],[d26,d32]) ).
cnf(d34,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| in(X0,'cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ in(X0,'the$uInternalRel'(sK73)) ),
inference(resolution,[status(thm)],[d33,c41]) ).
cnf(d35,plain,
( in(X0,'empty$uset')
| empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ in('ordered$upair'(X0,X1),'the$uInternalRel'(sK73)) ),
inference(resolution,[status(thm)],[d34,c37]) ).
cnf(d36,plain,
( ~ related(sK73,X0,X1)
| ~ 'rel$ustr'(sK73)
| ~ element(X0,'the$ucarrier'(sK73))
| ~ element(X1,'the$ucarrier'(sK73))
| empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| in(X0,'empty$uset') ),
inference(resolution,[status(thm)],[d35,c13]) ).
cnf(d37,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ related(sK73,X0,X1)
| ~ 'rel$ustr'(sK73)
| ~ element(X0,'the$ucarrier'(sK73))
| ~ element(X1,'empty$uset')
| in(X0,'empty$uset') ),
inference(demodulation,[status(thm)],[d36,d21]) ).
cnf(d38,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ related(sK73,X0,X1)
| ~ 'rel$ustr'(sK73)
| ~ element(X0,'empty$uset')
| ~ element(X1,'empty$uset')
| in(X0,'empty$uset') ),
inference(demodulation,[status(thm)],[d37,d21]) ).
cnf(d39,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ related(sK73,X0,X1)
| ~ element(X0,'empty$uset')
| ~ element(X1,'empty$uset')
| in(X0,'empty$uset') ),
inference(resolution,[status(thm)],[c49,d38]) ).
cnf(d40,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ element(sK75,'empty$uset')
| ~ element(sK74,'empty$uset')
| in(sK75,'empty$uset') ),
inference(resolution,[status(thm)],[d39,c55]) ).
cnf(d41,plain,
element(sK75,'empty$uset'),
inference(demodulation,[status(thm)],[c52,d21]) ).
cnf(d42,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| ~ element(sK74,'empty$uset')
| in(sK75,'empty$uset') ),
inference(resolution,[status(thm)],[d41,d40]) ).
cnf(d43,plain,
element(sK74,'empty$uset'),
inference(demodulation,[status(thm)],[c51,d21]) ).
cnf(d44,plain,
( empty('cartesian$uproduct2'('empty$uset','empty$uset'))
| in(sK75,'empty$uset') ),
inference(resolution,[status(thm)],[d43,d42]) ).
cnf(d45,plain,
( 'empty$uset' = 'cartesian$uproduct2'('empty$uset','empty$uset')
| in(sK75,'empty$uset') ),
inference(resolution,[status(thm)],[d44,d31]) ).
cnf(d46,plain,
( ~ empty(X0)
| 'empty$uset' = 'cartesian$uproduct2'('empty$uset','empty$uset') ),
inference(resolution,[status(thm)],[d45,d30]) ).
cnf(d47,plain,
'empty$uset' = 'cartesian$uproduct2'('empty$uset','empty$uset'),
inference(resolution,[status(thm)],[d46,c24]) ).
cnf(d48,plain,
( ~ 'relation$uof2$uas$usubset'(X0,'empty$uset','empty$uset')
| subset(X0,'empty$uset') ),
inference(superposition,[status(thm)],[d47,d27]) ).
cnf(d49,plain,
subset('the$uInternalRel'(sK73),'empty$uset'),
inference(resolution,[status(thm)],[d48,d26]) ).
cnf(d50,plain,
( ~ empty('empty$uset')
| ~ in(X0,'the$uInternalRel'(sK73)) ),
inference(resolution,[status(thm)],[d49,d1]) ).
cnf(d51,plain,
~ in(X0,'the$uInternalRel'(sK73)),
inference(resolution,[status(thm)],[c24,d50]) ).
cnf(d52,plain,
empty('the$uInternalRel'(sK73)),
inference(resolution,[status(thm)],[d51,d0]) ).
cnf(d53,plain,
( ~ empty('the$uInternalRel'(X1))
| ~ related(X1,X2,X0)
| ~ 'rel$ustr'(X1)
| ~ element(X2,'the$ucarrier'(X1))
| ~ element(X0,'the$ucarrier'(X1)) ),
inference(resolution,[status(thm)],[c13,c47]) ).
cnf(d54,plain,
( ~ empty('the$uInternalRel'(sK73))
| ~ 'rel$ustr'(sK73)
| ~ element(sK74,'the$ucarrier'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[d53,c55]) ).
cnf(d55,plain,
( ~ empty('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73))
| ~ element(sK74,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c49,d54]) ).
cnf(d56,plain,
( ~ empty('the$uInternalRel'(sK73))
| ~ element(sK75,'the$ucarrier'(sK73)) ),
inference(resolution,[status(thm)],[c51,d55]) ).
cnf(d57,plain,
~ empty('the$uInternalRel'(sK73)),
inference(resolution,[status(thm)],[c52,d56]) ).
cnf(d58,plain,
$false,
inference(resolution,[status(thm)],[d57,d52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU339+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.09/0.36 % Computer : n011.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 : Sat Sep 26 09:15:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.78/6.74 % SZS status Theorem for theBenchmark.p
% 47.78/6.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------