%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SET994+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:33:42 AM UTC 2026
% Result : Theorem 4.50s 3.57s
% Output : CNFRefutation 4.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 54 ( 22 unt; 0 def)
% Number of atoms : 133 ( 64 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 126 ( 47 ~; 51 |; 16 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 59 ( 4 sgn 16 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(existence_m1_subset_1,axiom,
! [X0] :
? [X1] : element(X1,X0) ).
fof(fc12_relat_1,axiom,
( 'relation$uempty$uyielding'('empty$uset')
& relation('empty$uset')
& empty('empty$uset') ) ).
fof(rc1_xboole_0,axiom,
? [X0] : empty(X0) ).
fof(s3_funct_1__e4_14__funct_1,axiom,
! [X0] :
? [X1] :
( ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = n0 )
& 'relation$udom'(X1) = X0
& function(X1)
& relation(X1) ) ).
fof(s3_funct_1__e7_14__funct_1,axiom,
! [X0] :
? [X1] :
( ! [X2] :
( in(X2,X0)
=> apply(X1,X2) = n1 )
& 'relation$udom'(X1) = X0
& function(X1)
& relation(X1) ) ).
fof(spc0_boole,axiom,
empty(n0) ).
fof(spc1_boole,axiom,
~ empty(n1) ).
fof(t2_subset,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(X1) ) ) ).
fof(t6_boole,axiom,
! [X0] :
( empty(X0)
=> X0 = 'empty$uset' ) ).
fof(t8_boole,axiom,
! [X0,X1] :
~ ( empty(X1)
& X0 != X1
& empty(X0) ) ).
fof(t16_funct_1,conjecture,
! [X0] :
( ! [X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( ( 'relation$udom'(X2) = X0
& 'relation$udom'(X1) = X0 )
=> X1 = X2 ) ) )
=> X0 = 'empty$uset' ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ! [X1] :
( ( function(X1)
& relation(X1) )
=> ! [X2] :
( ( function(X2)
& relation(X2) )
=> ( ( 'relation$udom'(X2) = X0
& 'relation$udom'(X1) = X0 )
=> X1 = X2 ) ) )
=> X0 = 'empty$uset' ),
inference(negate_conjecture,[status(cth)],[t16_funct_1]) ).
cnf(c3,plain,
element(sK5(X0),X0),
inference(clausification,[status(esa)],[existence_m1_subset_1]) ).
cnf(c4,plain,
empty('empty$uset'),
inference(clausification,[status(esa)],[fc12_relat_1]) ).
cnf(c20,plain,
empty(sK13),
inference(clausification,[status(esa)],[rc1_xboole_0]) ).
cnf(c29,plain,
relation(sK22(X0)),
inference(clausification,[status(esa)],[s3_funct_1__e4_14__funct_1]) ).
cnf(c30,plain,
function(sK22(X0)),
inference(clausification,[status(esa)],[s3_funct_1__e4_14__funct_1]) ).
cnf(c31,plain,
'relation$udom'(sK22(X0)) = X0,
inference(clausification,[status(esa)],[s3_funct_1__e4_14__funct_1]) ).
cnf(c32,plain,
( apply(sK22(X1),X0) = n0
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[s3_funct_1__e4_14__funct_1]) ).
cnf(c33,plain,
relation(sK25(X0)),
inference(clausification,[status(esa)],[s3_funct_1__e7_14__funct_1]) ).
cnf(c34,plain,
function(sK25(X0)),
inference(clausification,[status(esa)],[s3_funct_1__e7_14__funct_1]) ).
cnf(c35,plain,
'relation$udom'(sK25(X0)) = X0,
inference(clausification,[status(esa)],[s3_funct_1__e7_14__funct_1]) ).
cnf(c36,plain,
( apply(sK25(X1),X0) = n1
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[s3_funct_1__e7_14__funct_1]) ).
cnf(c37,plain,
empty(n0),
inference(clausification,[status(esa)],[spc0_boole]) ).
cnf(c38,plain,
~ empty(n1),
inference(clausification,[status(esa)],[spc1_boole]) ).
cnf(c40,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(clausification,[status(esa)],[t2_subset]) ).
cnf(c45,plain,
( X0 = 'empty$uset'
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t6_boole]) ).
cnf(c47,plain,
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(clausification,[status(esa)],[t8_boole]) ).
cnf(c48,plain,
( 'relation$udom'(X1) != sK44
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| 'relation$udom'(X0) != sK44
| X1 = X0
| ~ function(X0) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c49,plain,
sK44 != 'empty$uset',
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
sK13 = 'empty$uset',
inference(resolution,[status(thm)],[c45,c20]) ).
cnf(d1,plain,
( ~ empty(X0)
| sK13 = X0 ),
inference(resolution,[status(thm)],[c47,c20]) ).
cnf(d2,plain,
( ~ empty(X0)
| 'empty$uset' = X0 ),
inference(demodulation,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
n0 = 'empty$uset',
inference(resolution,[status(thm)],[c45,c37]) ).
cnf(d4,plain,
( empty(X0)
| in(sK5(X0),X0) ),
inference(resolution,[status(thm)],[c40,c3]) ).
cnf(d5,plain,
( apply(sK22(X0),sK5(X0)) = n0
| empty(X0) ),
inference(resolution,[status(thm)],[d4,c32]) ).
cnf(d6,plain,
( empty(X0)
| apply(sK22(X0),sK5(X0)) = 'empty$uset' ),
inference(demodulation,[status(thm)],[d5,d3]) ).
cnf(d7,plain,
( 'empty$uset' = X0
| apply(sK22(X0),sK5(X0)) = 'empty$uset' ),
inference(resolution,[status(thm)],[d6,d2]) ).
cnf(d8,plain,
( apply(sK25(X0),sK5(X0)) = n1
| empty(X0) ),
inference(resolution,[status(thm)],[d4,c36]) ).
cnf(d9,plain,
( 'empty$uset' = X0
| apply(sK25(X0),sK5(X0)) = n1 ),
inference(resolution,[status(thm)],[d8,d2]) ).
cnf(d10,plain,
( ~ relation(sK22(X0))
| ~ relation(X1)
| ~ function(sK22(X0))
| ~ function(X1)
| 'relation$udom'(X1) != sK44
| sK22(X0) = X1
| X0 != sK44 ),
inference(superposition,[status(thm)],[c31,c48]) ).
cnf(d11,plain,
( ~ relation(X1)
| ~ function(sK22(X0))
| ~ function(X1)
| sK22(X0) = X1
| 'relation$udom'(X1) != sK44
| X0 != sK44 ),
inference(resolution,[status(thm)],[c29,d10]) ).
cnf(d12,plain,
( ~ relation(X1)
| ~ function(X1)
| sK22(X0) = X1
| 'relation$udom'(X1) != sK44
| X0 != sK44 ),
inference(resolution,[status(thm)],[c30,d11]) ).
cnf(d13,plain,
( ~ relation(sK25(X0))
| ~ function(sK25(X0))
| sK22(X1) = sK25(X0)
| X1 != sK44
| X0 != sK44 ),
inference(superposition,[status(thm)],[c35,d12]) ).
cnf(d14,plain,
( ~ function(sK25(X1))
| sK22(X0) = sK25(X1)
| X1 != sK44
| X0 != sK44 ),
inference(resolution,[status(thm)],[c33,d13]) ).
cnf(d15,plain,
( sK22(X1) = sK25(X0)
| X1 != sK44
| X0 != sK44 ),
inference(resolution,[status(thm)],[c34,d14]) ).
cnf(d16,plain,
( sK22(X0) = sK25(sK44)
| X0 != sK44 ),
inference(equality_resolution,[status(thm)],[d15]) ).
cnf(d17,plain,
sK22(sK44) = sK25(sK44),
inference(equality_resolution,[status(thm)],[d16]) ).
cnf(d18,plain,
( 'empty$uset' = sK44
| apply(sK22(sK44),sK5(sK44)) = n1 ),
inference(superposition,[status(thm)],[d17,d9]) ).
cnf(d19,plain,
( 'empty$uset' = sK44
| 'empty$uset' = sK44
| n1 = 'empty$uset' ),
inference(superposition,[status(thm)],[d18,d7]) ).
cnf(d20,plain,
( 'empty$uset' = sK44
| ~ empty('empty$uset') ),
inference(superposition,[status(thm)],[d19,c38]) ).
cnf(d21,plain,
'empty$uset' = sK44,
inference(resolution,[status(thm)],[c4,d20]) ).
cnf(d22,plain,
'empty$uset' != 'empty$uset',
inference(demodulation,[status(thm)],[c49,d21]) ).
cnf(d23,plain,
$false,
inference(equality_resolution,[status(thm)],[d22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET994+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n009.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Sat Sep 26 08:29:45 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/3.57 % SZS status Theorem for theBenchmark.p
% 4.50/3.57 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------