%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU266+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 : n006.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 12.93s 8.62s
% Output : CNFRefutation 12.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 18
% Syntax : Number of formulae : 87 ( 18 unt; 0 def)
% Number of atoms : 209 ( 61 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 197 ( 75 ~; 95 |; 9 &)
% ( 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 : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 116 ( 13 sgn 47 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [X0,X1,X2] :
( element(X2,powerset('cartesian$uproduct2'(X0,X1)))
=> relation(X2) ) ).
fof(d5_relat_1,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = 'relation$urng'(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in('ordered$upair'(X3,X2),X0) ) ) ) ).
fof(dt_k5_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2'(X2,X0,X1)
=> element('relation$urng$uas$usubset'(X0,X1,X2),powerset(X1)) ) ).
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(rc1_xboole_0,axiom,
? [X0] : empty(X0) ).
fof(redefinition_k5_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2'(X2,X0,X1)
=> 'relation$urng$uas$usubset'(X0,X1,X2) = 'relation$urng'(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(t8_boole,axiom,
! [X0,X1] :
~ ( empty(X1)
& X0 != X1
& empty(X0) ) ).
fof(t23_relset_1,conjecture,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
=> ( ! [X3] :
~ ( ! [X4] : ~ in('ordered$upair'(X4,X3),X2)
& in(X3,X1) )
<=> 'relation$urng$uas$usubset'(X0,X1,X2) = X1 ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
=> ( ! [X3] :
~ ( ! [X4] : ~ in('ordered$upair'(X4,X3),X2)
& in(X3,X1) )
<=> 'relation$urng$uas$usubset'(X0,X1,X2) = X1 ) ),
inference(negate_conjecture,[status(cth)],[t23_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'(sK10(X0,X2),X2),X0)
| ~ in(X2,X1)
| X1 != 'relation$urng'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d5_relat_1]) ).
cnf(c6,plain,
( in('ordered$upair'(sK14(X0,X1),sK12(X0,X1)),X0)
| in(sK12(X0,X1),X1)
| X1 = 'relation$urng'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d5_relat_1]) ).
cnf(c7,plain,
( ~ in(sK12(X0,X1),X1)
| ~ in('ordered$upair'(X2,sK12(X0,X1)),X0)
| X1 = 'relation$urng'(X0)
| ~ relation(X0) ),
inference(clausification,[status(esa)],[d5_relat_1]) ).
cnf(c10,plain,
( element('relation$urng$uas$usubset'(X1,X2,X0),powerset(X2))
| ~ 'relation$uof2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[dt_k5_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(c17,plain,
empty(sK33),
inference(clausification,[status(esa)],[rc1_xboole_0]) ).
cnf(c19,plain,
( 'relation$urng$uas$usubset'(X1,X2,X0) = 'relation$urng'(X0)
| ~ 'relation$uof2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_k5_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(c25,plain,
( in(X2,'relation$urng'(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(c37,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t8_boole]) ).
cnf(c38,plain,
'relation$uof2$uas$usubset'(sK68,sK66,sK67),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c41,plain,
( 'relation$urng$uas$usubset'(sK66,sK67,sK68) = sK67
| in('ordered$upair'(sK70(X0),X0),sK68)
| ~ in(X0,sK67) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c42,plain,
( in(sK71,sK67)
| 'relation$urng$uas$usubset'(sK66,sK67,sK68) != sK67 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c43,plain,
( ~ in('ordered$upair'(X0,sK71),sK68)
| 'relation$urng$uas$usubset'(sK66,sK67,sK68) != sK67 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'relation$uof2'(sK68,sK66,sK67),
inference(resolution,[status(thm)],[c20,c38]) ).
cnf(d1,plain,
'relation$urng$uas$usubset'(sK66,sK67,sK68) = 'relation$urng'(sK68),
inference(resolution,[status(thm)],[d0,c19]) ).
cnf(d2,plain,
( in(sK71,sK67)
| 'relation$urng'(sK68) != sK67 ),
inference(demodulation,[status(thm)],[c42,d1]) ).
cnf(d3,plain,
( ~ 'relation$uof2'(sK68,sK66,sK67)
| element('relation$urng'(sK68),powerset(sK67)) ),
inference(superposition,[status(thm)],[d1,c10]) ).
cnf(d4,plain,
element('relation$urng'(sK68),powerset(sK67)),
inference(resolution,[status(thm)],[d0,d3]) ).
cnf(d5,plain,
( ~ empty(sK67)
| ~ in(X0,'relation$urng'(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$urng'(sK68)) ),
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
sK33 = 'empty$uset',
inference(resolution,[status(thm)],[c35,c17]) ).
cnf(d9,plain,
( ~ empty(X0)
| sK33 = X0 ),
inference(resolution,[status(thm)],[c37,c17]) ).
cnf(d10,plain,
( ~ empty(X0)
| 'empty$uset' = X0 ),
inference(demodulation,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
( element(X0,sK67)
| ~ in(X0,'relation$urng'(sK68)) ),
inference(resolution,[status(thm)],[c33,d4]) ).
cnf(d12,plain,
( ~ relation(X0)
| in(sK12(X0,X1),X1)
| X1 = 'relation$urng'(X0)
| ~ relation(X0)
| in(sK12(X0,X1),'relation$urng'(X0)) ),
inference(resolution,[status(thm)],[c25,c6]) ).
cnf(d13,plain,
( element(sK12(sK68,X0),sK67)
| ~ relation(sK68)
| in(sK12(sK68,X0),X0)
| X0 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d12,d11]) ).
cnf(d14,plain,
( relation(X0)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(resolution,[status(thm)],[c11,c1]) ).
cnf(d15,plain,
relation(sK68),
inference(resolution,[status(thm)],[d14,c38]) ).
cnf(d16,plain,
( element(sK12(sK68,X0),sK67)
| in(sK12(sK68,X0),X0)
| X0 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d15,d13]) ).
cnf(d17,plain,
( element(sK12(sK68,X0),X0)
| element(sK12(sK68,X0),sK67)
| X0 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d16,c23]) ).
cnf(d18,plain,
( element(sK12(sK68,sK67),sK67)
| sK67 = 'relation$urng'(sK68) ),
inference(factoring,[status(thm)],[d17]) ).
cnf(d19,plain,
( empty(sK67)
| in(sK12(sK68,sK67),sK67)
| sK67 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d18,c26]) ).
cnf(d20,plain,
( ~ in(sK12(sK68,X0),sK67)
| 'relation$urng$uas$usubset'(sK66,sK67,sK68) = sK67
| ~ relation(sK68)
| ~ in(sK12(sK68,X0),X0)
| X0 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[c7,c41]) ).
cnf(d21,plain,
( ~ relation(sK68)
| ~ in(sK12(sK68,X0),sK67)
| ~ in(sK12(sK68,X0),X0)
| 'relation$urng'(sK68) = sK67
| X0 = 'relation$urng'(sK68) ),
inference(demodulation,[status(thm)],[d20,d1]) ).
cnf(d22,plain,
( ~ in(sK12(sK68,X0),sK67)
| ~ in(sK12(sK68,X0),X0)
| 'relation$urng'(sK68) = sK67
| X0 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d15,d21]) ).
cnf(d23,plain,
( ~ in(sK12(sK68,sK67),sK67)
| 'relation$urng'(sK68) = sK67
| sK67 = 'relation$urng'(sK68)
| empty(sK67)
| sK67 = 'relation$urng'(sK68) ),
inference(resolution,[status(thm)],[d19,d22]) ).
cnf(d24,plain,
( empty(sK67)
| sK67 = 'relation$urng'(sK68)
| empty(sK67)
| sK67 = 'relation$urng'(sK68)
| 'relation$urng'(sK68) = sK67 ),
inference(resolution,[status(thm)],[d23,d19]) ).
cnf(d25,plain,
( 'empty$uset' = sK67
| sK67 = 'relation$urng'(sK68)
| 'relation$urng'(sK68) = sK67 ),
inference(resolution,[status(thm)],[d24,d10]) ).
cnf(d26,plain,
( sK67 = 'relation$urng'(sK68)
| 'empty$uset' = sK67
| sK67 != sK67 ),
inference(equality_factoring,[status(thm)],[d25]) ).
cnf(d27,plain,
( sK67 = 'relation$urng'(sK68)
| 'empty$uset' = sK67 ),
inference(equality_resolution,[status(thm)],[d26]) ).
cnf(d28,plain,
( 'empty$uset' = sK67
| in(sK71,sK67)
| sK67 != sK67 ),
inference(superposition,[status(thm)],[d27,d2]) ).
cnf(d29,plain,
( in(sK71,sK67)
| 'empty$uset' = sK67 ),
inference(equality_resolution,[status(thm)],[d28]) ).
cnf(d30,plain,
( ~ relation(X1)
| in('ordered$upair'(sK10(X1,X0),X0),X1)
| ~ in(X0,'relation$urng'(X1)) ),
inference(equality_resolution,[status(thm)],[c3]) ).
cnf(d31,plain,
( ~ in('ordered$upair'(X0,sK71),sK68)
| 'relation$urng'(sK68) != sK67 ),
inference(demodulation,[status(thm)],[c43,d1]) ).
cnf(d32,plain,
( 'empty$uset' = sK67
| ~ in('ordered$upair'(X0,sK71),sK68)
| sK67 != sK67 ),
inference(superposition,[status(thm)],[d27,d31]) ).
cnf(d33,plain,
( ~ in('ordered$upair'(X0,sK71),sK68)
| 'empty$uset' = sK67 ),
inference(equality_resolution,[status(thm)],[d32]) ).
cnf(d34,plain,
( ~ relation(sK68)
| ~ in(sK71,'relation$urng'(sK68))
| 'empty$uset' = sK67 ),
inference(resolution,[status(thm)],[d33,d30]) ).
cnf(d35,plain,
( ~ in(sK71,'relation$urng'(sK68))
| 'empty$uset' = sK67 ),
inference(resolution,[status(thm)],[d15,d34]) ).
cnf(d36,plain,
( 'empty$uset' = sK67
| 'empty$uset' = sK67
| ~ in(sK71,sK67) ),
inference(superposition,[status(thm)],[d27,d35]) ).
cnf(d37,plain,
( 'empty$uset' = sK67
| 'empty$uset' = sK67 ),
inference(resolution,[status(thm)],[d36,d29]) ).
cnf(d38,plain,
empty(sK67),
inference(demodulation,[status(thm)],[c15,d37]) ).
cnf(d39,plain,
empty('relation$urng'(sK68)),
inference(resolution,[status(thm)],[d38,d7]) ).
cnf(d40,plain,
( ~ empty(X0)
| X0 = sK67 ),
inference(demodulation,[status(thm)],[c35,d37]) ).
cnf(d41,plain,
'relation$urng'(sK68) = sK67,
inference(resolution,[status(thm)],[d40,d39]) ).
cnf(d42,plain,
in(sK71,sK67),
inference(resolution,[status(thm)],[d41,d2]) ).
cnf(d43,plain,
~ empty(sK67),
inference(resolution,[status(thm)],[d42,c36]) ).
cnf(d44,plain,
$false,
inference(resolution,[status(thm)],[d38,d43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU266+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.11/5.38 % Computer : n006.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Sat Sep 26 09:01:47 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.93/8.62 % SZS status Theorem for theBenchmark.p
% 12.93/8.62 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------