%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW965+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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 : Fri Sep 25 03:27:51 PM UTC 2026
% Result : Theorem 160.18s 21.56s
% Output : Proof 160.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW965+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 23:19:06 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 160.18/21.56 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 160.18/21.56 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 160.18/21.56 fof(f131, axiom, ! [VAR_V_136] : ( pred_attacker(tuple_client_B_out_6(VAR_V_136)) => pred_attacker(VAR_V_136) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax131)).
% 160.18/21.56 fof(f131_nnf, plain, ! [VAR_V_136] : ((~(pred_attacker(tuple_client_B_out_6(VAR_V_136))) | pred_attacker(VAR_V_136))), inference(nnf_transformation, [status(thm)], [f131])).
% 160.18/21.56 fof(f131_sk, plain, ! [VAR_V_136] : ((~(pred_attacker(tuple_client_B_out_6(VAR_V_136))) | pred_attacker(VAR_V_136))), inference(skolemisation, [status(esa)], [f131_nnf])).
% 160.18/21.56 cnf(c131, plain, ~pred_attacker(tuple_client_B_out_6(X0)) | pred_attacker(X0), inference(cnf_transformation, [status(esa)], [f131_sk])).
% 160.18/21.56 fof(sdef3, definition, (spl3 <=> (pred_attacker(tuple_client_B_out_6(name_objective)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 160.18/21.56 cnf(p188, plain, (pred_attacker(tuple_client_B_out_6(name_objective)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 160.18/21.56 cnf(p2231, plain, (pred_attacker(name_objective) | ~spl3), inference(resolution, [status(thm)], [c131, p188])).
% 160.18/21.56 fof(f187, conjecture, pred_attacker(name_objective), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co0)).
% 160.18/21.56 fof(f187_neg, negated_conjecture, ~(pred_attacker(name_objective)), inference(negated_conjecture, [status(cth)], [f187])).
% 160.18/21.56 fof(f187_nnf, plain, ~(pred_attacker(name_objective)), inference(nnf_transformation, [status(thm)], [f187_neg])).
% 160.18/21.56 fof(f187_sk, plain, ~(pred_attacker(name_objective)), inference(skolemisation, [status(esa)], [f187_nnf])).
% 160.18/21.56 cnf(c187, plain, ~pred_attacker(name_objective), inference(cnf_transformation, [status(esa)], [f187_sk])).
% 160.18/21.56 cnf(p2232, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p2231, c187])).
% 160.18/21.56 cnf(sct0, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p2232])).
% 160.18/21.56 fof(sdef0, definition, (spl0 <=> (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) | ~pred_attacker(tuple_client_B_in_5(X1)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 160.18/21.56 cnf(p185, plain, (~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X1,name_skB)) | ~pred_attacker(tuple_client_B_in_5(X1)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 160.18/21.56 fof(f103, axiom, ! [VAR_X_41,VAR_Y_42] : pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax103)).
% 160.18/21.56 fof(f103_nnf, plain, ! [VAR_X_41,VAR_Y_42] : (pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42)), inference(nnf_transformation, [status(thm)], [f103])).
% 160.18/21.56 fof(f103_sk, plain, ! [VAR_X_41,VAR_Y_42] : (pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42)), inference(skolemisation, [status(esa)], [f103_nnf])).
% 160.18/21.56 cnf(c103, plain, pred_eq_bitstring_bitstring(X0,X1), inference(cnf_transformation, [status(esa)], [f103_sk])).
% 160.18/21.56 cnf(p8336, plain, (~pred_attacker(tuple_client_B_in_5(X0)) | ~spl0), inference(resolution, [status(thm)], [p185, c103])).
% 160.18/21.56 fof(f137, axiom, ! [VAR_V_161] : ( pred_attacker(VAR_V_161) => pred_attacker(tuple_client_B_in_5(VAR_V_161)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax137)).
% 160.18/21.56 fof(f137_nnf, plain, ! [VAR_V_161] : ((~(pred_attacker(VAR_V_161)) | pred_attacker(tuple_client_B_in_5(VAR_V_161)))), inference(nnf_transformation, [status(thm)], [f137])).
% 160.18/21.56 fof(f137_sk, plain, ! [VAR_V_161] : ((~(pred_attacker(VAR_V_161)) | pred_attacker(tuple_client_B_in_5(VAR_V_161)))), inference(skolemisation, [status(esa)], [f137_nnf])).
% 160.18/21.56 cnf(c137, plain, ~pred_attacker(X0) | pred_attacker(tuple_client_B_in_5(X0)), inference(cnf_transformation, [status(esa)], [f137_sk])).
% 160.18/21.56 fof(f109, axiom, pred_attacker(tuple_true), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax109)).
% 160.18/21.56 fof(f109_nnf, plain, pred_attacker(tuple_true), inference(nnf_transformation, [status(thm)], [f109])).
% 160.18/21.56 cnf(c109, plain, pred_attacker(tuple_true), inference(cnf_transformation, [status(esa)], [f109_nnf])).
% 160.18/21.56 cnf(p2907, plain, pred_attacker(tuple_client_B_in_5(tuple_true)), inference(resolution, [status(thm)], [c137, c109])).
% 160.18/21.56 cnf(p8337, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p8336, p2907])).
% 160.18/21.56 cnf(sct1, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p8337])).
% 160.18/21.56 fof(sdef1, definition, (spl1 <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) | ~pred_attacker(tuple_client_B_in_3(X0)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 160.18/21.56 cnf(p186, plain, (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X0,name_skB))) | ~pred_attacker(tuple_client_B_in_3(X0)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 160.18/21.56 cnf(p8435, plain, (~pred_attacker(tuple_client_B_in_3(X0)) | ~spl1), inference(resolution, [status(thm)], [p186, c103])).
% 160.18/21.56 fof(f139, axiom, ! [VAR_V_167] : ( pred_attacker(VAR_V_167) => pred_attacker(tuple_client_B_in_3(VAR_V_167)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax139)).
% 160.18/21.56 fof(f139_nnf, plain, ! [VAR_V_167] : ((~(pred_attacker(VAR_V_167)) | pred_attacker(tuple_client_B_in_3(VAR_V_167)))), inference(nnf_transformation, [status(thm)], [f139])).
% 160.18/21.56 fof(f139_sk, plain, ! [VAR_V_167] : ((~(pred_attacker(VAR_V_167)) | pred_attacker(tuple_client_B_in_3(VAR_V_167)))), inference(skolemisation, [status(esa)], [f139_nnf])).
% 160.18/21.56 cnf(c139, plain, ~pred_attacker(X0) | pred_attacker(tuple_client_B_in_3(X0)), inference(cnf_transformation, [status(esa)], [f139_sk])).
% 160.18/21.56 cnf(p3208, plain, pred_attacker(tuple_client_B_in_3(tuple_true)), inference(resolution, [status(thm)], [c139, c109])).
% 160.18/21.56 cnf(p8436, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p8435, p3208])).
% 160.18/21.56 cnf(sct2, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p8436])).
% 160.18/21.56 fof(sdef2, definition, (spl2 <=> (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) | ~pred_attacker(tuple_client_B_in_2(X0)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 160.18/21.56 cnf(p187, plain, (~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X0,constr_pkey(name_skS)))) | ~pred_attacker(tuple_client_B_in_2(X0)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 160.18/21.56 cnf(p8533, plain, (~pred_attacker(tuple_client_B_in_2(X0)) | ~spl2), inference(resolution, [status(thm)], [p187, c103])).
% 160.18/21.56 fof(f141, axiom, ! [VAR_V_173] : ( pred_attacker(VAR_V_173) => pred_attacker(tuple_client_B_in_2(VAR_V_173)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax141)).
% 160.18/21.56 fof(f141_nnf, plain, ! [VAR_V_173] : ((~(pred_attacker(VAR_V_173)) | pred_attacker(tuple_client_B_in_2(VAR_V_173)))), inference(nnf_transformation, [status(thm)], [f141])).
% 160.18/21.56 fof(f141_sk, plain, ! [VAR_V_173] : ((~(pred_attacker(VAR_V_173)) | pred_attacker(tuple_client_B_in_2(VAR_V_173)))), inference(skolemisation, [status(esa)], [f141_nnf])).
% 160.18/21.56 cnf(c141, plain, ~pred_attacker(X0) | pred_attacker(tuple_client_B_in_2(X0)), inference(cnf_transformation, [status(esa)], [f141_sk])).
% 160.18/21.56 cnf(p3525, plain, pred_attacker(tuple_client_B_in_2(tuple_true)), inference(resolution, [status(thm)], [c141, c109])).
% 160.18/21.56 cnf(p8534, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p8533, p3525])).
% 160.18/21.56 cnf(sct3, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p8534])).
% 160.18/21.56 fof(f184, axiom, ! [VAR_0X40SID_577,VAR_AENC_NA_A_579,VAR_AENC_NB_578,VAR_SIGN_A_PKA_580X30] : ( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB)) & pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578)) & 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_3(VAR_AENC_NA_A_579)) & 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_2(VAR_SIGN_A_PKA_580X30)) ) => pred_attacker(tuple_client_B_out_6(name_objective)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax184)).
% 160.18/21.56 fof(f184_nnf, plain, ! [VAR_0X40SID_577,VAR_AENC_NA_A_579,VAR_AENC_NB_578,VAR_SIGN_A_PKA_580X30] : (((((((~(pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB))) | ~(pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578)))) | ~(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_3(VAR_AENC_NA_A_579)))) | ~(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_2(VAR_SIGN_A_PKA_580X30)))) | pred_attacker(tuple_client_B_out_6(name_objective)))), inference(nnf_transformation, [status(thm)], [f184])).
% 160.18/21.56 fof(f184_sk, plain, ! [VAR_0X40SID_577,VAR_AENC_NB_578,VAR_AENC_NA_A_579,VAR_SIGN_A_PKA_580X30] : (((((((~(pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB))) | ~(pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578)))) | ~(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_3(VAR_AENC_NA_A_579)))) | ~(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_2(VAR_SIGN_A_PKA_580X30)))) | pred_attacker(tuple_client_B_out_6(name_objective)))), inference(skolemisation, [status(esa)], [f184_nnf])).
% 160.18/21.56 cnf(c184, plain, ~pred_eq_bitstring_bitstring(name_Nb(X0),constr_adec(X2,name_skB)) | ~pred_attacker(tuple_client_B_in_5(X2)) | ~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(X1,name_skB))) | ~pred_attacker(tuple_client_B_in_3(X1)) | ~pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(X3,constr_pkey(name_skS)))) | ~pred_attacker(tuple_client_B_in_2(X3)) | pred_attacker(tuple_client_B_out_6(name_objective)), inference(cnf_transformation, [status(esa)], [f184_sk])).
% 160.18/21.56 cnf(ssp0, plain, (spl0 | spl1 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [c184, sdef0, sdef1, sdef2, sdef3])).
% 160.18/21.56 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, sct0, sct1, sct2, sct3])).
% 160.18/21.56 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------