%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW968+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 : n005.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 34.70s 4.94s
% Output : CNFRefutation 34.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 22
% Syntax : Number of formulae : 86 ( 19 unt; 0 def)
% Number of atoms : 295 ( 6 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 403 ( 194 ~; 176 |; 18 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 8 con; 0-5 aty)
% Number of variables : 237 ( 114 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax80,axiom,
! [X0,X1,X2] : 'constr$ucbc$udec$u2'('constr$ucbc$uenc$u2'(X1,X2,X0),X0) = 'tuple$u2'(X1,X2) ).
fof(ax83,axiom,
! [X0,X1,X2,X3,X4] : 'constr$ucbc$u4$uget$u2$uprefixes'('constr$ucbc$uenc$u4'(X1,X2,X3,X4,X0)) = 'constr$ucbc$uenc$u2'(X1,X2,X0) ).
fof(ax88,axiom,
! [X0,X1] : 'constr$udec'('constr$uenc'(X1,X0),X0) = 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(ax102,axiom,
'pred$uattacker'('tuple$utrue') ).
fof(ax106,axiom,
! [X0] :
( 'pred$uattacker'('tuple$userver$uS$uout$u2'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax107,axiom,
! [X0,X1,X2] :
( ( 'pred$uattacker'(X2)
& 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$userver$uS$uin$u1'(X0,X1,X2)) ) ).
fof(ax113,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('constr$udec'(X0,X1)) ) ).
fof(ax121,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uA$uout$u9'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax129,axiom,
! [X0] :
( 'pred$uattacker'('tuple$uclient$uA$uout$u10'(X0))
=> 'pred$uattacker'(X0) ) ).
fof(ax134,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0)) ) ).
fof(ax136,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X0)) ) ).
fof(ax138,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0)) ) ).
fof(ax140,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0)) ) ).
fof(ax151,axiom,
! [X0] :
( 'pred$uattacker'(X0)
=> 'pred$uattacker'('constr$ucbc$u4$uget$u2$uprefixes'(X0)) ) ).
fof(ax170,axiom,
! [X0,X1] :
( ( 'pred$uattacker'(X1)
& 'pred$uattacker'(X0) )
=> 'pred$uattacker'('tuple$u2'(X0,X1)) ) ).
fof(ax176,axiom,
'pred$uattacker'('name$uI') ).
fof(ax185,axiom,
! [X0,X1,X2,X3,X4] :
( ( 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X2,'name$uKas')))
& 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X2,'name$uKas')))
& 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X3))
& 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$ucbc$udec$u2'(X1,'name$uKas')))
& 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X4))
& 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X3,X2,X0)),'constr$ucbc$udec$u1'(X4,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X1,'name$uKas')))) )
=> 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1')) ) ).
fof(ax186,axiom,
! [X0,X1,X2,X3,X4] :
( ( 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X2))
& 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X2,'name$uKas')))
& 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X2,'name$uKas')))
& 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X3))
& 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
& 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$ucbc$udec$u2'(X1,'name$uKas')))
& 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X4))
& 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X3,X2,X0)),'constr$ucbc$udec$u1'(X4,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X1,'name$uKas')))) )
=> 'pred$uattacker'('tuple$uclient$uA$uout$u10'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X1,'name$uKas'))))) ) ).
fof(ax188,axiom,
! [X0,X1,X2,X3] :
( 'pred$uattacker'('tuple$userver$uS$uin$u1'(X1,X2,X3))
=> 'pred$uattacker'('tuple$userver$uS$uout$u2'('constr$ucbc$uenc$u4'(X3,X2,'name$uKab$u66'(X0),'constr$ucbc$uenc$u2'('name$uKab$u66'(X0),X1,'name$uKbs'),'name$uKas'))) ) ).
fof(co0,conjecture,
'pred$uattacker'('tuple$u2'('name$uobjective1','name$uobjective2')) ).
fof(negated_conjecture,negated_conjecture,
~ 'pred$uattacker'('tuple$u2'('name$uobjective1','name$uobjective2')),
inference(negate_conjecture,[status(cth)],[co0]) ).
cnf(c80,plain,
'constr$ucbc$udec$u2'('constr$ucbc$uenc$u2'(X0,X1,X2),X2) = 'tuple$u2'(X0,X1),
inference(clausification,[status(esa)],[ax80]) ).
cnf(c83,plain,
'constr$ucbc$u4$uget$u2$uprefixes'('constr$ucbc$uenc$u4'(X0,X1,X2,X3,X4)) = 'constr$ucbc$uenc$u2'(X0,X1,X4),
inference(clausification,[status(esa)],[ax83]) ).
cnf(c88,plain,
'constr$udec'('constr$uenc'(X0,X1),X1) = X0,
inference(clausification,[status(esa)],[ax88]) ).
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(c102,plain,
'pred$uattacker'('tuple$utrue'),
inference(clausification,[status(esa)],[ax102]) ).
cnf(c106,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$userver$uS$uout$u2'(X0)) ),
inference(clausification,[status(esa)],[ax106]) ).
cnf(c107,plain,
( 'pred$uattacker'('tuple$userver$uS$uin$u1'(X0,X1,X2))
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax107]) ).
cnf(c113,plain,
( 'pred$uattacker'('constr$udec'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax113]) ).
cnf(c121,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uA$uout$u9'(X0)) ),
inference(clausification,[status(esa)],[ax121]) ).
cnf(c129,plain,
( 'pred$uattacker'(X0)
| ~ 'pred$uattacker'('tuple$uclient$uA$uout$u10'(X0)) ),
inference(clausification,[status(esa)],[ax129]) ).
cnf(c134,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax134]) ).
cnf(c136,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax136]) ).
cnf(c138,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax138]) ).
cnf(c140,plain,
( 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax140]) ).
cnf(c151,plain,
( 'pred$uattacker'('constr$ucbc$u4$uget$u2$uprefixes'(X0))
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax151]) ).
cnf(c170,plain,
( 'pred$uattacker'('tuple$u2'(X0,X1))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(clausification,[status(esa)],[ax170]) ).
cnf(c176,plain,
'pred$uattacker'('name$uI'),
inference(clausification,[status(esa)],[ax176]) ).
cnf(c185,plain,
( 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X0,X3,X2)),'constr$ucbc$udec$u1'(X1,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X4,'name$uKas'))))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X4))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$ucbc$udec$u2'(X4,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X3,'name$uKas')))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X2),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X3,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X0)) ),
inference(clausification,[status(esa)],[ax185]) ).
cnf(c186,plain,
( ~ 'pred$ueq$ubitstring$ubitstring'('name$uA','constr$utuple$u2$uget$u1'('constr$ucbc$udec$u2'(X3,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X2,X1,X0)),'constr$ucbc$udec$u1'(X4,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X3,'name$uKas'))))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X4))
| 'pred$uattacker'('tuple$uclient$uA$uout$u10'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X3,'name$uKas')))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X1,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X1,'name$uKas'))) ),
inference(clausification,[status(esa)],[ax186]) ).
cnf(c188,plain,
( 'pred$uattacker'('tuple$userver$uS$uout$u2'('constr$ucbc$uenc$u4'(X2,X1,'name$uKab$u66'(X3),'constr$ucbc$uenc$u2'('name$uKab$u66'(X3),X0,'name$uKbs'),'name$uKas')))
| ~ 'pred$uattacker'('tuple$userver$uS$uin$u1'(X0,X1,X2)) ),
inference(clausification,[status(esa)],[ax188]) ).
cnf(c189,plain,
~ 'pred$uattacker'('tuple$u2'('name$uobjective1','name$uobjective2')),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'pred$uattacker'('constr$ucbc$uenc$u4'(X0,X1,X2,X3,X4))
| 'pred$uattacker'('constr$ucbc$uenc$u2'(X0,X1,X4)) ),
inference(superposition,[status(thm)],[c83,c151]) ).
cnf(d1,plain,
( 'pred$uattacker'('constr$ucbc$uenc$u4'(X2,X1,'name$uKab$u66'(X3),'constr$ucbc$uenc$u2'('name$uKab$u66'(X3),X0,'name$uKbs'),'name$uKas'))
| ~ 'pred$uattacker'('tuple$userver$uS$uin$u1'(X0,X1,X2)) ),
inference(resolution,[status(thm)],[c188,c106]) ).
cnf(d2,plain,
( 'pred$uattacker'('constr$ucbc$uenc$u2'(X2,X1,'name$uKas'))
| ~ 'pred$uattacker'('tuple$userver$uS$uin$u1'(X0,X1,X2)) ),
inference(resolution,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
( ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0)
| 'pred$uattacker'('constr$ucbc$uenc$u2'(X0,X1,'name$uKas')) ),
inference(resolution,[status(thm)],[d2,c107]) ).
cnf(d4,plain,
( ~ 'pred$uattacker'('constr$uenc'(X0,X1))
| ~ 'pred$uattacker'(X1)
| 'pred$uattacker'(X0) ),
inference(superposition,[status(thm)],[c88,c113]) ).
cnf(d5,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| 'pred$uattacker'('tuple$uclient$uA$uout$u10'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X4,'name$uKas')))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X2),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X0,'name$uKas')))
| ~ 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X1,X0,X2)),'constr$ucbc$udec$u1'(X3,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X4,'name$uKas'))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X0,'name$uKas'))) ),
inference(resolution,[status(thm)],[c95,c186]) ).
cnf(d6,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| 'pred$uattacker'('tuple$uclient$uA$uout$u10'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X2,'name$uKas')))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X1),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X0,'name$uKas')))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X0,'name$uKas'))) ),
inference(resolution,[status(thm)],[d5,c95]) ).
cnf(d7,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| 'pred$uattacker'('tuple$uclient$uA$uout$u10'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X2,'name$uKas')))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X1,'name$uKas'))) ),
inference(resolution,[status(thm)],[c95,d6]) ).
cnf(d8,plain,
( 'pred$uattacker'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X3,'name$uKas'))))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X1,'name$uKas'))) ),
inference(resolution,[status(thm)],[d7,c129]) ).
cnf(d9,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X1))
| 'pred$uattacker'('constr$uenc'('name$uobjective2','constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X0,'name$uKas')))) ),
inference(resolution,[status(thm)],[c95,d8]) ).
cnf(d10,plain,
( 'pred$uattacker'('name$uobjective2')
| ~ 'pred$uattacker'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X1,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0)) ),
inference(resolution,[status(thm)],[d9,d4]) ).
cnf(d11,plain,
( ~ 'pred$uattacker'('name$uobjective1')
| ~ 'pred$uattacker'('name$uobjective2') ),
inference(resolution,[status(thm)],[c170,c189]) ).
cnf(d12,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X2),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X0,'name$uKas')))
| ~ 'pred$ueq$ubitstring$ubitstring'('tuple$usucc'('name$uNa0x27'(X1,X0,X2)),'constr$ucbc$udec$u1'(X3,'constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X4,'name$uKas'))))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X0,'name$uKas'))) ),
inference(resolution,[status(thm)],[c95,c185]) ).
cnf(d13,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X1),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X0,'name$uKas')))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uB','constr$utuple$u4$uget$u1'('constr$ucbc$udec$u4'(X0,'name$uKas'))) ),
inference(resolution,[status(thm)],[d12,c95]) ).
cnf(d14,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$ueq$ubitstring$ubitstring'('name$uNa'(X0),'constr$utuple$u4$uget$u0x30'('constr$ucbc$udec$u4'(X1,'name$uKas'))) ),
inference(resolution,[status(thm)],[c95,d13]) ).
cnf(d15,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1')) ),
inference(resolution,[status(thm)],[d14,c95]) ).
cnf(d16,plain,
( ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1')) ),
inference(resolution,[status(thm)],[d15,c140]) ).
cnf(d17,plain,
( ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X1))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d16,c138]) ).
cnf(d18,plain,
( ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d17,c136]) ).
cnf(d19,plain,
( ~ 'pred$uattacker'(X3)
| 'pred$uattacker'('tuple$uclient$uA$uout$u9'('name$uobjective1'))
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d18,c134]) ).
cnf(d20,plain,
( 'pred$uattacker'('name$uobjective1')
| ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d19,c121]) ).
cnf(d21,plain,
( 'pred$uattacker'('name$uobjective1')
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d20,c176]) ).
cnf(d22,plain,
( 'pred$uattacker'('name$uobjective1')
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d21,c176]) ).
cnf(d23,plain,
( 'pred$uattacker'('name$uobjective1')
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d22,c176]) ).
cnf(d24,plain,
'pred$uattacker'('name$uobjective1'),
inference(resolution,[status(thm)],[d23,c176]) ).
cnf(d25,plain,
~ 'pred$uattacker'('name$uobjective2'),
inference(resolution,[status(thm)],[d24,d11]) ).
cnf(d26,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X0))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X1))
| ~ 'pred$uattacker'('constr$utuple$u2$uget$u0x30$ubitstring'('constr$ucbc$udec$u2'(X0,'name$uKas'))) ),
inference(resolution,[status(thm)],[d25,d10]) ).
cnf(d27,plain,
( ~ 'pred$uattacker'('constr$ucbc$udec$u2'(X1,'name$uKas'))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X2))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'(X1))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X0)) ),
inference(resolution,[status(thm)],[d26,c101]) ).
cnf(d28,plain,
( ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u6'('constr$ucbc$uenc$u2'(X0,X1,'name$uKas')))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| ~ 'pred$uattacker'('tuple$u2'(X0,X1)) ),
inference(superposition,[status(thm)],[c80,d27]) ).
cnf(d29,plain,
( ~ 'pred$uattacker'('constr$ucbc$uenc$u2'(X0,X1,'name$uKas'))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| ~ 'pred$uattacker'('tuple$u2'(X0,X1)) ),
inference(resolution,[status(thm)],[d28,c136]) ).
cnf(d30,plain,
( ~ 'pred$uattacker'(X0)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X5)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X3))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X2))
| ~ 'pred$uattacker'('tuple$u2'(X0,X1)) ),
inference(resolution,[status(thm)],[d29,d3]) ).
cnf(d31,plain,
( ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u2'(X5))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d30,c170]) ).
cnf(d32,plain,
( ~ 'pred$uattacker'(X5)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u4'(X4))
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X3))
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d31,c140]) ).
cnf(d33,plain,
( ~ 'pred$uattacker'(X5)
| ~ 'pred$uattacker'('tuple$uclient$uA$uin$u8'(X4))
| ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d32,c138]) ).
cnf(d34,plain,
( ~ 'pred$uattacker'(X5)
| ~ 'pred$uattacker'(X4)
| ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d33,c134]) ).
cnf(d35,plain,
( ~ 'pred$uattacker'(X4)
| ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d34,c176]) ).
cnf(d36,plain,
( ~ 'pred$uattacker'(X3)
| ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d35,c176]) ).
cnf(d37,plain,
( ~ 'pred$uattacker'(X2)
| ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d36,c176]) ).
cnf(d38,plain,
( ~ 'pred$uattacker'(X1)
| ~ 'pred$uattacker'(X0) ),
inference(resolution,[status(thm)],[d37,c176]) ).
cnf(d39,plain,
~ 'pred$uattacker'(X0),
inference(resolution,[status(thm)],[d38,c176]) ).
cnf(d40,plain,
$false,
inference(resolution,[status(thm)],[d39,c102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW968+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.11/0.36 % Computer : n005.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 26 16:39:03 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 34.70/4.94 % SZS status Theorem for theBenchmark.p
% 34.70/4.94 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------