%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWW959+1 : TPTP v9.0.0. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 05:05:04 PM UTC 2025
% Result : Theorem 1.96s 0.59s
% Output : CNFRefutation 1.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 37 ( 22 unt; 0 def)
% Number of atoms : 67 ( 3 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 53 ( 23 ~; 20 |; 5 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 7 con; 0-2 aty)
% Number of variables : 28 ( 5 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co0,plain,
pred_attacker(name_objective),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co0) ).
fof(co0_negated,plain,
~ pred_attacker(name_objective),
inference(negate_conjecture,[status(cth)],[co0]) ).
cnf(168,plain,
~ pred_attacker(name_objective),
inference(cnf,[status(esa)],[co0_negated]) ).
cnf(l0,plain,
~ pred_attacker(name_objective),
inference(instantiation,[status(thm)],[168]) ).
fof(ax113,plain,
! [VAR_V_126] :
( pred_attacker(tuple_client_B_out_6(VAR_V_126))
=> pred_attacker(VAR_V_126) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax113) ).
cnf(113,plain,
( ~ pred_attacker(tuple_client_B_out_6(X0))
| pred_attacker(X0) ),
inference(cnf,[status(esa)],[ax113]) ).
cnf(l1,plain,
( ~ pred_attacker(tuple_client_B_out_6(name_objective))
| pred_attacker(name_objective) ),
inference(instantiation,[status(thm)],[113]) ).
fof(ax165,plain,
! [VAR_0X40SID_545,VAR_AENC_NA_A_547,VAR_AENC_NB_546,VAR_SIGN_A_PKA_548] :
( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_545),constr_adec(VAR_AENC_NB_546,name_skB))
& pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_546))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_547,name_skB)))
& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_547))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_548,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_548)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax165) ).
cnf(165,plain,
( ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_Nb(X2),constr_adec(X3,name_skB))
| ~ pred_attacker(tuple_client_B_in_3(X1))
| ~ pred_attacker(tuple_client_B_in_5(X3))
| ~ pred_attacker(tuple_client_B_in_2(X0))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(cnf,[status(esa)],[ax165]) ).
cnf(l2,plain,
( ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(tuple_out_1(constr_pkey(name_skA)),constr_pkey(name_skS))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(name_c,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_Nb(X2_2),constr_adec(constr_CONST_4,name_skB))
| ~ pred_attacker(tuple_client_B_in_3(name_c))
| ~ pred_attacker(tuple_client_B_in_5(constr_CONST_4))
| ~ pred_attacker(tuple_client_B_in_2(tuple_out_1(constr_pkey(name_skA))))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(instantiation,[status(thm)],[165]) ).
fof(ax86,plain,
! [VAR_X_35,VAR_Y_36] : pred_eq_bitstring_bitstring(VAR_X_35,VAR_Y_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax86) ).
cnf(86,plain,
pred_eq_bitstring_bitstring(X0,X1),
inference(cnf,[status(esa)],[ax86]) ).
cnf(l6,plain,
pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(name_c,name_skB))),
inference(instantiation,[status(thm)],[86]) ).
fof(ax123,plain,
! [VAR_V_163] :
( pred_attacker(VAR_V_163)
=> pred_attacker(tuple_client_B_in_2(VAR_V_163)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax123) ).
cnf(123,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_2(X0)) ),
inference(cnf,[status(esa)],[ax123]) ).
cnf(l17,plain,
( ~ pred_attacker(tuple_out_1(constr_pkey(name_skA)))
| pred_attacker(tuple_client_B_in_2(tuple_out_1(constr_pkey(name_skA)))) ),
inference(instantiation,[status(thm)],[123]) ).
fof(ax157,plain,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax157) ).
cnf(157,plain,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
inference(cnf,[status(esa)],[ax157]) ).
cnf(l18,plain,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
inference(instantiation,[status(thm)],[157]) ).
cnf(l13,plain,
pred_eq_bitstring_bitstring(name_Nb(X2_2),constr_adec(constr_CONST_4,name_skB)),
inference(instantiation,[status(thm)],[86]) ).
fof(ax79,plain,
! [VAR_K_16,VAR_M_15] : constr_dec(constr_enc(VAR_M_15,VAR_K_16),VAR_K_16) = VAR_M_15,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax79) ).
cnf(79,plain,
constr_dec(constr_enc(X0,X1),X1) = X0,
inference(cnf,[status(esa)],[ax79]) ).
cnf(l4,plain,
constr_dec(constr_enc(name_A,X1_4),X1_4) = name_A,
inference(instantiation,[status(thm)],[79]) ).
fof(ax121,plain,
! [VAR_V_157] :
( pred_attacker(VAR_V_157)
=> pred_attacker(tuple_client_B_in_3(VAR_V_157)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax121) ).
cnf(121,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_3(X0)) ),
inference(cnf,[status(esa)],[ax121]) ).
cnf(l15,plain,
( ~ pred_attacker(name_c)
| pred_attacker(tuple_client_B_in_3(name_c)) ),
inference(instantiation,[status(thm)],[121]) ).
fof(ax149,plain,
pred_attacker(name_c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax149) ).
cnf(149,plain,
pred_attacker(name_c),
inference(cnf,[status(esa)],[ax149]) ).
cnf(l16,plain,
pred_attacker(name_c),
inference(instantiation,[status(thm)],[149]) ).
cnf(l10,plain,
pred_eq_bitstring_bitstring(constr_dec(constr_enc(name_A,X1_4),X1_4),constr_tuple_2_get_0x30(constr_checksign(tuple_out_1(constr_pkey(name_skA)),constr_pkey(name_skS)))),
inference(instantiation,[status(thm)],[86]) ).
fof(ax119,plain,
! [VAR_V_151] :
( pred_attacker(VAR_V_151)
=> pred_attacker(tuple_client_B_in_5(VAR_V_151)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax119) ).
cnf(119,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_5(X0)) ),
inference(cnf,[status(esa)],[ax119]) ).
cnf(l12,plain,
( ~ pred_attacker(constr_CONST_4)
| pred_attacker(tuple_client_B_in_5(constr_CONST_4)) ),
inference(instantiation,[status(thm)],[119]) ).
fof(ax139,plain,
pred_attacker(constr_CONST_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax139) ).
cnf(139,plain,
pred_attacker(constr_CONST_4),
inference(cnf,[status(esa)],[ax139]) ).
cnf(l14,plain,
pred_attacker(constr_CONST_4),
inference(instantiation,[status(thm)],[139]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l6,l17,l18,l13,l4,l15,l16,l10,l12,l14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWW959+1 : TPTP v9.0.0. Released v7.4.0.
% 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 15:01:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 9
% 0.19/0.35 % launching worker at depth: 10
% 0.19/0.44 % launching worker at depth: 11
% 1.96/0.59 % SZS status Theorem for theBenchmark
% 1.96/0.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------