%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU265+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:29 AM UTC 2026
% Result : Theorem 23.06s 5.96s
% Output : CNFRefutation 23.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 16
% Syntax : Number of formulae : 80 ( 15 unt; 0 def)
% Number of atoms : 196 ( 56 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 185 ( 69 ~; 91 |; 7 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 109 ( 13 sgn 45 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [X0,X1,X2] :
( element(X2,powerset('cartesian$uproduct2'(X0,X1)))
=> relation(X2) ) ).
fof(d4_relat_1,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = 'relation$udom'(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in('ordered$upair'(X2,X3),X0) ) ) ) ).
fof(dt_k4_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2'(X2,X0,X1)
=> element('relation$udom$uas$usubset'(X0,X1,X2),powerset(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(existence_m1_subset_1,axiom,
! [X0] :
? [X1] : element(X1,X0) ).
fof(fc1_xboole_0,axiom,
empty('empty$uset') ).
fof(redefinition_k4_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2'(X2,X0,X1)
=> 'relation$udom$uas$usubset'(X0,X1,X2) = 'relation$udom'(X2) ) ).
fof(redefinition_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
<=> 'relation$uof2'(X2,X0,X1) ) ).
fof(t1_subset,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ) ).
fof(t20_relat_1,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in('ordered$upair'(X0,X1),X2)
=> ( in(X1,'relation$urng'(X2))
& in(X0,'relation$udom'(X2)) ) ) ) ).
fof(t2_subset,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(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(t22_relset_1,conjecture,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X1,X0)
=> ( ! [X3] :
~ ( ! [X4] : ~ in('ordered$upair'(X3,X4),X2)
& in(X3,X1) )
<=> 'relation$udom$uas$usubset'(X1,X0,X2) = X1 ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X1,X0)
=> ( ! [X3] :
~ ( ! [X4] : ~ in('ordered$upair'(X3,X4),X2)
& in(X3,X1) )
<=> 'relation$udom$uas$usubset'(X1,X0,X2) = X1 ) ),
inference(negate_conjecture,[status(cth)],[t22_relset_1]) ).
cnf(c1,plain,
( relation(X0)
| ~ element(X0,powerset('cartesian$uproduct2'(X1,X2))) ),
inference(clausification,[status(esa)],[cc1_relset_1]) ).
cnf(c3,plain,
( in('ordered$upair'(X2,sK10(X0,X2)),X0)
| ~ in(X2,X1)
| X1 != 'relation$udom'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d4_relat_1]) ).
cnf(c6,plain,
( in('ordered$upair'(sK12(X0,X1),sK14(X0,X1)),X0)
| in(sK12(X0,X1),X1)
| X1 = 'relation$udom'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d4_relat_1]) ).
cnf(c7,plain,
( ~ in(sK12(X0,X1),X1)
| ~ in('ordered$upair'(sK12(X0,X1),X2),X0)
| X1 = 'relation$udom'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d4_relat_1]) ).
cnf(c10,plain,
( element('relation$udom$uas$usubset'(X1,X2,X0),powerset(X1))
| ~ 'relation$uof2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[dt_k4_relset_1]) ).
cnf(c11,plain,
( element(X0,powerset('cartesian$uproduct2'(X1,X2)))
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[dt_m2_relset_1]) ).
cnf(c13,plain,
element(sK27(X0),X0),
inference(clausification,[status(esa)],[existence_m1_subset_1]) ).
cnf(c15,plain,
empty('empty$uset'),
inference(clausification,[status(esa)],[fc1_xboole_0]) ).
cnf(c19,plain,
( 'relation$udom$uas$usubset'(X1,X2,X0) = 'relation$udom'(X0)
| ~ 'relation$uof2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_k4_relset_1]) ).
cnf(c20,plain,
( 'relation$uof2'(X0,X1,X2)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c23,plain,
( element(X0,X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t1_subset]) ).
cnf(c24,plain,
( in(X1,'relation$udom'(X0))
| ~ in('ordered$upair'(X1,X2),X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[t20_relat_1]) ).
cnf(c26,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(clausification,[status(esa)],[t2_subset]) ).
cnf(c33,plain,
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t4_subset]) ).
cnf(c34,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t5_subset]) ).
cnf(c35,plain,
( X0 = 'empty$uset'
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t6_boole]) ).
cnf(c36,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t7_boole]) ).
cnf(c38,plain,
'relation$uof2$uas$usubset'(sK68,sK67,sK66),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c41,plain,
( 'relation$udom$uas$usubset'(sK67,sK66,sK68) = sK67
| in('ordered$upair'(X0,sK70(X0)),sK68)
| ~ in(X0,sK67) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c42,plain,
( in(sK71,sK67)
| 'relation$udom$uas$usubset'(sK67,sK66,sK68) != sK67 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c43,plain,
( ~ in('ordered$upair'(sK71,X0),sK68)
| 'relation$udom$uas$usubset'(sK67,sK66,sK68) != sK67 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'relation$uof2'(sK68,sK67,sK66),
inference(resolution,[status(thm)],[c20,c38]) ).
cnf(d1,plain,
'relation$udom$uas$usubset'(sK67,sK66,sK68) = 'relation$udom'(sK68),
inference(resolution,[status(thm)],[d0,c19]) ).
cnf(d2,plain,
( in(sK71,sK67)
| 'relation$udom'(sK68) != sK67 ),
inference(demodulation,[status(thm)],[c42,d1]) ).
cnf(d3,plain,
( ~ 'relation$uof2'(sK68,sK67,sK66)
| element('relation$udom'(sK68),powerset(sK67)) ),
inference(superposition,[status(thm)],[d1,c10]) ).
cnf(d4,plain,
element('relation$udom'(sK68),powerset(sK67)),
inference(resolution,[status(thm)],[d0,d3]) ).
cnf(d5,plain,
( ~ empty(sK67)
| ~ in(X0,'relation$udom'(sK68)) ),
inference(resolution,[status(thm)],[c34,d4]) ).
cnf(d6,plain,
( empty(X0)
| in(sK27(X0),X0) ),
inference(resolution,[status(thm)],[c26,c13]) ).
cnf(d7,plain,
( ~ empty(sK67)
| empty('relation$udom'(sK68)) ),
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
( element(X0,sK67)
| ~ in(X0,'relation$udom'(sK68)) ),
inference(resolution,[status(thm)],[c33,d4]) ).
cnf(d9,plain,
( ~ relation(X0)
| in(sK12(X0,X1),X1)
| X1 = 'relation$udom'(X0)
| ~ relation(X0)
| in(sK12(X0,X1),'relation$udom'(X0)) ),
inference(resolution,[status(thm)],[c24,c6]) ).
cnf(d10,plain,
( element(sK12(sK68,X0),sK67)
| ~ relation(sK68)
| in(sK12(sK68,X0),X0)
| X0 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
( relation(X0)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(resolution,[status(thm)],[c11,c1]) ).
cnf(d12,plain,
relation(sK68),
inference(resolution,[status(thm)],[d11,c38]) ).
cnf(d13,plain,
( element(sK12(sK68,X0),sK67)
| in(sK12(sK68,X0),X0)
| X0 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d12,d10]) ).
cnf(d14,plain,
( element(sK12(sK68,X0),X0)
| element(sK12(sK68,X0),sK67)
| X0 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d13,c23]) ).
cnf(d15,plain,
( element(sK12(sK68,sK67),sK67)
| sK67 = 'relation$udom'(sK68) ),
inference(factoring,[status(thm)],[d14]) ).
cnf(d16,plain,
( empty(sK67)
| in(sK12(sK68,sK67),sK67)
| sK67 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d15,c26]) ).
cnf(d17,plain,
( ~ in(sK12(sK68,X0),sK67)
| 'relation$udom$uas$usubset'(sK67,sK66,sK68) = sK67
| ~ relation(sK68)
| ~ in(sK12(sK68,X0),X0)
| X0 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(d18,plain,
( ~ relation(sK68)
| ~ in(sK12(sK68,X0),sK67)
| ~ in(sK12(sK68,X0),X0)
| 'relation$udom'(sK68) = sK67
| X0 = 'relation$udom'(sK68) ),
inference(demodulation,[status(thm)],[d17,d1]) ).
cnf(d19,plain,
( ~ in(sK12(sK68,X0),sK67)
| ~ in(sK12(sK68,X0),X0)
| 'relation$udom'(sK68) = sK67
| X0 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d12,d18]) ).
cnf(d20,plain,
( ~ in(sK12(sK68,sK67),sK67)
| 'relation$udom'(sK68) = sK67
| sK67 = 'relation$udom'(sK68)
| empty(sK67)
| sK67 = 'relation$udom'(sK68) ),
inference(resolution,[status(thm)],[d16,d19]) ).
cnf(d21,plain,
( empty(sK67)
| sK67 = 'relation$udom'(sK68)
| empty(sK67)
| sK67 = 'relation$udom'(sK68)
| 'relation$udom'(sK68) = sK67 ),
inference(resolution,[status(thm)],[d20,d16]) ).
cnf(d22,plain,
( sK67 = 'empty$uset'
| sK67 = 'relation$udom'(sK68)
| 'relation$udom'(sK68) = sK67 ),
inference(resolution,[status(thm)],[d21,c35]) ).
cnf(d23,plain,
( sK67 = 'empty$uset'
| sK67 = 'relation$udom'(sK68)
| sK67 != sK67 ),
inference(equality_factoring,[status(thm)],[d22]) ).
cnf(d24,plain,
( sK67 = 'empty$uset'
| sK67 = 'relation$udom'(sK68) ),
inference(equality_resolution,[status(thm)],[d23]) ).
cnf(d25,plain,
( sK67 = 'empty$uset'
| in(sK71,sK67)
| sK67 != sK67 ),
inference(superposition,[status(thm)],[d24,d2]) ).
cnf(d26,plain,
( in(sK71,sK67)
| sK67 = 'empty$uset' ),
inference(equality_resolution,[status(thm)],[d25]) ).
cnf(d27,plain,
( ~ relation(X1)
| in('ordered$upair'(X0,sK10(X1,X0)),X1)
| ~ in(X0,'relation$udom'(X1)) ),
inference(equality_resolution,[status(thm)],[c3]) ).
cnf(d28,plain,
( ~ in('ordered$upair'(sK71,X0),sK68)
| 'relation$udom'(sK68) != sK67 ),
inference(demodulation,[status(thm)],[c43,d1]) ).
cnf(d29,plain,
( sK67 = 'empty$uset'
| ~ in('ordered$upair'(sK71,X0),sK68)
| sK67 != sK67 ),
inference(superposition,[status(thm)],[d24,d28]) ).
cnf(d30,plain,
( ~ in('ordered$upair'(sK71,X0),sK68)
| sK67 = 'empty$uset' ),
inference(equality_resolution,[status(thm)],[d29]) ).
cnf(d31,plain,
( ~ relation(sK68)
| ~ in(sK71,'relation$udom'(sK68))
| sK67 = 'empty$uset' ),
inference(resolution,[status(thm)],[d30,d27]) ).
cnf(d32,plain,
( ~ in(sK71,'relation$udom'(sK68))
| sK67 = 'empty$uset' ),
inference(resolution,[status(thm)],[d12,d31]) ).
cnf(d33,plain,
( sK67 = 'empty$uset'
| sK67 = 'empty$uset'
| ~ in(sK71,sK67) ),
inference(superposition,[status(thm)],[d24,d32]) ).
cnf(d34,plain,
( sK67 = 'empty$uset'
| sK67 = 'empty$uset' ),
inference(resolution,[status(thm)],[d33,d26]) ).
cnf(d35,plain,
empty(sK67),
inference(demodulation,[status(thm)],[c15,d34]) ).
cnf(d36,plain,
empty('relation$udom'(sK68)),
inference(resolution,[status(thm)],[d35,d7]) ).
cnf(d37,plain,
( ~ empty(X0)
| X0 = sK67 ),
inference(demodulation,[status(thm)],[c35,d34]) ).
cnf(d38,plain,
'relation$udom'(sK68) = sK67,
inference(resolution,[status(thm)],[d37,d36]) ).
cnf(d39,plain,
in(sK71,sK67),
inference(resolution,[status(thm)],[d38,d2]) ).
cnf(d40,plain,
~ empty(sK67),
inference(resolution,[status(thm)],[d39,c36]) ).
cnf(d41,plain,
$false,
inference(resolution,[status(thm)],[d35,d40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU265+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n003.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sat Sep 26 09:03:24 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.06/5.96 % SZS status Theorem for theBenchmark.p
% 23.06/5.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------