%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW958+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 : n009.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:35 PM UTC 2026
% Result : Theorem 185.78s 23.94s
% Output : CNFRefutation 185.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 22
% Syntax : Number of formulae : 93 ( 26 unt; 0 def)
% Number of atoms : 222 ( 16 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 253 ( 124 ~; 108 |; 7 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-2 aty)
% Number of variables : 157 ( 157 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f191,axiom,
! [VAR_K_0X30,VAR_M_0X30] : constr_adec(constr_aenc(VAR_M_0X30,constr_pkey(VAR_K_0X30)),VAR_K_0X30) = VAR_M_0X30,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f192,axiom,
! [VAR_X_10X30] : constr_add(VAR_X_10X30,constr_neg(VAR_X_10X30)) = constr_ZERO,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,axiom,
! [VAR_X_9] : constr_add(VAR_X_9,constr_ZERO) = VAR_X_9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f194,axiom,
! [VAR_X_7,VAR_Y_8] : constr_add(VAR_X_7,VAR_Y_8) = constr_add(VAR_Y_8,VAR_X_7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f195,axiom,
! [VAR_X_0X30,VAR_Y_0X30,VAR_Z_0X30] : constr_add(VAR_X_0X30,constr_add(VAR_Y_0X30,VAR_Z_0X30)) = constr_add(constr_add(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f197,axiom,
! [VAR_V_30X30] :
( pred_attacker(VAR_V_30X30)
=> pred_attacker(constr_pkey(VAR_V_30X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f205,axiom,
! [VAR_V_53] :
( pred_attacker(tuple_out_1(VAR_V_53))
=> pred_attacker(VAR_V_53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f206,axiom,
! [VAR_V_57] :
( pred_attacker(VAR_V_57)
=> pred_attacker(constr_neg(VAR_V_57)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f239,axiom,
! [VAR_V_194] :
( pred_attacker(tuple_client_A_out_5(VAR_V_194))
=> pred_attacker(VAR_V_194) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f242,axiom,
! [VAR_V_20X309,VAR_V_210X30] :
( pred_attacker(tuple_client_A_out_3(VAR_V_20X309,VAR_V_210X30))
=> pred_attacker(VAR_V_210X30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f243,axiom,
! [VAR_V_214,VAR_V_215] :
( ( pred_attacker(VAR_V_215)
& pred_attacker(VAR_V_214) )
=> pred_attacker(tuple_client_A_in_4(VAR_V_214,VAR_V_215)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f246,axiom,
! [VAR_V_229] :
( pred_attacker(VAR_V_229)
=> pred_attacker(tuple_client_A_in_2(VAR_V_229)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f247,axiom,
! [VAR_V_232] :
( pred_attacker(tuple_client_A_in_2(VAR_V_232))
=> pred_attacker(VAR_V_232) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f248,axiom,
! [VAR_V_235] :
( pred_attacker(VAR_V_235)
=> pred_attacker(tuple_client_A_in_1(VAR_V_235)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f250,axiom,
! [VAR_V_242,VAR_V_243] :
( ( pred_attacker(VAR_V_243)
& pred_attacker(VAR_V_242) )
=> pred_attacker(constr_aenc(VAR_V_242,VAR_V_243)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f251,axiom,
! [VAR_V_246,VAR_V_247] :
( ( pred_attacker(VAR_V_247)
& pred_attacker(VAR_V_246) )
=> pred_attacker(constr_adec(VAR_V_246,VAR_V_247)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f252,axiom,
! [VAR_V_250X30,VAR_V_251] :
( ( pred_attacker(VAR_V_251)
& pred_attacker(VAR_V_250X30) )
=> pred_attacker(constr_add(VAR_V_250X30,VAR_V_251)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f268,axiom,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f271,axiom,
pred_attacker(tuple_out_4(constr_pkey(name_skD))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f272,axiom,
! [VAR_LASTT_336,VAR_PKNEXTT_337] :
( ( pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_337))
& pred_attacker(tuple_client_A_in_2(VAR_LASTT_336)) )
=> pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),VAR_PKNEXTT_337))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f273,axiom,
! [VAR_AENC_ADD_NA_SA_SB_SC_SD_377,VAR_LASTT_376,VAR_PKNEXTT_378] :
( ( pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_378))
& pred_attacker(tuple_client_A_in_2(VAR_LASTT_376))
& pred_attacker(tuple_client_A_in_4(VAR_LASTT_376,VAR_AENC_ADD_NA_SA_SB_SC_SD_377)) )
=> pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_SD_377,name_skA),constr_neg(name_Na)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f277,conjecture,
pred_attacker(name_Sa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f278,negated_conjecture,
~ pred_attacker(name_Sa),
inference(negated_conjecture,[status(cth)],[f277]) ).
fof(f469,plain,
! [X0,X1] : constr_adec(constr_aenc(X0,constr_pkey(X1)),X1) = X0,
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f470,plain,
! [X0] : constr_add(X0,constr_neg(X0)) = constr_ZERO,
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f471,plain,
! [X0] : constr_add(X0,constr_ZERO) = X0,
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f472,plain,
! [X0,X1] : constr_add(X0,X1) = constr_add(X1,X0),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f473,plain,
! [X0,X1,X2] : constr_add(constr_add(X0,X1),X2) = constr_add(X0,constr_add(X1,X2)),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f475,plain,
! [VAR_V_30X30] :
( pred_attacker(constr_pkey(VAR_V_30X30))
| ~ pred_attacker(VAR_V_30X30) ),
inference(pre_NNF_transformation,[status(thm)],[f197]) ).
fof(f476,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(constr_pkey(X0)) ),
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f491,plain,
! [VAR_V_53] :
( pred_attacker(VAR_V_53)
| ~ pred_attacker(tuple_out_1(VAR_V_53)) ),
inference(pre_NNF_transformation,[status(thm)],[f205]) ).
fof(f492,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f493,plain,
! [VAR_V_57] :
( pred_attacker(constr_neg(VAR_V_57))
| ~ pred_attacker(VAR_V_57) ),
inference(pre_NNF_transformation,[status(thm)],[f206]) ).
fof(f494,plain,
! [X0] :
( pred_attacker(constr_neg(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f493]) ).
fof(f570,plain,
! [VAR_V_194] :
( pred_attacker(VAR_V_194)
| ~ pred_attacker(tuple_client_A_out_5(VAR_V_194)) ),
inference(pre_NNF_transformation,[status(thm)],[f239]) ).
fof(f571,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_out_5(X0)) ),
inference(cnf_transformation,[status(thm)],[f570]) ).
fof(f577,plain,
! [VAR_V_20X309,VAR_V_210X30] :
( pred_attacker(VAR_V_210X30)
| ~ pred_attacker(tuple_client_A_out_3(VAR_V_20X309,VAR_V_210X30)) ),
inference(pre_NNF_transformation,[status(thm)],[f242]) ).
fof(f578,plain,
! [VAR_V_210X30] :
( pred_attacker(VAR_V_210X30)
| ! [VAR_V_20X309] : ~ pred_attacker(tuple_client_A_out_3(VAR_V_20X309,VAR_V_210X30)) ),
inference(miniscoping,[status(thm)],[f577]) ).
fof(f579,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_out_3(X1,X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f578]) ).
fof(f580,plain,
! [VAR_V_214,VAR_V_215] :
( pred_attacker(tuple_client_A_in_4(VAR_V_214,VAR_V_215))
| ~ pred_attacker(VAR_V_215)
| ~ pred_attacker(VAR_V_214) ),
inference(pre_NNF_transformation,[status(thm)],[f243]) ).
fof(f581,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(tuple_client_A_in_4(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f580]) ).
fof(f588,plain,
! [VAR_V_229] :
( pred_attacker(tuple_client_A_in_2(VAR_V_229))
| ~ pred_attacker(VAR_V_229) ),
inference(pre_NNF_transformation,[status(thm)],[f246]) ).
fof(f589,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_2(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f588]) ).
fof(f590,plain,
! [VAR_V_232] :
( pred_attacker(VAR_V_232)
| ~ pred_attacker(tuple_client_A_in_2(VAR_V_232)) ),
inference(pre_NNF_transformation,[status(thm)],[f247]) ).
fof(f591,plain,
! [X0] :
( ~ pred_attacker(tuple_client_A_in_2(X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f590]) ).
fof(f592,plain,
! [VAR_V_235] :
( pred_attacker(tuple_client_A_in_1(VAR_V_235))
| ~ pred_attacker(VAR_V_235) ),
inference(pre_NNF_transformation,[status(thm)],[f248]) ).
fof(f593,plain,
! [X0] :
( pred_attacker(tuple_client_A_in_1(X0))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f592]) ).
fof(f596,plain,
! [VAR_V_242,VAR_V_243] :
( pred_attacker(constr_aenc(VAR_V_242,VAR_V_243))
| ~ pred_attacker(VAR_V_243)
| ~ pred_attacker(VAR_V_242) ),
inference(pre_NNF_transformation,[status(thm)],[f250]) ).
fof(f597,plain,
! [X0,X1] :
( pred_attacker(constr_aenc(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f596]) ).
fof(f598,plain,
! [VAR_V_246,VAR_V_247] :
( pred_attacker(constr_adec(VAR_V_246,VAR_V_247))
| ~ pred_attacker(VAR_V_247)
| ~ pred_attacker(VAR_V_246) ),
inference(pre_NNF_transformation,[status(thm)],[f251]) ).
fof(f599,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(X0)
| pred_attacker(constr_adec(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f598]) ).
fof(f600,plain,
! [VAR_V_250X30,VAR_V_251] :
( pred_attacker(constr_add(VAR_V_250X30,VAR_V_251))
| ~ pred_attacker(VAR_V_251)
| ~ pred_attacker(VAR_V_250X30) ),
inference(pre_NNF_transformation,[status(thm)],[f252]) ).
fof(f601,plain,
! [X0,X1] :
( pred_attacker(constr_add(X1,X0))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f600]) ).
fof(f620,plain,
pred_attacker(tuple_out_1(constr_pkey(name_skA))),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f623,plain,
pred_attacker(tuple_out_4(constr_pkey(name_skD))),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f624,plain,
! [VAR_LASTT_336,VAR_PKNEXTT_337] :
( pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),VAR_PKNEXTT_337)))
| ~ pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_337))
| ~ pred_attacker(tuple_client_A_in_2(VAR_LASTT_336)) ),
inference(pre_NNF_transformation,[status(thm)],[f272]) ).
fof(f625,plain,
! [VAR_PKNEXTT_337] :
( pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),VAR_PKNEXTT_337)))
| ~ pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_337))
| ! [VAR_LASTT_336] : ~ pred_attacker(tuple_client_A_in_2(VAR_LASTT_336)) ),
inference(miniscoping,[status(thm)],[f624]) ).
fof(f626,plain,
! [X0,X1] :
( pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),X0)))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f625]) ).
fof(f627,plain,
! [VAR_AENC_ADD_NA_SA_SB_SC_SD_377,VAR_LASTT_376,VAR_PKNEXTT_378] :
( pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_SD_377,name_skA),constr_neg(name_Na))))
| ~ pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_378))
| ~ pred_attacker(tuple_client_A_in_2(VAR_LASTT_376))
| ~ pred_attacker(tuple_client_A_in_4(VAR_LASTT_376,VAR_AENC_ADD_NA_SA_SB_SC_SD_377)) ),
inference(pre_NNF_transformation,[status(thm)],[f273]) ).
fof(f628,plain,
! [VAR_AENC_ADD_NA_SA_SB_SC_SD_377] :
( pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_SD_377,name_skA),constr_neg(name_Na))))
| ! [VAR_PKNEXTT_378] : ~ pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_378))
| ! [VAR_LASTT_376] :
( ~ pred_attacker(tuple_client_A_in_2(VAR_LASTT_376))
| ~ pred_attacker(tuple_client_A_in_4(VAR_LASTT_376,VAR_AENC_ADD_NA_SA_SB_SC_SD_377)) ) ),
inference(miniscoping,[status(thm)],[f627]) ).
fof(f629,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_1(X2))
| ~ pred_attacker(tuple_client_A_in_4(X0,X1))
| pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(X1,name_skA),constr_neg(name_Na))))
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(cnf_transformation,[status(thm)],[f628]) ).
fof(f639,plain,
~ pred_attacker(name_Sa),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f660,plain,
! [X0] : constr_add(constr_ZERO,X0) = X0,
inference(paramodulation,[status(thm)],[f471,f472]) ).
fof(f672,plain,
! [X0] : constr_ZERO = constr_add(constr_neg(X0),X0),
inference(paramodulation,[status(thm)],[f472,f470]) ).
fof(f692,plain,
pred_attacker(constr_pkey(name_skA)),
inference(resolution,[status(thm)],[f492,f620]) ).
fof(f706,plain,
! [X0,X1] :
( pred_attacker(constr_aenc(constr_add(name_Na,name_Sa),X1))
| ~ pred_attacker(tuple_client_A_in_1(X1))
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(resolution,[status(thm)],[f579,f626]) ).
fof(f709,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| pred_attacker(X0)
| ~ pred_attacker(constr_aenc(X0,constr_pkey(X1))) ),
inference(paramodulation,[status(thm)],[f469,f599]) ).
fof(f723,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_2(X0))
| pred_attacker(constr_add(constr_adec(X1,name_skA),constr_neg(name_Na)))
| ~ pred_attacker(tuple_client_A_in_1(X2))
| ~ pred_attacker(tuple_client_A_in_4(X0,X1)) ),
inference(resolution,[status(thm)],[f629,f571]) ).
fof(f738,plain,
! [X0,X1] : constr_add(constr_ZERO,X0) = constr_add(constr_neg(X1),constr_add(X1,X0)),
inference(paramodulation,[status(thm)],[f672,f473]) ).
fof(f754,plain,
! [X0,X1] : constr_add(constr_add(X0,X1),constr_neg(X1)) = constr_add(X0,constr_ZERO),
inference(paramodulation,[status(thm)],[f470,f473]) ).
fof(f766,plain,
! [X0,X1] : constr_add(constr_neg(X0),constr_add(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f660,f738]) ).
fof(f767,plain,
! [X0,X1] : X0 = constr_add(constr_add(X0,X1),constr_neg(X1)),
inference(forward_demodulation,[status(thm)],[f471,f754]) ).
fof(f832,plain,
! [X0,X1] :
( ~ pred_attacker(constr_add(X0,X1))
| pred_attacker(X1)
| ~ pred_attacker(constr_neg(X0)) ),
inference(paramodulation,[status(thm)],[f766,f601]) ).
fof(f870,plain,
! [X0,X1] :
( ~ pred_attacker(constr_add(X1,X0))
| pred_attacker(X1)
| ~ pred_attacker(constr_neg(X0)) ),
inference(paramodulation,[status(thm)],[f767,f601]) ).
fof(f1072,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(X0)
| pred_attacker(constr_add(name_Na,name_Sa))
| ~ pred_attacker(tuple_client_A_in_1(constr_pkey(X0))) ),
inference(resolution,[status(thm)],[f709,f706]) ).
fof(f1080,plain,
! [X0,X1,X2] :
( pred_attacker(constr_add(constr_neg(name_Na),constr_adec(X2,name_skA)))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_4(X1,X2))
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(paramodulation,[status(thm)],[f472,f723]) ).
fof(f9319,plain,
! [X0,X1] :
( pred_attacker(name_Sa)
| ~ pred_attacker(constr_neg(name_Na))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(X0)
| ~ pred_attacker(tuple_client_A_in_1(constr_pkey(X0))) ),
inference(resolution,[status(thm)],[f1072,f832]) ).
fof(f9320,plain,
! [X0,X1] :
( ~ pred_attacker(constr_neg(name_Na))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_1(constr_pkey(X0)))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9319,f639]) ).
fof(f9321,plain,
! [X0,X1] :
( ~ pred_attacker(constr_pkey(X0))
| ~ pred_attacker(constr_neg(name_Na))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f9320,f593]) ).
fof(f9322,plain,
! [X0,X1] :
( ~ pred_attacker(constr_neg(name_Na))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9321,f476]) ).
fof(f9454,plain,
! [X0,X1,X2] :
( pred_attacker(constr_neg(name_Na))
| ~ pred_attacker(constr_neg(constr_adec(X2,name_skA)))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_4(X1,X2))
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(resolution,[status(thm)],[f1080,f870]) ).
fof(f9457,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_4(X1,X2))
| ~ pred_attacker(constr_neg(constr_adec(X2,name_skA)))
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9454,f9322]) ).
fof(f9459,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_1(X2))
| ~ pred_attacker(tuple_client_A_in_4(X1,X0))
| ~ pred_attacker(constr_adec(X0,name_skA)) ),
inference(resolution,[status(thm)],[f9457,f494]) ).
fof(f9461,plain,
! [X0,X1,X2] :
( ~ pred_attacker(X0)
| ~ pred_attacker(X2)
| ~ pred_attacker(tuple_client_A_in_2(X2))
| ~ pred_attacker(tuple_client_A_in_1(X1))
| ~ pred_attacker(constr_adec(X0,name_skA)) ),
inference(resolution,[status(thm)],[f9459,f581]) ).
fof(f9462,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_1(X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(constr_adec(X1,name_skA))
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9461,f591]) ).
fof(f9464,plain,
! [X0,X1,X2] :
( ~ pred_attacker(tuple_client_A_in_2(X2))
| ~ pred_attacker(constr_aenc(X1,constr_pkey(name_skA)))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(paramodulation,[status(thm)],[f469,f9462]) ).
fof(f9734,plain,
! [X0,X1,X2] :
( ~ pred_attacker(constr_pkey(name_skA))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_A_in_2(X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(resolution,[status(thm)],[f9464,f597]) ).
fof(f9735,plain,
! [X0,X1,X2] :
( ~ pred_attacker(constr_pkey(name_skA))
| ~ pred_attacker(tuple_client_A_in_2(X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f9734]) ).
fof(f9736,plain,
! [X0,X1,X2] :
( ~ pred_attacker(X2)
| ~ pred_attacker(tuple_client_A_in_2(X1))
| ~ pred_attacker(tuple_client_A_in_1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9735,f692]) ).
fof(f10532,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_client_A_in_1(X1))
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f626,f9736]) ).
fof(f10534,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| ~ pred_attacker(tuple_client_A_in_2(X0)) ),
inference(resolution,[status(thm)],[f10532,f593]) ).
fof(f10535,plain,
! [X0] : ~ pred_attacker(X0),
inference(backward_subsumption_resolution,[status(thm)],[f589,f10534]) ).
fof(f10538,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f623,f10535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW958+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 10:20:27 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 185.78/23.94 % Refutation found
% 185.78/23.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 185.78/23.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.73/24.03 % Elapsed time: 23.581931 seconds
% 11.73/24.03 % CPU time: 186.415224 seconds
% 11.73/24.03 % Total memory used: 496.595 MB
% 11.73/24.03 % Net memory used: 466.381 MB
%------------------------------------------------------------------------------