%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW965+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 03:08:36 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 16
% Syntax : Number of formulae : 60 ( 18 unt; 4 def)
% Number of atoms : 130 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 139 ( 69 ~; 54 |; 5 &)
% ( 4 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 5 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-2 aty)
% Number of variables : 54 ( 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f104,axiom,
! [VAR_X_41,VAR_Y_42] : pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,axiom,
! [VAR_V_69] :
( pred_attacker(tuple_out_3(VAR_V_69))
=> pred_attacker(VAR_V_69) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,axiom,
! [VAR_V_81] :
( pred_attacker(tuple_out_1(VAR_V_81))
=> pred_attacker(VAR_V_81) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [VAR_V_136] :
( pred_attacker(tuple_client_B_out_6(VAR_V_136))
=> pred_attacker(VAR_V_136) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,axiom,
! [VAR_V_161] :
( pred_attacker(VAR_V_161)
=> pred_attacker(tuple_client_B_in_5(VAR_V_161)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,axiom,
! [VAR_V_167] :
( pred_attacker(VAR_V_167)
=> pred_attacker(tuple_client_B_in_3(VAR_V_167)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [VAR_V_173] :
( pred_attacker(VAR_V_173)
=> pred_attacker(tuple_client_B_in_2(VAR_V_173)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [VAR_V_256] : pred_attacker(name_new0x2Dname(VAR_V_256)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f177,axiom,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f179,axiom,
pred_attacker(tuple_out_3(constr_pkey(name_skS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,axiom,
! [VAR_0X40SID_577,VAR_AENC_NA_A_579,VAR_AENC_NB_578,VAR_SIGN_A_PKA_580X30] :
( ( pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_580X30))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS))))
& pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_579))
& pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_579,name_skB)))
& pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578))
& pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB)) )
=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,conjecture,
pred_attacker(name_objective),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
~ pred_attacker(name_objective),
inference(negated_conjecture,[status(cth)],[f188]) ).
fof(f293,plain,
! [X0,X1] : pred_eq_bitstring_bitstring(X0,X1),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f311,plain,
! [VAR_V_69] :
( pred_attacker(VAR_V_69)
| ~ pred_attacker(tuple_out_3(VAR_V_69)) ),
inference(pre_NNF_transformation,[status(thm)],[f114]) ).
fof(f312,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_out_3(X0)) ),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f319,plain,
! [VAR_V_81] :
( pred_attacker(VAR_V_81)
| ~ pred_attacker(tuple_out_1(VAR_V_81)) ),
inference(pre_NNF_transformation,[status(thm)],[f118]) ).
fof(f320,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f350,plain,
! [VAR_V_136] :
( pred_attacker(VAR_V_136)
| ~ pred_attacker(tuple_client_B_out_6(VAR_V_136)) ),
inference(pre_NNF_transformation,[status(thm)],[f132]) ).
fof(f351,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_B_out_6(X0)) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f364,plain,
! [VAR_V_161] :
( pred_attacker(tuple_client_B_in_5(VAR_V_161))
| ~ pred_attacker(VAR_V_161) ),
inference(pre_NNF_transformation,[status(thm)],[f138]) ).
fof(f365,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_5(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f368,plain,
! [VAR_V_167] :
( pred_attacker(tuple_client_B_in_3(VAR_V_167))
| ~ pred_attacker(VAR_V_167) ),
inference(pre_NNF_transformation,[status(thm)],[f140]) ).
fof(f369,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f372,plain,
! [VAR_V_173] :
( pred_attacker(tuple_client_B_in_2(VAR_V_173))
| ~ pred_attacker(VAR_V_173) ),
inference(pre_NNF_transformation,[status(thm)],[f142]) ).
fof(f373,plain,
! [X0] :
( pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f430,plain,
! [X0] : pred_attacker(name_new0x2Dname(X0)),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f433,plain,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f435,plain,
pred_attacker(tuple_out_3(constr_pkey(name_skS))),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f447,plain,
! [VAR_0X40SID_577,VAR_AENC_NA_A_579,VAR_AENC_NB_578,VAR_SIGN_A_PKA_580X30] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_580X30))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_579))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_579,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578))
| ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB)) ),
inference(pre_NNF_transformation,[status(thm)],[f185]) ).
fof(f448,plain,
( pred_attacker(tuple_client_B_out_6(name_objective))
| ! [VAR_SIGN_A_PKA_580X30] :
( ~ pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_580X30))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS))))
| ! [VAR_AENC_NA_A_579] :
( ~ pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_579))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_579,name_skB)))
| ! [VAR_AENC_NB_578] :
( ~ pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578))
| ! [VAR_0X40SID_577] : ~ pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB)) ) ) ) ),
inference(miniscoping,[status(thm)],[f447]) ).
fof(f449,plain,
! [X0,X1,X2,X3] :
( pred_attacker(tuple_client_B_out_6(name_objective))
| ~ pred_attacker(tuple_client_B_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS))))
| ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X2,name_skB)))
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f455,plain,
~ pred_attacker(name_objective),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f456,definition,
! [X0,X1] :
( sQ0_spl
<=> ( ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f457,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X1))
| ~ pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
! [X2] :
( sQ1_spl
<=> ( ~ pred_attacker(tuple_client_B_in_3(X2))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X2,name_skB))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f460,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
! [X3] :
( sQ2_spl
<=> ( ~ pred_attacker(tuple_client_B_in_2(X3))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS)))) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(tuple_client_B_in_2(X0))
| ~ pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,definition,
( sQ3_spl
<=> pred_attacker(tuple_client_B_out_6(name_objective)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ3_spl
| pred_attacker(tuple_client_B_out_6(name_objective)) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,plain,
( sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f449,f456,f459,f462,f465]) ).
fof(f541,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(tuple_client_B_in_2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f293]) ).
fof(f577,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f430,f590]) ).
fof(f590,plain,
! [X0] :
( ~ sQ2_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f373,f541]) ).
fof(f591,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f577]) ).
fof(f592,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(tuple_client_B_in_3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f293]) ).
fof(f633,plain,
pred_attacker(constr_pkey(name_skA)),
inference(resolution,[status(thm)],[f320,f433]) ).
fof(f637,plain,
pred_attacker(constr_pkey(name_skS)),
inference(resolution,[status(thm)],[f312,f435]) ).
fof(f639,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f637,f660]) ).
fof(f660,plain,
! [X0] :
( ~ sQ1_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f369,f592]) ).
fof(f661,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f639]) ).
fof(f662,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(tuple_client_B_in_5(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f293]) ).
fof(f669,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f633,f685]) ).
fof(f685,plain,
! [X0] :
( ~ sQ0_spl
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f365,f662]) ).
fof(f686,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f669]) ).
fof(f740,plain,
( ~ sQ3_spl
| pred_attacker(name_objective) ),
inference(resolution,[status(thm)],[f351,f466]) ).
fof(f742,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f740,f455]) ).
fof(f743,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f742]) ).
fof(f744,plain,
$false,
inference(sat_refutation,[status(thm)],[f468,f591,f661,f686,f743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW965+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:21:32 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.43 % Elapsed time: 0.066599 seconds
% 0.14/0.43 % CPU time: 0.229381 seconds
% 0.14/0.43 % Total memory used: 106.304 MB
% 0.14/0.43 % Net memory used: 106.095 MB
%------------------------------------------------------------------------------