%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV750-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 09:04:39 AM UTC 2026
% Result : Unsatisfiable 2.79s 16.38s
% Output : CNFRefutation 2.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 15
% Syntax : Number of clauses : 49 ( 28 unt; 0 nHn; 30 RR)
% Number of literals : 77 ( 27 equ; 32 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 15 con; 0-3 aty)
% Number of variables : 79 ( 25 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_inf__sup__ord_I4_J_0,axiom,
( 'c$ulessequals'(X1,'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X2,X1,X0),X0)
| ~ 'class$uLattices$uOlattice'(X0) ) ).
cnf(cls_sup__idem_0,axiom,
( 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X1,X0) = X1
| ~ 'class$uLattices$uOupper$u$usemilattice'(X0) ) ).
cnf(cls_sup__absorb1_0,axiom,
( ~ 'c$ulessequals'(X2,X1,X0)
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X2,X0) = X1
| ~ 'class$uLattices$uOupper$u$usemilattice'(X0) ) ).
cnf(cls_insert__code_1,axiom,
hBOOL(hAPP('c$uSet$uOinsert'(X0,X1,X2),X0)) ).
cnf(cls_insert__iff_1,axiom,
hBOOL('c$uin'(X0,'c$uSet$uOinsert'(X0,X1,X2),X2)) ).
cnf(cls_insert__absorb_0,axiom,
( ~ hBOOL('c$uin'(X0,X1,X2))
| 'c$uSet$uOinsert'(X0,X1,X2) = X1 ) ).
cnf(cls_unique__session__keys_1,axiom,
( ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X7,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X7),'c$uMessage$uOmsg$uOMPair'(X0,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X8),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey',X5),X9))))),'c$uList$uOset'(X2,'tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X3,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X3),'c$uMessage$uOmsg$uOMPair'(X1,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X4),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey',X5),X6))))),'c$uList$uOset'(X2,'tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| ~ hBOOL('c$uin'(X2,'c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent')))
| X0 = X1 ) ).
cnf(cls_mem__def_1,axiom,
( ~ hBOOL(hAPP(X1,X0))
| hBOOL('c$uin'(X0,X1,X2)) ) ).
cnf(cls_conjecture_2,negated_conjecture,
hBOOL('c$uin'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent'))) ).
cnf(cls_conjecture_4,negated_conjecture,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uAa','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uONonce'('v$uNAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uKa'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uKa'),'c$uMessage$uOmsg$uOAgent'('v$uAa')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')) ).
cnf(cls_conjecture_7,negated_conjecture,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uA','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uA'),'c$uMessage$uOmsg$uOMPair'('v$uNA','c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uB'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uB'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOAgent'('v$uA')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')) ).
cnf(cls_conjecture_9,negated_conjecture,
'v$uK' = 'v$uKa' ).
cnf(cls_conjecture_10,negated_conjecture,
( 'v$uNA' != 'c$uMessage$uOmsg$uONonce'('v$uNAa')
| 'v$uK' != 'v$uKa' ) ).
cnf(clsarity_nat__Lattices_Oupper__semilattice,axiom,
'class$uLattices$uOupper$u$usemilattice'('tc$unat') ).
cnf(clsarity_nat__Lattices_Olattice,axiom,
'class$uLattices$uOlattice'('tc$unat') ).
cnf(c80,plain,
( 'c$ulessequals'(X1,'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X2,X1,X0),X0)
| ~ 'class$uLattices$uOlattice'(X0) ),
inference(clausification,[status(esa)],[cls_inf__sup__ord_I4_J_0]) ).
cnf(c94,plain,
( 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X1,X0) = X1
| ~ 'class$uLattices$uOupper$u$usemilattice'(X0) ),
inference(clausification,[status(esa)],[cls_sup__idem_0]) ).
cnf(c164,plain,
( ~ 'c$ulessequals'(X2,X1,X0)
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X1,X2,X0) = X1
| ~ 'class$uLattices$uOupper$u$usemilattice'(X0) ),
inference(clausification,[status(esa)],[cls_sup__absorb1_0]) ).
cnf(c183,plain,
hBOOL(hAPP('c$uSet$uOinsert'(X0,X1,X2),X0)),
inference(clausification,[status(esa)],[cls_insert__code_1]) ).
cnf(c246,plain,
hBOOL('c$uin'(X0,'c$uSet$uOinsert'(X0,X1,X2),X2)),
inference(clausification,[status(esa)],[cls_insert__iff_1]) ).
cnf(c254,plain,
( ~ hBOOL('c$uin'(X0,X1,X2))
| 'c$uSet$uOinsert'(X0,X1,X2) = X1 ),
inference(clausification,[status(esa)],[cls_insert__absorb_0]) ).
cnf(c612,plain,
( ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X7,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X7),'c$uMessage$uOmsg$uOMPair'(X0,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X8),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey',X5),X9))))),'c$uList$uOset'(X2,'tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X3,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X3),'c$uMessage$uOmsg$uOMPair'(X1,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X4),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey',X5),X6))))),'c$uList$uOset'(X2,'tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| ~ hBOOL('c$uin'(X2,'c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent')))
| X0 = X1 ),
inference(clausification,[status(esa)],[cls_unique__session__keys_1]) ).
cnf(c629,plain,
( ~ hBOOL(hAPP(X1,X0))
| hBOOL('c$uin'(X0,X1,X2)) ),
inference(clausification,[status(esa)],[cls_mem__def_1]) ).
cnf(c652,plain,
hBOOL('c$uin'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent'))),
inference(clausification,[status(esa)],[cls_conjecture_2]) ).
cnf(c654,plain,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uAa','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uONonce'('v$uNAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uKa'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uKa'),'c$uMessage$uOmsg$uOAgent'('v$uAa')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')),
inference(clausification,[status(esa)],[cls_conjecture_4]) ).
cnf(c657,plain,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uA','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uA'),'c$uMessage$uOmsg$uOMPair'('v$uNA','c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uB'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uB'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOAgent'('v$uA')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')),
inference(clausification,[status(esa)],[cls_conjecture_7]) ).
cnf(c659,plain,
'v$uK' = 'v$uKa',
inference(clausification,[status(esa)],[cls_conjecture_9]) ).
cnf(c660,plain,
( 'v$uNA' != 'c$uMessage$uOmsg$uONonce'('v$uNAa')
| 'v$uK' != 'v$uKa' ),
inference(clausification,[status(esa)],[cls_conjecture_10]) ).
cnf(c672,plain,
'class$uLattices$uOupper$u$usemilattice'('tc$unat'),
inference(clausification,[status(esa)],[clsarity_nat__Lattices_Oupper__semilattice]) ).
cnf(c675,plain,
'class$uLattices$uOlattice'('tc$unat'),
inference(clausification,[status(esa)],[clsarity_nat__Lattices_Olattice]) ).
cnf(d0,plain,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uAa','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uONonce'('v$uNAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uKa'),'c$uMessage$uOmsg$uOAgent'('v$uAa')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')),
inference(demodulation,[status(thm)],[c654,c659]) ).
cnf(d1,plain,
hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer','v$uAa','c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uONonce'('v$uNAa'),'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'('v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK','v$uBa'),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),'c$uMessage$uOmsg$uOAgent'('v$uAa')))))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent')),
inference(demodulation,[status(thm)],[d0,c659]) ).
cnf(d2,plain,
( ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X1,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X1),'c$uMessage$uOmsg$uOMPair'(X0,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X2),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),X3))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| ~ hBOOL('c$uin'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent')))
| X0 = 'c$uMessage$uOmsg$uONonce'('v$uNAa') ),
inference(resolution,[status(thm)],[d1,c612]) ).
cnf(d3,plain,
'c$uSet$uOinsert'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','tc$uList$uOlist'('tc$uEvent$uOevent')) = 'c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared',
inference(resolution,[status(thm)],[c254,c652]) ).
cnf(d4,plain,
hBOOL(hAPP('c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared','v$uevso')),
inference(superposition,[status(thm)],[d3,c183]) ).
cnf(d5,plain,
( 'c$uSet$uOinsert'(X1,X0,X2) = X0
| ~ hBOOL(hAPP(X0,X1)) ),
inference(resolution,[status(thm)],[c629,c254]) ).
cnf(d6,plain,
'c$uSet$uOinsert'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared',X0) = 'c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared',
inference(resolution,[status(thm)],[d5,d4]) ).
cnf(d7,plain,
hBOOL('c$uin'('v$uevso','c$uNS$u$uShared$u$uMirabelle$uOns$u$ushared',X0)),
inference(superposition,[status(thm)],[d6,c246]) ).
cnf(d8,plain,
( ~ hBOOL('c$uin'('c$uEvent$uOevent$uOSays'('c$uMessage$uOagent$uOServer',X1,'c$uMessage$uOmsg$uOCrypt'(hAPP('c$uPublic$uOshrK',X1),'c$uMessage$uOmsg$uOMPair'(X0,'c$uMessage$uOmsg$uOMPair'('c$uMessage$uOmsg$uOAgent'(X2),'c$uMessage$uOmsg$uOMPair'(hAPP('c$uMessage$uOmsg$uOKey','v$uK'),X3))))),'c$uList$uOset'('v$uevso','tc$uEvent$uOevent'),'tc$uEvent$uOevent'))
| X0 = 'c$uMessage$uOmsg$uONonce'('v$uNAa') ),
inference(resolution,[status(thm)],[d7,d2]) ).
cnf(d9,plain,
'v$uNA' = 'c$uMessage$uOmsg$uONonce'('v$uNAa'),
inference(resolution,[status(thm)],[d8,c657]) ).
cnf(d10,plain,
( 'v$uK' != 'v$uK'
| 'v$uNA' != 'c$uMessage$uOmsg$uONonce'('v$uNAa') ),
inference(demodulation,[status(thm)],[c660,c659]) ).
cnf(d11,plain,
'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X0,'tc$unat') = X0,
inference(resolution,[status(thm)],[c94,c672]) ).
cnf(d12,plain,
( ~ 'class$uLattices$uOlattice'('tc$unat')
| 'c$ulessequals'(X0,X0,'tc$unat') ),
inference(superposition,[status(thm)],[d11,c80]) ).
cnf(d13,plain,
'c$ulessequals'(X0,X0,'tc$unat'),
inference(resolution,[status(thm)],[c675,d12]) ).
cnf(d14,plain,
( ~ 'class$uLattices$uOupper$u$usemilattice'('tc$unat')
| 'c$uLattices$uOupper$u$usemilattice$u$uclass$uOsup'(X0,X0,'tc$unat') = X0 ),
inference(resolution,[status(thm)],[c164,d13]) ).
cnf(d15,plain,
( ~ 'class$uLattices$uOupper$u$usemilattice'('tc$unat')
| X0 = X0 ),
inference(demodulation,[status(thm)],[d14,d11]) ).
cnf(d16,plain,
X0 = X0,
inference(resolution,[status(thm)],[c672,d15]) ).
cnf(d17,plain,
'v$uNA' != 'c$uMessage$uOmsg$uONonce'('v$uNAa'),
inference(resolution,[status(thm)],[d16,d10]) ).
cnf(d18,plain,
$false,
inference(resolution,[status(thm)],[d17,d9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV750-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 14:54:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.79/16.38 % SZS status Unsatisfiable for theBenchmark.p
% 2.79/16.38 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------