%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW959+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 14.09s 13.95s
% Output : CNFRefutation 14.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of formulae : 48 ( 20 unt; 0 def)
% Number of atoms : 108 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 108 ( 48 ~; 46 |; 7 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 7 con; 0-2 aty)
% Number of variables : 59 ( 30 sgn 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax86,axiom,
! [X0,X1] : 'pred$ueq$ubitstring$ubitstring'(X0,X1) ).
fof(ax91,axiom,
'pred$uattacker'('tuple$utrue') ).
fof(ax102,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$ukey$uretrieval$userver$uin$u1'(X0,X1)) ) ).
fof(ax113,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'(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(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(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(co0,conjecture,
'pred$uattacker'('name$uobjective') ).
fof(negated_conjecture,negated_conjecture,
~ 'pred$uattacker'('name$uobjective'),
inference(negate_conjecture,[status(cth)],[co0]) ).
cnf(c86,plain,
'pred$ueq$ubitstring$ubitstring'(X0,X1),
inference(clausification,[status(esa)],[ax86]) ).
cnf(c91,plain,
'pred$uattacker'('tuple$utrue'),
inference(clausification,[status(esa)],[ax91]) ).
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(c113,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uB$uout$u6'(X0)) ),
inference(clausification,[status(esa)],[ax113]) ).
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(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(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(c168,plain,
~ 'pred$uattacker'('name$uobjective'),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,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(d1,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)],[d0,c102]) ).
cnf(d2,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uA','constr$upkey'('name$uskA')),'name$uskS')))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c152,d1]) ).
cnf(d3,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)],[d2,c91]) ).
cnf(d4,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(d5,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)],[d4,c102]) ).
cnf(d6,plain,
( 'pred$uattacker'('tuple$ukey$uretrieval$userver$uout$u2'('constr$usign'('tuple$u2'('name$uB','constr$upkey'('name$uskB')),'name$uskS')))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[c151,d5]) ).
cnf(d7,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)],[d6,d3]) ).
cnf(d8,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(d9,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNb'(X0),'constr$uadec'(X1,'name$uskB')) ),
inference(resolution,[status(thm)],[d8,c86]) ).
cnf(d10,plain,
( ~ 'pred$uattacker'('tuple$uclient$uB$uin$u2'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ),
inference(resolution,[status(thm)],[c86,d9]) ).
cnf(d11,plain,
( ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u3'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X0))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')) ),
inference(resolution,[status(thm)],[d10,c123]) ).
cnf(d12,plain,
( ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'('tuple$uclient$uB$uin$u5'(X1))
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d11,c121]) ).
cnf(d13,plain,
( ~ 'pred$uattacker'(X2)
| 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d12,c119]) ).
cnf(d14,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d13,d7]) ).
cnf(d15,plain,
( 'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d14,d7]) ).
cnf(d16,plain,
'pred$uattacker'('tuple$uclient$uB$uout$u6'('name$uobjective')),
inference(resolution,[status(thm)],[d15,d7]) ).
cnf(d17,plain,
'pred$uattacker'('name$uobjective'),
inference(resolution,[status(thm)],[d16,c113]) ).
cnf(d18,plain,
$false,
inference(resolution,[status(thm)],[c168,d17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW959+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/10.41 % Computer : n015.cluster.edu
% 0.12/10.41 % Model : x86_64 x86_64
% 0.12/10.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.41 % Memory : 8046.5625MB
% 0.12/10.41 % OS : Linux 6.8.0-71-generic
% 0.12/10.41 % CPULimit : 300
% 0.12/10.41 % WCLimit : 300
% 0.12/10.41 % DateTime : Sat Sep 26 16:41:54 UTC 2026
% 0.12/10.41 % CPUTime :
% 0.12/10.41 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.09/13.95 % SZS status Theorem for theBenchmark.p
% 14.09/13.95 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------