%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU353+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 : n017.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:45 AM UTC 2026
% Result : Theorem 13.17s 7.17s
% Output : CNFRefutation 13.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 51 ( 20 unt; 0 def)
% Number of atoms : 115 ( 23 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 98 ( 34 ~; 37 |; 15 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-4 aty)
% Number of variables : 46 ( 1 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_funct_2,axiom,
! [X0,X1,X2] :
( 'relation$uof2'(X2,X0,X1)
=> ( ( 'v1$upartfun1'(X2,X0,X1)
& function(X2) )
=> ( 'quasi$utotal'(X2,X0,X1)
& function(X2) ) ) ) ).
fof(d11_grcat_1,axiom,
! [X0] :
( 'one$usorted$ustr'(X0)
=> 'identity$uon$ucarrier'(X0) = 'identity$uas$urelation$uof'('the$ucarrier'(X0)) ) ).
fof(dt_k6_partfun1,axiom,
! [X0] :
( 'relation$uof2$uas$usubset'('identity$uas$urelation$uof'(X0),X0,X0)
& 'v1$upartfun1'('identity$uas$urelation$uof'(X0),X0,X0) ) ).
fof(fc1_struct_0,axiom,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ~ empty('the$ucarrier'(X0)) ) ).
fof(fc2_partfun1,axiom,
! [X0] :
( transitive('identity$urelation'(X0))
& antisymmetric('identity$urelation'(X0))
& symmetric('identity$urelation'(X0))
& reflexive('identity$urelation'(X0))
& function('identity$urelation'(X0))
& relation('identity$urelation'(X0)) ) ).
fof(redefinition_k6_partfun1,axiom,
! [X0] : 'identity$uas$urelation$uof'(X0) = 'identity$urelation'(X0) ).
fof(redefinition_k8_funct_2,axiom,
! [X0,X1,X2,X3] :
( ( element(X3,X0)
& 'relation$uof2'(X2,X0,X1)
& 'quasi$utotal'(X2,X0,X1)
& function(X2)
& ~ empty(X0) )
=> 'apply$uas$uelement'(X0,X1,X2,X3) = apply(X2,X3) ) ).
fof(redefinition_m2_relset_1,axiom,
! [X0,X1,X2] :
( 'relation$uof2$uas$usubset'(X2,X0,X1)
<=> 'relation$uof2'(X2,X0,X1) ) ).
fof(t2_subset,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( in(X0,X1)
| empty(X1) ) ) ).
fof(t35_funct_1,axiom,
! [X0,X1] :
( in(X1,X0)
=> apply('identity$urelation'(X0),X1) = X1 ) ).
fof(t91_tmap_1,conjecture,
! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> 'apply$uas$uelement'('the$ucarrier'(X0),'the$ucarrier'(X0),'identity$uon$ucarrier'(X0),X1) = X1 ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] :
( ( 'one$usorted$ustr'(X0)
& ~ 'empty$ucarrier'(X0) )
=> ! [X1] :
( element(X1,'the$ucarrier'(X0))
=> 'apply$uas$uelement'('the$ucarrier'(X0),'the$ucarrier'(X0),'identity$uon$ucarrier'(X0),X1) = X1 ) ),
inference(negate_conjecture,[status(cth)],[t91_tmap_1]) ).
cnf(c2,plain,
( 'quasi$utotal'(X0,X1,X2)
| ~ 'v1$upartfun1'(X0,X1,X2)
| ~ function(X0)
| ~ 'relation$uof2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[cc1_funct_2]) ).
cnf(c26,plain,
( 'identity$uon$ucarrier'(X0) = 'identity$uas$urelation$uof'('the$ucarrier'(X0))
| ~ 'one$usorted$ustr'(X0) ),
inference(clausification,[status(esa)],[d11_grcat_1]) ).
cnf(c27,plain,
'v1$upartfun1'('identity$uas$urelation$uof'(X0),X0,X0),
inference(clausification,[status(esa)],[dt_k6_partfun1]) ).
cnf(c28,plain,
'relation$uof2$uas$usubset'('identity$uas$urelation$uof'(X0),X0,X0),
inference(clausification,[status(esa)],[dt_k6_partfun1]) ).
cnf(c39,plain,
( ~ empty('the$ucarrier'(X0))
| ~ 'one$usorted$ustr'(X0)
| 'empty$ucarrier'(X0) ),
inference(clausification,[status(esa)],[fc1_struct_0]) ).
cnf(c43,plain,
function('identity$urelation'(X0)),
inference(clausification,[status(esa)],[fc2_partfun1]) ).
cnf(c84,plain,
'identity$uas$urelation$uof'(X0) = 'identity$urelation'(X0),
inference(clausification,[status(esa)],[redefinition_k6_partfun1]) ).
cnf(c85,plain,
( ~ element(X3,X0)
| ~ function(X2)
| ~ 'relation$uof2'(X2,X0,X1)
| ~ 'quasi$utotal'(X2,X0,X1)
| empty(X0)
| 'apply$uas$uelement'(X0,X1,X2,X3) = apply(X2,X3) ),
inference(clausification,[status(esa)],[redefinition_k8_funct_2]) ).
cnf(c86,plain,
( 'relation$uof2'(X0,X1,X2)
| ~ 'relation$uof2$uas$usubset'(X0,X1,X2) ),
inference(clausification,[status(esa)],[redefinition_m2_relset_1]) ).
cnf(c90,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(clausification,[status(esa)],[t2_subset]) ).
cnf(c91,plain,
( apply('identity$urelation'(X1),X0) = X0
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[t35_funct_1]) ).
cnf(c99,plain,
~ 'empty$ucarrier'(sK98),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c100,plain,
'one$usorted$ustr'(sK98),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c101,plain,
element(sK99,'the$ucarrier'(sK98)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c102,plain,
'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),sK99) != sK99,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
'identity$uon$ucarrier'(sK98) = 'identity$uas$urelation$uof'('the$ucarrier'(sK98)),
inference(resolution,[status(thm)],[c26,c100]) ).
cnf(d1,plain,
'identity$uon$ucarrier'(sK98) = 'identity$urelation'('the$ucarrier'(sK98)),
inference(demodulation,[status(thm)],[d0,c84]) ).
cnf(d2,plain,
( empty('the$ucarrier'(sK98))
| in(sK99,'the$ucarrier'(sK98)) ),
inference(resolution,[status(thm)],[c90,c101]) ).
cnf(d3,plain,
( apply('identity$urelation'('the$ucarrier'(sK98)),sK99) = sK99
| empty('the$ucarrier'(sK98)) ),
inference(resolution,[status(thm)],[d2,c91]) ).
cnf(d4,plain,
( empty('the$ucarrier'(sK98))
| apply('identity$uon$ucarrier'(sK98),sK99) = sK99 ),
inference(demodulation,[status(thm)],[d3,d1]) ).
cnf(d5,plain,
( 'empty$ucarrier'(sK98)
| ~ 'one$usorted$ustr'(sK98)
| apply('identity$uon$ucarrier'(sK98),sK99) = sK99 ),
inference(resolution,[status(thm)],[d4,c39]) ).
cnf(d6,plain,
( ~ 'one$usorted$ustr'(sK98)
| apply('identity$uon$ucarrier'(sK98),sK99) = sK99 ),
inference(resolution,[status(thm)],[c99,d5]) ).
cnf(d7,plain,
apply('identity$uon$ucarrier'(sK98),sK99) = sK99,
inference(resolution,[status(thm)],[c100,d6]) ).
cnf(d8,plain,
'relation$uof2$uas$usubset'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98)),
inference(superposition,[status(thm)],[d0,c28]) ).
cnf(d9,plain,
'relation$uof2'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98)),
inference(resolution,[status(thm)],[c86,d8]) ).
cnf(d10,plain,
( 'quasi$utotal'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98))
| ~ 'v1$upartfun1'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98))
| ~ function('identity$uon$ucarrier'(sK98)) ),
inference(resolution,[status(thm)],[d9,c2]) ).
cnf(d11,plain,
'v1$upartfun1'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98)),
inference(superposition,[status(thm)],[d0,c27]) ).
cnf(d12,plain,
( 'quasi$utotal'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98))
| ~ function('identity$uon$ucarrier'(sK98)) ),
inference(resolution,[status(thm)],[d11,d10]) ).
cnf(d13,plain,
function('identity$uon$ucarrier'(sK98)),
inference(superposition,[status(thm)],[d1,c43]) ).
cnf(d14,plain,
'quasi$utotal'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98)),
inference(resolution,[status(thm)],[d13,d12]) ).
cnf(d15,plain,
( empty('the$ucarrier'(sK98))
| ~ element(X0,'the$ucarrier'(sK98))
| ~ 'relation$uof2'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98))
| ~ function('identity$uon$ucarrier'(sK98))
| 'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),X0) = apply('identity$uon$ucarrier'(sK98),X0) ),
inference(resolution,[status(thm)],[d14,c85]) ).
cnf(d16,plain,
( empty('the$ucarrier'(sK98))
| ~ element(X0,'the$ucarrier'(sK98))
| ~ 'relation$uof2'('identity$uon$ucarrier'(sK98),'the$ucarrier'(sK98),'the$ucarrier'(sK98))
| 'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),X0) = apply('identity$uon$ucarrier'(sK98),X0) ),
inference(resolution,[status(thm)],[d13,d15]) ).
cnf(d17,plain,
( empty('the$ucarrier'(sK98))
| ~ element(X0,'the$ucarrier'(sK98))
| 'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),X0) = apply('identity$uon$ucarrier'(sK98),X0) ),
inference(resolution,[status(thm)],[d9,d16]) ).
cnf(d18,plain,
( empty('the$ucarrier'(sK98))
| 'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),sK99) = apply('identity$uon$ucarrier'(sK98),sK99) ),
inference(resolution,[status(thm)],[d17,c101]) ).
cnf(d19,plain,
( empty('the$ucarrier'(sK98))
| 'apply$uas$uelement'('the$ucarrier'(sK98),'the$ucarrier'(sK98),'identity$uon$ucarrier'(sK98),sK99) = sK99 ),
inference(demodulation,[status(thm)],[d18,d7]) ).
cnf(d20,plain,
empty('the$ucarrier'(sK98)),
inference(resolution,[status(thm)],[c102,d19]) ).
cnf(d21,plain,
( 'empty$ucarrier'(sK98)
| ~ 'one$usorted$ustr'(sK98) ),
inference(resolution,[status(thm)],[d20,c39]) ).
cnf(d22,plain,
~ 'one$usorted$ustr'(sK98),
inference(resolution,[status(thm)],[c99,d21]) ).
cnf(d23,plain,
$false,
inference(resolution,[status(thm)],[c100,d22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU353+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/5.38 % Computer : n017.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sat Sep 26 09:13:24 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.17/7.17 % SZS status Theorem for theBenchmark.p
% 13.17/7.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------