%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:12:36 AM UTC 2026
% Result : Theorem 54.88s 8.66s
% Output : CNFRefutation 54.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 27
% Syntax : Number of formulae : 92 ( 26 unt; 0 def)
% Number of atoms : 234 ( 27 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 249 ( 107 ~; 110 |; 15 &)
% ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 7 con; 0-4 aty)
% Number of variables : 164 ( 48 sgn 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax4,axiom,
'constr$uCONST$u0x30' != 'name$uA' ).
fof(ax5,axiom,
'constr$uCONST$u0x30' != 'name$uB' ).
fof(ax80,axiom,
! [X0,X1] : 'constr$uchecksign'('constr$usign'(X1,X0),'constr$upkey'(X0)) = X1 ).
fof(ax84,axiom,
! [X0,X1] : 'constr$uecb$udec$u1'('constr$uecb$uenc$u1'(X1,'constr$upkey'(X0)),X0) = X1 ).
fof(ax86,axiom,
! [X0,X1,X2,X3] : 'constr$uecb$uenc$u3'(X1,X2,X3,X0) = 'tuple$u3'('constr$uecb$uenc$u1'(X1,X0),'constr$uecb$uenc$u1'(X2,X0),'constr$uecb$uenc$u1'(X3,X0)) ).
fof(ax89,axiom,
! [X0,X1] : 'constr$utuple$u2$uget$u1$ubitstring'('tuple$u2'(X0,X1)) = X1 ).
fof(ax95,axiom,
! [X0,X1] : 'pred$ueq$ubitstring$ubitstring'(X0,X1) ).
fof(ax101,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('constr$utuple$u2$uget$u0x30$ubitstring'(X0)) ) ).
fof(ax105,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('constr$upkey'(X0)) ) ).
fof(ax113,axiom,
! [X0] :
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax114,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,X1)) ) ).
fof(ax117,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1)) ) ).
fof(ax130,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('constr$uecb$udec$u1'(X0,X1)) ) ).
fof(ax133,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax135,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uB$uout$u4'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax139,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0)) ) ).
fof(ax141,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0)) ) ).
fof(ax143,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0)) ) ).
fof(ax161,axiom,
'pred$uattacker'('constr$uCONST$u0x30') ).
fof(ax169,axiom,
! [X0,X1,X2] :
( 'pred$uattacker'('tuple$u3'(X0,X1,X2))
=> 'pred$uattacker'(X1) ) ).
fof(ax171,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$u2'(X0,X1)) ) ).
fof(ax190,axiom,
'pred$uattacker'('tuple$uclient$uB$uout$u1'('name$uB','name$uA')) ).
fof(ax191,axiom,
! [X0,X1,X2] :
( ( 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))
& 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uecb$udec$u2'(X1,'name$uskB'))) )
=> 'pred$uattacker'('tuple$uclient$uB$uout$u4'('constr$uecb$uenc$u3'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uecb$udec$u2'(X1,'name$uskB')),'name$uNb'(X0),'name$uB','constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))) ) ).
fof(ax192,axiom,
! [X0,X1,X2,X3] :
( ( 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X3))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X3,'constr$upkey'('name$uskS'))))
& 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uecb$udec$u2'(X1,'name$uskB')))
& 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uecb$udec$u1'(X2,'name$uskB')) )
=> 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ) ).
fof(ax193,axiom,
! [X0,X1,X2] :
( ( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X2,X0))
& 'pred$utable'('tuple$ukeys'(X0,X1)) )
=> 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'(X0,X1),'name$uskS'))) ) ).
fof(ax194,axiom,
! [X0,X1] :
( ( 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1))
& X0 != 'name$uA'
& X0 != 'name$uB' )
=> 'pred$utable'('tuple$ukeys'(X0,X1)) ) ).
fof(co0,conjecture,
! [X0] : 'pred$uattacker'('tuple$u2'('name$uNb'(X0),'name$uobjective')) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0] : 'pred$uattacker'('tuple$u2'('name$uNb'(X0),'name$uobjective')),
inference(negate_conjecture,[status(cth)],[co0]) ).
cnf(c4,plain,
'constr$uCONST$u0x30' != 'name$uA',
inference(clausification,[status(esa)],[ax4]) ).
cnf(c5,plain,
'constr$uCONST$u0x30' != 'name$uB',
inference(clausification,[status(esa)],[ax5]) ).
cnf(c80,plain,
'constr$uchecksign'('constr$usign'(X0,X1),'constr$upkey'(X1)) = X0,
inference(clausification,[status(esa)],[ax80]) ).
cnf(c84,plain,
'constr$uecb$udec$u1'('constr$uecb$uenc$u1'(X0,'constr$upkey'(X1)),X1) = X0,
inference(clausification,[status(esa)],[ax84]) ).
cnf(c86,plain,
'constr$uecb$uenc$u3'(X0,X1,X2,X3) = 'tuple$u3'('constr$uecb$uenc$u1'(X0,X3),'constr$uecb$uenc$u1'(X1,X3),'constr$uecb$uenc$u1'(X2,X3)),
inference(clausification,[status(esa)],[ax86]) ).
cnf(c89,plain,
'constr$utuple$u2$uget$u1$ubitstring'('tuple$u2'(X0,X1)) = X1,
inference(clausification,[status(esa)],[ax89]) ).
cnf(c95,plain,
'pred$ueq$ubitstring$ubitstring'(X0,X1),
inference(clausification,[status(esa)],[ax95]) ).
cnf(c101,plain,
( 'pred$uattacker'('constr$utuple$u2$uget$u0x30$ubitstring'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax101]) ).
cnf(c105,plain,
( 'pred$uattacker'('constr$upkey'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax105]) ).
cnf(c113,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0)) ),
inference(clausification,[status(esa)],[ax113]) ).
cnf(c114,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax114]) ).
cnf(c117,plain,
( 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax117]) ).
cnf(c130,plain,
( 'pred$uattacker'('constr$uecb$udec$u1'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax130]) ).
cnf(c133,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uB$uout$u6'(X0)) ),
inference(clausification,[status(esa)],[ax133]) ).
cnf(c135,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uB$uout$u4'(X0)) ),
inference(clausification,[status(esa)],[ax135]) ).
cnf(c139,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax139]) ).
cnf(c141,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax141]) ).
cnf(c143,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax143]) ).
cnf(c161,plain,
'pred$uattacker'('constr$uCONST$u0x30'),
inference(clausification,[status(esa)],[ax161]) ).
cnf(c169,plain,
( 'pred$uattacker'(X1)
| ~ 'pred$uattacker'('tuple$u3'(X0,X1,X2)) ),
inference(clausification,[status(esa)],[ax169]) ).
cnf(c171,plain,
( 'pred$uattacker'('tuple$u2'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax171]) ).
cnf(c190,plain,
'pred$uattacker'('tuple$uclient$uB$uout$u1'('name$uB','name$uA')),
inference(clausification,[status(esa)],[ax190]) ).
cnf(c191,plain,
( ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| 'pred$uattacker'('tuple$uclient$uB$uout$u4'('constr$uecb$uenc$u3'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uecb$udec$u2'(X0,'name$uskB')),'name$uNb'(X1),'name$uB','constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uecb$udec$u2'(X0,'name$uskB'))) ),
inference(clausification,[status(esa)],[ax191]) ).
cnf(c192,plain,
( ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uecb$udec$u2'(X3,'name$uskB')))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uecb$udec$u1'(X1,'name$uskB'))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ),
inference(clausification,[status(esa)],[ax192]) ).
cnf(c193,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'(X0,X1),'name$uskS')))
| ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X2,X0))
| ~ 'pred$utable'('tuple$ukeys'(X0,X1)) ),
inference(clausification,[status(esa)],[ax193]) ).
cnf(c194,plain,
( 'pred$utable'('tuple$ukeys'(X0,X1))
| ~ 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1))
| X0 = 'name$uA'
| X0 = 'name$uB' ),
inference(clausification,[status(esa)],[ax194]) ).
cnf(c195,plain,
~ 'pred$uattacker'('tuple$u2'('name$uNb'(sK201),'name$uobjective')),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'pred$uattacker'('name$uNb'(sK201))
| ~ 'pred$uattacker'('name$uobjective') ),
inference(resolution,[status(thm)],[c171,c195]) ).
cnf(d1,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X2))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X1),'constr$uecb$udec$u1'(X2,'name$uskB'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X0,'constr$upkey'('name$uskS')))) ),
inference(resolution,[status(thm)],[c95,c192]) ).
cnf(d2,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X3))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X2),'constr$uecb$udec$u1'(X3,'name$uskB'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X1,'constr$upkey'('name$uskS'))))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c141,d1]) ).
cnf(d3,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X2)
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uecb$udec$u1'(X1,'name$uskB')) ),
inference(resolution,[status(thm)],[d2,c95]) ).
cnf(d4,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uecb$udec$u1'(X1,'name$uskB')) ),
inference(factoring,[status(thm)],[d3]) ).
cnf(d5,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ),
inference(resolution,[status(thm)],[c95,d4]) ).
cnf(d6,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X1))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c139,d5]) ).
cnf(d7,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c143,d6]) ).
cnf(d8,plain,
( ~ 'pred$uattacker'(X1)
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d7,c101]) ).
cnf(d9,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(factoring,[status(thm)],[d8]) ).
cnf(d10,plain,
'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')),
inference(resolution,[status(thm)],[d9,c190]) ).
cnf(d11,plain,
'pred$uattacker'('name$uobjective'),
inference(resolution,[status(thm)],[d10,c133]) ).
cnf(d12,plain,
~ 'pred$uattacker'('name$uNb'(sK201)),
inference(resolution,[status(thm)],[d11,d0]) ).
cnf(d13,plain,
( ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'('constr$uecb$uenc$u1'(X0,'constr$upkey'(X1)))
| 'pred$uattacker'(X0) ),
inference(superposition,[status(thm)],[c84,c130]) ).
cnf(d14,plain,
( ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X1)
| 'pred$utable'('tuple$ukeys'(X0,X1))
| X0 = 'name$uB'
| X0 = 'name$uA' ),
inference(resolution,[status(thm)],[c194,c117]) ).
cnf(d15,plain,
( ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X2,X0))
| 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'(X0,X1),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X1)
| X0 = 'name$uB'
| X0 = 'name$uA' ),
inference(resolution,[status(thm)],[d14,c193]) ).
cnf(d16,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'(X0,X2),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X2)
| X0 = 'name$uB'
| X0 = 'name$uA'
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c114,d15]) ).
cnf(d17,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u0x30',X0),'name$uskS')))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u0x30' = 'name$uB'
| 'constr$uCONST$u0x30' = 'name$uA' ),
inference(resolution,[status(thm)],[d16,c161]) ).
cnf(d18,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u0x30',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u0x30' = 'name$uB'
| 'constr$uCONST$u0x30' = 'name$uA' ),
inference(factoring,[status(thm)],[d17]) ).
cnf(d19,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u0x30',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u0x30' = 'name$uB' ),
inference(resolution,[status(thm)],[c4,d18]) ).
cnf(d20,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u0x30',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c5,d19]) ).
cnf(d21,plain,
( 'pred$uattacker'('constr$usign'('tuple$u2'('constr$uCONST$u0x30',X0),'name$uskS'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d20,c113]) ).
cnf(d22,plain,
( 'pred$uattacker'('constr$uecb$uenc$u1'(X2,X1))
| ~ 'pred$uattacker'('constr$uecb$uenc$u3'(X0,X2,X3,X1)) ),
inference(superposition,[status(thm)],[c86,c169]) ).
cnf(d23,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
| 'pred$uattacker'('tuple$uclient$uB$uout$u4'('constr$uecb$uenc$u3'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uecb$udec$u2'(X1,'name$uskB')),'name$uNb'(X2),'name$uB','constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X0,'constr$upkey'('name$uskS'))))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X0,'constr$upkey'('name$uskS')))) ),
inference(resolution,[status(thm)],[c95,c191]) ).
cnf(d24,plain,
( 'pred$uattacker'('constr$uecb$uenc$u3'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uecb$udec$u2'(X1,'name$uskB')),'name$uNb'(X2),'name$uB','constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X0,'constr$upkey'('name$uskS')))))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X0,'constr$upkey'('name$uskS')))) ),
inference(resolution,[status(thm)],[d23,c135]) ).
cnf(d25,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('constr$uecb$uenc$u3'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uecb$udec$u2'(X0,'name$uskB')),'name$uNb'(X1),'name$uB','constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))) ),
inference(resolution,[status(thm)],[c95,d24]) ).
cnf(d26,plain,
( 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X2),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X1,'constr$upkey'('name$uskS')))))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0)) ),
inference(resolution,[status(thm)],[d25,d22]) ).
cnf(d27,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X1),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c141,d26]) ).
cnf(d28,plain,
( ~ 'pred$uattacker'(X2)
| 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X1),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d27,c143]) ).
cnf(d29,plain,
( 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X1),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X0,'constr$upkey'('name$uskS')))))
| ~ 'pred$uattacker'(X0) ),
inference(factoring,[status(thm)],[d28]) ).
cnf(d30,plain,
( ~ 'pred$uattacker'('constr$usign'(X0,'name$uskS'))
| 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X1),'constr$utuple$u2$uget$u1$ubitstring'(X0))) ),
inference(superposition,[status(thm)],[c80,d29]) ).
cnf(d31,plain,
( ~ 'pred$uattacker'('constr$usign'('tuple$u2'(X0,X1),'name$uskS'))
| 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X2),X1)) ),
inference(superposition,[status(thm)],[c89,d30]) ).
cnf(d32,plain,
( ~ 'pred$uattacker'(X1)
| 'pred$uattacker'('constr$uecb$uenc$u1'('name$uNb'(X0),X1)) ),
inference(resolution,[status(thm)],[d31,d21]) ).
cnf(d33,plain,
( 'pred$uattacker'('name$uNb'(X1))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('constr$upkey'(X0)) ),
inference(resolution,[status(thm)],[d32,d13]) ).
cnf(d34,plain,
( 'pred$uattacker'('name$uNb'(X1))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c105,d33]) ).
cnf(d35,plain,
'pred$uattacker'('name$uNb'(X0)),
inference(resolution,[status(thm)],[d34,c190]) ).
cnf(d36,plain,
$false,
inference(resolution,[status(thm)],[d35,d12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW964+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n018.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Sat Sep 26 16:41:22 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.56 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 54.88/8.66 % SZS status Theorem for theBenchmark.p
% 54.88/8.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------