%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW967+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:14:57 AM UTC 2026
% Result : Theorem 121.36s 18.58s
% Output : CNFRefutation 121.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 9
% Syntax : Number of formulae : 33 ( 14 unt; 0 def)
% Number of atoms : 87 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 99 ( 45 ~; 41 |; 7 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 5 con; 0-3 aty)
% Number of variables : 48 ( 20 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax83,axiom,
! [VAR_X_81,VAR_Y_82] : pred_eq_bitstring_bitstring(VAR_X_81,VAR_Y_82),
file('theBenchmark.p',ax83) ).
fof(ax109,axiom,
! [VAR_V_172] :
( pred_attacker(tuple_client_A_out_9(VAR_V_172))
=> pred_attacker(VAR_V_172) ),
file('theBenchmark.p',ax109) ).
fof(ax120,axiom,
! [VAR_V_223] :
( pred_attacker(VAR_V_223)
=> pred_attacker(tuple_client_A_in_8(VAR_V_223)) ),
file('theBenchmark.p',ax120) ).
fof(ax122,axiom,
! [VAR_V_229] :
( pred_attacker(VAR_V_229)
=> pred_attacker(tuple_client_A_in_6(VAR_V_229)) ),
file('theBenchmark.p',ax122) ).
fof(ax124,axiom,
! [VAR_V_235] :
( pred_attacker(VAR_V_235)
=> pred_attacker(tuple_client_A_in_4(VAR_V_235)) ),
file('theBenchmark.p',ax124) ).
fof(ax126,axiom,
! [VAR_V_241] :
( pred_attacker(VAR_V_241)
=> pred_attacker(tuple_client_A_in_2(VAR_V_241)) ),
file('theBenchmark.p',ax126) ).
fof(ax171,axiom,
! [VAR_0X40SID_598,VAR_ENC_KAB_A0X27_60X300X30,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_ENC_NB_596,VAR_ENC_SUCC_NA0X27_599] :
( ( pred_attacker(tuple_client_A_in_2(VAR_ENC_NA_B_ENC_KAB_A_597))
& pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_598),constr_tuple_4_get_0x30(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas)))
& pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(VAR_ENC_NA_B_ENC_KAB_A_597,name_Kas)))
& pred_attacker(tuple_client_A_in_4(VAR_ENC_NB_596))
& pred_attacker(tuple_client_A_in_6(VAR_ENC_KAB_A0X27_60X300X30))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas)))
& pred_attacker(tuple_client_A_in_8(VAR_ENC_SUCC_NA0X27_599))
& pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(VAR_ENC_NB_596,VAR_ENC_NA_B_ENC_KAB_A_597,VAR_0X40SID_598)),constr_cbc_dec_1(VAR_ENC_SUCC_NA0X27_599,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(VAR_ENC_KAB_A0X27_60X300X30,name_Kas)))) )
=> pred_attacker(tuple_client_A_out_9(name_objective)) ),
file('theBenchmark.p',ax171) ).
fof(co0,conjecture,
pred_attacker(name_objective),
file('theBenchmark.p',co0) ).
fof(co0_neg,negated_conjecture,
~ pred_attacker(name_objective),
inference(assume_negation,[status(cth)],[co0]) ).
cnf(c_119,plain,
pred_eq_bitstring_bitstring(A,B),
inference(clausify,[status(thm)],[ax83]) ).
cnf(c_145,plain,
( pred_attacker(A)
| ~ pred_attacker(tuple_client_A_out_9(A)) ),
inference(clausify,[status(thm)],[ax109]) ).
cnf(c_156,plain,
( pred_attacker(tuple_client_A_in_8(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax120]) ).
cnf(c_158,plain,
( pred_attacker(tuple_client_A_in_6(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax122]) ).
cnf(c_160,plain,
( pred_attacker(tuple_client_A_in_4(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax124]) ).
cnf(c_162,plain,
( pred_attacker(tuple_client_A_in_2(A))
| ~ pred_attacker(A) ),
inference(clausify,[status(thm)],[ax126]) ).
cnf(c_198,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(B))
| ~ pred_eq_bitstring_bitstring(name_Na(C),constr_tuple_4_get_0x30(constr_cbc_dec_4(B,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(B,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(A))
| ~ pred_attacker(tuple_client_A_in_6(E))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(E,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(D))
| ~ pred_eq_bitstring_bitstring(tuple_succ(name_Na0x27(A,B,C)),constr_cbc_dec_1(D,constr_tuple_2_get_0x30_bitstring(constr_cbc_dec_2(E,name_Kas)))) ),
inference(clausify,[status(thm)],[ax171]) ).
fof(ax142,axiom,
pred_attacker(constr_CONST_4),
file('theBenchmark.p',ax142) ).
cnf(c_308,plain,
pred_attacker(constr_CONST_4),
inference(clausify,[status(thm)],[ax142]) ).
cnf(c_317,negated_conjecture,
~ pred_attacker(name_objective),
inference(clausify,[status(thm)],[co0_neg]) ).
cnf(c_341,negated_conjecture,
~ pred_attacker(tuple_client_A_out_9(name_objective)),
inference(resolve,[status(thm)],[c_145,c_317]) ).
cnf(c_3380,plain,
pred_attacker(tuple_client_A_in_2(constr_CONST_4)),
inference(resolve,[status(thm)],[c_162,c_308]) ).
cnf(c_3381,plain,
pred_attacker(tuple_client_A_in_4(constr_CONST_4)),
inference(resolve,[status(thm)],[c_160,c_308]) ).
cnf(c_3382,plain,
pred_attacker(tuple_client_A_in_6(constr_CONST_4)),
inference(resolve,[status(thm)],[c_158,c_308]) ).
cnf(c_32246,plain,
pred_attacker(tuple_client_A_in_8(tuple_client_A_in_6(constr_CONST_4))),
inference(resolve,[status(thm)],[c_156,c_3382]) ).
cnf(c_32710,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(D))
| ~ pred_eq_bitstring_bitstring(name_Na(E),constr_tuple_4_get_0x30(constr_cbc_dec_4(D,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(D,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(C))
| ~ pred_attacker(tuple_client_A_in_6(B))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_cbc_dec_2(B,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_198,c_119]) ).
cnf(c_32711,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(D))
| ~ pred_eq_bitstring_bitstring(name_Na(E),constr_tuple_4_get_0x30(constr_cbc_dec_4(D,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(D,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(C))
| ~ pred_attacker(tuple_client_A_in_6(B))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32710,c_119]) ).
cnf(c_32712,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(C))
| ~ pred_eq_bitstring_bitstring(name_Na(D),constr_tuple_4_get_0x30(constr_cbc_dec_4(C,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(C,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_4(B))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32711,c_3382]) ).
cnf(c_32713,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(B))
| ~ pred_eq_bitstring_bitstring(name_Na(C),constr_tuple_4_get_0x30(constr_cbc_dec_4(B,name_Kas)))
| ~ pred_eq_bitstring_bitstring(name_B,constr_tuple_4_get_1(constr_cbc_dec_4(B,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32712,c_3381]) ).
cnf(c_32714,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(C))
| ~ pred_eq_bitstring_bitstring(name_Na(B),constr_tuple_4_get_0x30(constr_cbc_dec_4(C,name_Kas)))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32713,c_119]) ).
cnf(c_32715,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_2(B))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32714,c_119]) ).
cnf(c_32716,plain,
( pred_attacker(tuple_client_A_out_9(name_objective))
| ~ pred_attacker(tuple_client_A_in_8(A)) ),
inference(resolve,[status(thm)],[c_32715,c_3380]) ).
cnf(c_32708,plain,
~ pred_attacker(tuple_client_A_in_8(A)),
inference(resolve,[status(thm)],[c_32716,c_341]) ).
cnf(c_32709,plain,
$false,
inference(resolve,[status(thm)],[c_32708,c_32246]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW967+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 16:38:42 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.13/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.38 % Process 1689618 was started by sandbox2 on n006,
% 0.13/0.38 % Sat Sep 26 16:38:42 2026
% 0.13/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.40
% 0.13/0.40 % From the command line: assign(max_seconds, 300).
% 0.13/0.40
% 0.13/0.40 % SInE: 75 to sos, 99 to usable, of 174 axioms (tolerance 2.00, depth 0 fixpoint).
% 121.36/18.58
% 121.36/18.58 % SZS status Theorem for theBenchmark
% 121.36/18.58
% 121.36/18.58 % Proof 1 at 12.33 (+ 4.97) seconds.
% 121.36/18.58 % Length of proof is 24.
% 121.36/18.58 % Level of proof is 4.
% 121.36/18.58 % Maximum clause weight is 102.000.
% 121.36/18.58 % Given clauses 41.
% 121.36/18.58
% 121.36/18.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------