%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW960+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 : 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 09:12:35 AM UTC 2026
% Result : Theorem 86.96s 13.20s
% Output : CNFRefutation 86.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 32
% Syntax : Number of formulae : 120 ( 33 unt; 0 def)
% Number of atoms : 302 ( 25 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 323 ( 141 ~; 144 |; 18 &)
% ( 0 <=>; 20 =>; 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 : 33 ( 33 usr; 9 con; 0-2 aty)
% Number of variables : 184 ( 51 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax34,axiom,
'constr$uCONST$u3' != 'name$uA' ).
fof(ax35,axiom,
'constr$uCONST$u3' != 'name$uB' ).
fof(ax78,axiom,
! [X0,X1] : 'constr$uadec'('constr$uaenc'(X1,'constr$upkey'(X0)),X0) = X1 ).
fof(ax81,axiom,
! [X0,X1] : 'constr$uchecksign'('constr$usign'(X1,X0),'constr$upkey'(X0)) = X1 ).
fof(ax82,axiom,
! [X0,X1] : 'constr$utuple$u2$uget$u1$ubitstring'('tuple$u2'(X0,X1)) = X1 ).
fof(ax86,axiom,
! [X0,X1] : 'pred$ueq$ubitstring$ubitstring'(X0,X1) ).
fof(ax93,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('constr$upkey'(X0)) ) ).
fof(ax100,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0)) ) ).
fof(ax101,axiom,
! [X0] :
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax102,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,X1)) ) ).
fof(ax105,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1)) ) ).
fof(ax113,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax115,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uB$uout$u4'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax119,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0)) ) ).
fof(ax121,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0)) ) ).
fof(ax123,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0)) ) ).
fof(ax126,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uA$uout$u5'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax132,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0)) ) ).
fof(ax134,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0)) ) ).
fof(ax138,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('constr$uadec'(X0,X1)) ) ).
fof(ax140,axiom,
'pred$uattacker'('constr$uCONST$u3') ).
fof(ax144,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$u2'(X0,X1)) ) ).
fof(ax151,axiom,
'pred$uattacker'('name$uB') ).
fof(ax152,axiom,
'pred$uattacker'('name$uA') ).
fof(ax155,axiom,
'pred$utable'('tuple$ukeys'('name$uA','constr$upkey'('name$uskA'))) ).
fof(ax156,axiom,
'pred$utable'('tuple$ukeys'('name$uB','constr$upkey'('name$uskB'))) ).
fof(ax162,axiom,
! [X0,X1,X2] :
( ( 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uI','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))
& 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
& 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u2$uget$u0x30'('constr$uadec'(X1,'name$uskA'))) )
=> 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))) ) ).
fof(ax164,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$uadec'(X1,'name$uskB'))) )
=> 'pred$uattacker'('tuple$uclient$uB$uout$u4'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X1,'name$uskB')),'name$uNb'(X0)),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))) ) ).
fof(ax165,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$uadec'(X1,'name$uskB')))
& 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uadec'(X2,'name$uskB')) )
=> 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ) ).
fof(ax166,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(ax167,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(c34,plain,
'constr$uCONST$u3' != 'name$uA',
inference(clausification,[status(esa)],[ax34]) ).
cnf(c35,plain,
'constr$uCONST$u3' != 'name$uB',
inference(clausification,[status(esa)],[ax35]) ).
cnf(c78,plain,
'constr$uadec'('constr$uaenc'(X0,'constr$upkey'(X1)),X1) = X0,
inference(clausification,[status(esa)],[ax78]) ).
cnf(c81,plain,
'constr$uchecksign'('constr$usign'(X0,X1),'constr$upkey'(X1)) = X0,
inference(clausification,[status(esa)],[ax81]) ).
cnf(c82,plain,
'constr$utuple$u2$uget$u1$ubitstring'('tuple$u2'(X0,X1)) = X1,
inference(clausification,[status(esa)],[ax82]) ).
cnf(c86,plain,
'pred$ueq$ubitstring$ubitstring'(X0,X1),
inference(clausification,[status(esa)],[ax86]) ).
cnf(c93,plain,
( 'pred$uattacker'('constr$upkey'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax93]) ).
cnf(c100,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax100]) ).
cnf(c101,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'(X0)) ),
inference(clausification,[status(esa)],[ax101]) ).
cnf(c102,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax102]) ).
cnf(c105,plain,
( 'pred$uattacker'('tuple$ukey$uregister$userver$uin$u1'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax105]) ).
cnf(c113,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uB$uout$u6'(X0)) ),
inference(clausification,[status(esa)],[ax113]) ).
cnf(c115,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uB$uout$u4'(X0)) ),
inference(clausification,[status(esa)],[ax115]) ).
cnf(c119,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax119]) ).
cnf(c121,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax121]) ).
cnf(c123,plain,
( 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax123]) ).
cnf(c126,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uA$uout$u5'(X0)) ),
inference(clausification,[status(esa)],[ax126]) ).
cnf(c132,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax132]) ).
cnf(c134,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax134]) ).
cnf(c138,plain,
( 'pred$uattacker'('constr$uadec'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax138]) ).
cnf(c140,plain,
'pred$uattacker'('constr$uCONST$u3'),
inference(clausification,[status(esa)],[ax140]) ).
cnf(c144,plain,
( 'pred$uattacker'('tuple$u2'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax144]) ).
cnf(c151,plain,
'pred$uattacker'('name$uB'),
inference(clausification,[status(esa)],[ax151]) ).
cnf(c152,plain,
'pred$uattacker'('name$uA'),
inference(clausification,[status(esa)],[ax152]) ).
cnf(c155,plain,
'pred$utable'('tuple$ukeys'('name$uA','constr$upkey'('name$uskA'))),
inference(clausification,[status(esa)],[ax155]) ).
cnf(c156,plain,
'pred$utable'('tuple$ukeys'('name$uB','constr$upkey'('name$uskB'))),
inference(clausification,[status(esa)],[ax156]) ).
cnf(c162,plain,
( ~ 'pred$ueq$ubitstring$ubitstring'('name$uI','constr$utuple$u2$uget$u0x30'('constr$uchecksign'(X1,'constr$upkey'('name$uskS'))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X2),'constr$utuple$u2$uget$u0x30'('constr$uadec'(X0,'name$uskA')))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X0,'name$uskA')),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X1,'constr$upkey'('name$uskS'))))))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0)) ),
inference(clausification,[status(esa)],[ax162]) ).
cnf(c164,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| ~ '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$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uadec'(X0,'name$uskB')))
| 'pred$uattacker'('tuple$uclient$uB$uout$u4'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X0,'name$uskB')),'name$uNb'(X1)),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS')))))) ),
inference(clausification,[status(esa)],[ax164]) ).
cnf(c165,plain,
( ~ '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$ueq$ubitstring$ubitstring'('name$uNb'(X2),'constr$uadec'(X1,'name$uskB'))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$uadec'(X0,'name$uskB')))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0)) ),
inference(clausification,[status(esa)],[ax165]) ).
cnf(c166,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)],[ax166]) ).
cnf(c167,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)],[ax167]) ).
cnf(c168,plain,
~ 'pred$uattacker'('tuple$u2'('name$uNb'(sK115),'name$uobjective')),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'pred$uattacker'('name$uNb'(sK115))
| ~ 'pred$uattacker'('name$uobjective') ),
inference(resolution,[status(thm)],[c144,c168]) ).
cnf(d1,plain,
( ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,'name$uB'))
| 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uB','constr$upkey'('name$uskB')),'name$uskS'))) ),
inference(resolution,[status(thm)],[c166,c156]) ).
cnf(d2,plain,
( ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('name$uB')
| 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uB','constr$upkey'('name$uskB')),'name$uskS'))) ),
inference(resolution,[status(thm)],[d1,c102]) ).
cnf(d3,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uB','constr$upkey'('name$uskB')),'name$uskS')))
| ~ 'pred$uattacker'('name$uB') ),
inference(factoring,[status(thm)],[d2]) ).
cnf(d4,plain,
'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uB','constr$upkey'('name$uskB')),'name$uskS'))),
inference(resolution,[status(thm)],[c151,d3]) ).
cnf(d5,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$uadec'(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)],[c86,c165]) ).
cnf(d6,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$uadec'(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)],[c121,d5]) ).
cnf(d7,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$uadec'(X1,'name$uskB')) ),
inference(resolution,[status(thm)],[d6,c86]) ).
cnf(d8,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$uadec'(X1,'name$uskB')) ),
inference(factoring,[status(thm)],[d7]) ).
cnf(d9,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)],[c86,d8]) ).
cnf(d10,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)],[c119,d9]) ).
cnf(d11,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c123,d10]) ).
cnf(d12,plain,
( ~ 'pred$uattacker'(X1)
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d11,c100]) ).
cnf(d13,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(factoring,[status(thm)],[d12]) ).
cnf(d14,plain,
'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')),
inference(resolution,[status(thm)],[d13,d4]) ).
cnf(d15,plain,
'pred$uattacker'('name$uobjective'),
inference(resolution,[status(thm)],[d14,c113]) ).
cnf(d16,plain,
~ 'pred$uattacker'('name$uNb'(sK115)),
inference(resolution,[status(thm)],[d15,d0]) ).
cnf(d17,plain,
( ~ 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,'name$uA'))
| 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS'))) ),
inference(resolution,[status(thm)],[c166,c155]) ).
cnf(d18,plain,
( ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('name$uA')
| 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS'))) ),
inference(resolution,[status(thm)],[d17,c102]) ).
cnf(d19,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS')))
| ~ 'pred$uattacker'('name$uA') ),
inference(factoring,[status(thm)],[d18]) ).
cnf(d20,plain,
'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS'))),
inference(resolution,[status(thm)],[c152,d19]) ).
cnf(d21,plain,
'pred$uattacker'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS')),
inference(resolution,[status(thm)],[d20,c101]) ).
cnf(d22,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$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X1,'name$uskB')),'name$uNb'(X2)),'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)],[c86,c164]) ).
cnf(d23,plain,
( 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X1,'name$uskB')),'name$uNb'(X2)),'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)],[d22,c115]) ).
cnf(d24,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X0,'name$uskB')),'name$uNb'(X1)),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))) ),
inference(resolution,[status(thm)],[c86,d23]) ).
cnf(d25,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'('constr$usign'(X0,'name$uskS')))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
| 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X1,'name$uskB')),'name$uNb'(X2)),'constr$utuple$u2$uget$u1$ubitstring'(X0))) ),
inference(superposition,[status(thm)],[c81,d24]) ).
cnf(d26,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'('constr$usign'('tuple$u2'(X0,X1),'name$uskS')))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X2))
| 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X2,'name$uskB')),'name$uNb'(X3)),X1)) ),
inference(superposition,[status(thm)],[c82,d25]) ).
cnf(d27,plain,
( ~ 'pred$uattacker'('constr$usign'('tuple$u2'(X3,X2),'name$uskS'))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X0,'name$uskB')),'name$uNb'(X1)),X2)) ),
inference(resolution,[status(thm)],[d26,c123]) ).
cnf(d28,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('constr$uaenc'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X0,'name$uskB')),'name$uNb'(X1)),'constr$upkey'('name$uskA'))) ),
inference(resolution,[status(thm)],[d27,d21]) ).
cnf(d29,plain,
( ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'('constr$uaenc'(X0,'constr$upkey'(X1)))
| 'pred$uattacker'(X0) ),
inference(superposition,[status(thm)],[c78,c138]) ).
cnf(d30,plain,
( ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X1)
| 'pred$utable'('tuple$ukeys'(X0,X1))
| X0 = 'name$uB'
| X0 = 'name$uA' ),
inference(resolution,[status(thm)],[c167,c105]) ).
cnf(d31,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)],[d30,c166]) ).
cnf(d32,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)],[c102,d31]) ).
cnf(d33,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u3',X0),'name$uskS')))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u3' = 'name$uB'
| 'constr$uCONST$u3' = 'name$uA' ),
inference(resolution,[status(thm)],[d32,c140]) ).
cnf(d34,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u3',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u3' = 'name$uB'
| 'constr$uCONST$u3' = 'name$uA' ),
inference(factoring,[status(thm)],[d33]) ).
cnf(d35,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u3',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0)
| 'constr$uCONST$u3' = 'name$uB' ),
inference(resolution,[status(thm)],[c34,d34]) ).
cnf(d36,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('constr$uCONST$u3',X0),'name$uskS')))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c35,d35]) ).
cnf(d37,plain,
( 'pred$uattacker'('constr$usign'('tuple$u2'('constr$uCONST$u3',X0),'name$uskS'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d36,c101]) ).
cnf(d38,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X2,'constr$upkey'('name$uskS'))))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u2$uget$u0x30'('constr$uadec'(X1,'name$uskA'))) ),
inference(resolution,[status(thm)],[c86,c162]) ).
cnf(d39,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X0,'name$uskA')),'constr$utuple$u2$uget$u1$ubitstring'('constr$uchecksign'(X1,'constr$upkey'('name$uskS')))))) ),
inference(resolution,[status(thm)],[d38,c86]) ).
cnf(d40,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'('constr$usign'(X0,'name$uskS')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')),'constr$utuple$u2$uget$u1$ubitstring'(X0)))) ),
inference(superposition,[status(thm)],[c81,d39]) ).
cnf(d41,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'('constr$usign'('tuple$u2'(X0,X1),'name$uskS')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X2,'name$uskA')),X1))) ),
inference(superposition,[status(thm)],[c82,d40]) ).
cnf(d42,plain,
( ~ 'pred$uattacker'('constr$usign'('tuple$u2'(X2,X1),'name$uskS'))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X0,'name$uskA')),X1))) ),
inference(resolution,[status(thm)],[d41,c134]) ).
cnf(d43,plain,
( ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0))
| 'pred$uattacker'('tuple$uclient$uA$uout$u5'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X0,'name$uskA')),X1))) ),
inference(resolution,[status(thm)],[d42,d37]) ).
cnf(d44,plain,
( 'pred$uattacker'('constr$uaenc'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')),X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d43,c126]) ).
cnf(d45,plain,
( 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| ~ 'pred$uattacker'('constr$upkey'(X0)) ),
inference(resolution,[status(thm)],[d44,d29]) ).
cnf(d46,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')))
| ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c93,d45]) ).
cnf(d47,plain,
( ~ 'pred$uattacker'(X1)
| 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X1,'name$uskA')))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d46,c132]) ).
cnf(d48,plain,
( 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'('constr$uadec'(X0,'name$uskA')))
| ~ 'pred$uattacker'(X0) ),
inference(factoring,[status(thm)],[d47]) ).
cnf(d49,plain,
( ~ 'pred$uattacker'('constr$uaenc'(X0,'constr$upkey'('name$uskA')))
| 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'(X0)) ),
inference(superposition,[status(thm)],[c78,d48]) ).
cnf(d50,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('constr$utuple$u2$uget$u1$ubitstring'('tuple$u2'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$uadec'(X0,'name$uskB')),'name$uNb'(X1)))) ),
inference(resolution,[status(thm)],[d49,d28]) ).
cnf(d51,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X0))
| 'pred$uattacker'('name$uNb'(X1)) ),
inference(demodulation,[status(thm)],[d50,c82]) ).
cnf(d52,plain,
( 'pred$uattacker'('name$uNb'(X1))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c121,d51]) ).
cnf(d53,plain,
'pred$uattacker'('name$uNb'(X0)),
inference(resolution,[status(thm)],[d52,d4]) ).
cnf(d54,plain,
$false,
inference(resolution,[status(thm)],[d53,d16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW960+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.54 % Computer : n017.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.54 % CPULimit : 300
% 0.09/0.54 % WCLimit : 300
% 0.09/0.54 % DateTime : Sat Sep 26 16:33:51 UTC 2026
% 0.09/0.54 % CPUTime :
% 0.09/0.54 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 86.96/13.20 % SZS status Theorem for theBenchmark.p
% 86.96/13.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------