%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWW961+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 : n018.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:05 PM UTC 2025
% Result : Theorem 3.09s 0.72s
% Output : CNFRefutation 3.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 44 ( 29 unt; 0 def)
% Number of atoms : 74 ( 12 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 : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 5 con; 0-2 aty)
% Number of variables : 47 ( 14 sgn 18 !; 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(176,plain,
~ pred_attacker(name_objective),
inference(cnf,[status(esa)],[co0_negated]) ).
cnf(l0,plain,
~ pred_attacker(name_objective),
inference(instantiation,[status(thm)],[176]) ).
fof(ax114,plain,
! [VAR_V_128] :
( pred_attacker(tuple_client_B_out_6(VAR_V_128))
=> pred_attacker(VAR_V_128) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax114) ).
cnf(114,plain,
( ~ pred_attacker(tuple_client_B_out_6(X0))
| pred_attacker(X0) ),
inference(cnf,[status(esa)],[ax114]) ).
cnf(l1,plain,
( ~ pred_attacker(tuple_client_B_out_6(name_objective))
| pred_attacker(name_objective) ),
inference(instantiation,[status(thm)],[114]) ).
fof(ax173,plain,
! [VAR_0X40SID_60X305,VAR_AENC_NA_A_60X307,VAR_AENC_NB_60X306,VAR_SIGN_A_PKA_60X308] :
( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_60X305),constr_adec(VAR_AENC_NB_60X306,name_skB))
& pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_60X306))
& pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(VAR_AENC_NA_A_60X307,name_skB)))
& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_60X307))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_60X308,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_60X308)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax173) ).
cnf(173,plain,
( ~ pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(X2,name_skB)))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS))))
| ~ pred_eq_bitstring_bitstring(name_Nb(X3),constr_adec(X1,name_skB))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(cnf,[status(esa)],[ax173]) ).
cnf(l2,plain,
( ~ pred_attacker(tuple_client_B_in_2(tuple_out_2(constr_pkey(name_skB))))
| ~ pred_attacker(tuple_client_B_in_5(constr_CONST_0x30))
| ~ pred_attacker(tuple_client_B_in_3(tuple_out_2(constr_pkey(name_skB))))
| ~ pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(tuple_out_2(constr_pkey(name_skB)),name_skB)))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(tuple_out_2(constr_pkey(name_skB)),constr_pkey(name_skS))))
| ~ pred_eq_bitstring_bitstring(name_Nb(X3_2),constr_adec(constr_CONST_0x30,name_skB))
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(instantiation,[status(thm)],[173]) ).
fof(ax89,plain,
! [VAR_X_41,VAR_Y_42] : pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax89) ).
cnf(89,plain,
pred_eq_bitstring_bitstring(X0,X1),
inference(cnf,[status(esa)],[ax89]) ).
cnf(l21,plain,
pred_eq_bitstring_bitstring(constr_assoc_pair_2_get_1(tuple_assoc_pair(X0_25,name_Nb(X3_2))),constr_tuple_2_get_0x30(tuple_2(constr_adec(constr_CONST_0x30,name_skB),X1_24))),
inference(instantiation,[status(thm)],[89]) ).
fof(ax80,plain,
! [VAR_K_20X30,VAR_M_19] : constr_getmess(constr_sign(VAR_M_19,VAR_K_20X30)) = VAR_M_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax80) ).
cnf(80,plain,
constr_getmess(constr_sign(X0,X1)) = X0,
inference(cnf,[status(esa)],[ax80]) ).
cnf(l26,plain,
constr_getmess(constr_sign(constr_tuple_2_get_0x30(constr_checksign(tuple_out_2(constr_pkey(name_skB)),constr_pkey(name_skS))),X1_26)) = constr_tuple_2_get_0x30(constr_checksign(tuple_out_2(constr_pkey(name_skB)),constr_pkey(name_skS))),
inference(instantiation,[status(thm)],[80]) ).
fof(ax124,plain,
! [VAR_V_165] :
( pred_attacker(VAR_V_165)
=> pred_attacker(tuple_client_B_in_2(VAR_V_165)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax124) ).
cnf(124,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_2(X0)) ),
inference(cnf,[status(esa)],[ax124]) ).
cnf(l7,plain,
( ~ pred_attacker(tuple_out_2(constr_pkey(name_skB)))
| pred_attacker(tuple_client_B_in_2(tuple_out_2(constr_pkey(name_skB)))) ),
inference(instantiation,[status(thm)],[124]) ).
fof(ax81,plain,
! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax81) ).
cnf(81,plain,
constr_checksign(constr_sign(X0,X1),constr_pkey(X1)) = X0,
inference(cnf,[status(esa)],[ax81]) ).
cnf(l22,plain,
constr_checksign(constr_sign(name_A,X1_22),constr_pkey(X1_22)) = name_A,
inference(instantiation,[status(thm)],[81]) ).
fof(ax166,plain,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax166) ).
cnf(166,plain,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
inference(cnf,[status(esa)],[ax166]) ).
cnf(l8,plain,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
inference(instantiation,[status(thm)],[166]) ).
cnf(l23,plain,
pred_eq_bitstring_bitstring(constr_checksign(constr_sign(name_A,X1_22),constr_pkey(X1_22)),constr_getmess(constr_sign(constr_tuple_2_get_0x30(constr_checksign(tuple_out_2(constr_pkey(name_skB)),constr_pkey(name_skS))),X1_26))),
inference(instantiation,[status(thm)],[89]) ).
cnf(l14,plain,
pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(tuple_out_2(constr_pkey(name_skB)),name_skB))),
inference(instantiation,[status(thm)],[89]) ).
fof(ax85,plain,
! [VAR_X0X30_11,VAR_X1_12] : constr_assoc_pair_2_get_1(tuple_assoc_pair(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax85) ).
cnf(85,plain,
constr_assoc_pair_2_get_1(tuple_assoc_pair(X0,X1)) = X1,
inference(cnf,[status(esa)],[ax85]) ).
cnf(l25,plain,
constr_assoc_pair_2_get_1(tuple_assoc_pair(X0_25,name_Nb(X3_2))) = name_Nb(X3_2),
inference(instantiation,[status(thm)],[85]) ).
fof(ax120,plain,
! [VAR_V_153] :
( pred_attacker(VAR_V_153)
=> pred_attacker(tuple_client_B_in_5(VAR_V_153)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax120) ).
cnf(120,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_5(X0)) ),
inference(cnf,[status(esa)],[ax120]) ).
cnf(l10,plain,
( ~ pred_attacker(constr_CONST_0x30)
| pred_attacker(tuple_client_B_in_5(constr_CONST_0x30)) ),
inference(instantiation,[status(thm)],[120]) ).
fof(ax151,plain,
pred_attacker(constr_CONST_0x30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax151) ).
cnf(151,plain,
pred_attacker(constr_CONST_0x30),
inference(cnf,[status(esa)],[ax151]) ).
cnf(l11,plain,
pred_attacker(constr_CONST_0x30),
inference(instantiation,[status(thm)],[151]) ).
fof(ax88,plain,
! [VAR_X0X30_0X30,VAR_X1_0X30] : constr_tuple_2_get_0x30(tuple_2(VAR_X0X30_0X30,VAR_X1_0X30)) = VAR_X0X30_0X30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax88) ).
cnf(88,plain,
constr_tuple_2_get_0x30(tuple_2(X0,X1)) = X0,
inference(cnf,[status(esa)],[ax88]) ).
cnf(l24,plain,
constr_tuple_2_get_0x30(tuple_2(constr_adec(constr_CONST_0x30,name_skB),X1_24)) = constr_adec(constr_CONST_0x30,name_skB),
inference(instantiation,[status(thm)],[88]) ).
fof(ax122,plain,
! [VAR_V_159] :
( pred_attacker(VAR_V_159)
=> pred_attacker(tuple_client_B_in_3(VAR_V_159)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax122) ).
cnf(122,plain,
( ~ pred_attacker(X0)
| pred_attacker(tuple_client_B_in_3(X0)) ),
inference(cnf,[status(esa)],[ax122]) ).
cnf(l15,plain,
( ~ pred_attacker(tuple_out_2(constr_pkey(name_skB)))
| pred_attacker(tuple_client_B_in_3(tuple_out_2(constr_pkey(name_skB)))) ),
inference(instantiation,[status(thm)],[122]) ).
cnf(l17,plain,
pred_attacker(tuple_out_2(constr_pkey(name_skB))),
inference(instantiation,[status(thm)],[166]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l21,l26,l7,l22,l8,l23,l14,l25,l10,l11,l24,l15,l17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW961+1 : TPTP v9.0.0. Released v7.4.0.
% 0.07/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n018.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 15:01:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 0.18/0.50 % launching worker at depth: 11
% 3.09/0.72 % SZS status Theorem for theBenchmark
% 3.09/0.72 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------