%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW957+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:09:50 PM UTC 2026
% Result : Theorem 0.13s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW957+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.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:20:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.50 % Refutation found
% 0.13/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.50 fof(f46,axiom,(
% 0.13/0.50 (! [VAR_X_14,VAR_Y_15] : constr_split(constr_concat(VAR_X_14,VAR_Y_15)) = tuple_2(VAR_X_14,VAR_Y_15) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f47,axiom,(
% 0.13/0.50 (! [VAR_X1_0X30,VAR_X2_0X30,VAR_Y1_0X30,VAR_Y2_0X30] : constr_xor(constr_concat(VAR_X1_0X30,VAR_Y1_0X30),constr_concat(VAR_X2_0X30,VAR_Y2_0X30)) = constr_concat(constr_xor(VAR_X1_0X30,VAR_X2_0X30),constr_xor(VAR_Y1_0X30,VAR_Y2_0X30)) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f48,axiom,(
% 0.13/0.50 (! [VAR_X_12,VAR_Y_13] : constr_C(constr_xor(VAR_X_12,VAR_Y_13)) = constr_xor(constr_C(VAR_X_12),constr_C(VAR_Y_13)) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f49,axiom,(
% 0.13/0.50 (! [VAR_X_11] : constr_xor(VAR_X_11,VAR_X_11) = constr_ZERO )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f50,axiom,(
% 0.13/0.50 (! [VAR_X_10X30] : constr_xor(VAR_X_10X30,constr_ZERO) = VAR_X_10X30 )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f51,axiom,(
% 0.13/0.50 (! [VAR_X_8,VAR_Y_9] : constr_xor(VAR_X_8,VAR_Y_9) = constr_xor(VAR_Y_9,VAR_X_8) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f52,axiom,(
% 0.13/0.50 (! [VAR_X_0X30,VAR_Y_0X30,VAR_Z_0X30] : constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f53,axiom,(
% 0.13/0.50 (! [VAR_V_31,VAR_V_32] :( ( pred_attacker(VAR_V_31)& pred_attacker(VAR_V_32) )=> pred_attacker(constr_xor(VAR_V_31,VAR_V_32)) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f55,axiom,(
% 0.13/0.50 (! [VAR_V_34] :( pred_attacker(VAR_V_34)=> pred_attacker(constr_split(VAR_V_34)) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f59,axiom,(
% 0.13/0.50 (! [VAR_V_49,VAR_V_50X30] :( pred_attacker(tuple_enc_oracle_out_2(VAR_V_49,VAR_V_50X30))=> pred_attacker(VAR_V_50X30) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f60,axiom,(
% 0.13/0.50 (! [VAR_V_53] :( pred_attacker(VAR_V_53)=> pred_attacker(tuple_enc_oracle_in_1(VAR_V_53)) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f63,axiom,(
% 0.13/0.50 pred_attacker(constr_ZERO) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f73,axiom,(
% 0.13/0.50 (! [VAR_V_81,VAR_V_82] :( pred_attacker(tuple_B_out_1(VAR_V_81,VAR_V_82))=> pred_attacker(VAR_V_82) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f75,axiom,(
% 0.13/0.50 (! [VAR_V_98,VAR_V_99] :( pred_attacker(tuple_2(VAR_V_98,VAR_V_99))=> pred_attacker(VAR_V_98) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f82,axiom,(
% 0.13/0.50 (! [VAR_M_150X30] :( pred_attacker(tuple_enc_oracle_in_1(VAR_M_150X30))=> pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_concat(VAR_M_150X30,constr_C(VAR_M_150X30)),constr_RC4(name_v,name_Kab)))) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f83,axiom,(
% 0.13/0.50 pred_attacker(tuple_B_out_1(name_v,constr_xor(constr_concat(name_objective,constr_C(name_objective)),constr_RC4(name_v,name_Kab)))) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f84,conjecture,(
% 0.13/0.50 pred_attacker(name_objective) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f85,negated_conjecture,(
% 0.13/0.50 ~(pred_attacker(name_objective) )),
% 0.13/0.50 inference(negated_conjecture,[status(cth)],[f84])).
% 0.13/0.50 fof(f131,plain,(
% 0.13/0.50 ![X0,X1]: (constr_split(constr_concat(X0,X1))=tuple_2(X0,X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.50 fof(f132,plain,(
% 0.13/0.50 ![X0,X1,X2,X3]: (constr_xor(constr_concat(X0,X1),constr_concat(X2,X3))=constr_concat(constr_xor(X0,X2),constr_xor(X1,X3)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f47])).
% 0.13/0.50 fof(f133,plain,(
% 0.13/0.50 ![X0,X1]: (constr_C(constr_xor(X0,X1))=constr_xor(constr_C(X0),constr_C(X1)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f48])).
% 0.13/0.50 fof(f134,plain,(
% 0.13/0.50 ![X0]: (constr_xor(X0,X0)=constr_ZERO)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f49])).
% 0.13/0.50 fof(f135,plain,(
% 0.13/0.50 ![X0]: (constr_xor(X0,constr_ZERO)=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f50])).
% 0.13/0.50 fof(f136,plain,(
% 0.13/0.50 ![X0,X1]: (constr_xor(X0,X1)=constr_xor(X1,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/0.50 fof(f137,plain,(
% 0.13/0.50 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(constr_xor(X0,X1),X2))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f52])).
% 0.13/0.50 fof(f138,plain,(
% 0.13/0.50 ![VAR_V_31,VAR_V_32]: ((~pred_attacker(VAR_V_31)|~pred_attacker(VAR_V_32))|pred_attacker(constr_xor(VAR_V_31,VAR_V_32)))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.13/0.50 fof(f139,plain,(
% 0.13/0.50 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_xor(X0,X1)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f138])).
% 0.13/0.50 fof(f141,plain,(
% 0.13/0.50 ![VAR_V_34]: (~pred_attacker(VAR_V_34)|pred_attacker(constr_split(VAR_V_34)))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.13/0.50 fof(f142,plain,(
% 0.13/0.50 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_split(X0)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.50 fof(f149,plain,(
% 0.13/0.50 ![VAR_V_49,VAR_V_50X30]: (~pred_attacker(tuple_enc_oracle_out_2(VAR_V_49,VAR_V_50X30))|pred_attacker(VAR_V_50X30))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.13/0.50 fof(f150,plain,(
% 0.13/0.50 ![VAR_V_50X30]: ((![VAR_V_49]: ~pred_attacker(tuple_enc_oracle_out_2(VAR_V_49,VAR_V_50X30)))|pred_attacker(VAR_V_50X30))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f149])).
% 0.13/0.50 fof(f151,plain,(
% 0.13/0.50 ![X0,X1]: (~pred_attacker(tuple_enc_oracle_out_2(X0,X1))|pred_attacker(X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f150])).
% 0.13/0.50 fof(f152,plain,(
% 0.13/0.50 ![VAR_V_53]: (~pred_attacker(VAR_V_53)|pred_attacker(tuple_enc_oracle_in_1(VAR_V_53)))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.13/0.50 fof(f153,plain,(
% 0.13/0.50 ![X0]: (~pred_attacker(X0)|pred_attacker(tuple_enc_oracle_in_1(X0)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f152])).
% 0.13/0.50 fof(f158,plain,(
% 0.13/0.50 pred_attacker(constr_ZERO)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f63])).
% 0.13/0.50 fof(f173,plain,(
% 0.13/0.50 ![VAR_V_81,VAR_V_82]: (~pred_attacker(tuple_B_out_1(VAR_V_81,VAR_V_82))|pred_attacker(VAR_V_82))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.13/0.50 fof(f174,plain,(
% 0.13/0.50 ![VAR_V_82]: ((![VAR_V_81]: ~pred_attacker(tuple_B_out_1(VAR_V_81,VAR_V_82)))|pred_attacker(VAR_V_82))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f173])).
% 0.13/0.50 fof(f175,plain,(
% 0.13/0.50 ![X0,X1]: (~pred_attacker(tuple_B_out_1(X0,X1))|pred_attacker(X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f174])).
% 0.13/0.50 fof(f178,plain,(
% 0.13/0.50 ![VAR_V_98,VAR_V_99]: (~pred_attacker(tuple_2(VAR_V_98,VAR_V_99))|pred_attacker(VAR_V_98))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.13/0.50 fof(f179,plain,(
% 0.13/0.50 ![VAR_V_98]: ((![VAR_V_99]: ~pred_attacker(tuple_2(VAR_V_98,VAR_V_99)))|pred_attacker(VAR_V_98))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f178])).
% 0.13/0.50 fof(f180,plain,(
% 0.13/0.50 ![X0,X1]: (~pred_attacker(tuple_2(X0,X1))|pred_attacker(X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f179])).
% 0.13/0.50 fof(f192,plain,(
% 0.13/0.50 ![VAR_M_150X30]: (~pred_attacker(tuple_enc_oracle_in_1(VAR_M_150X30))|pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_concat(VAR_M_150X30,constr_C(VAR_M_150X30)),constr_RC4(name_v,name_Kab)))))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 0.13/0.50 fof(f193,plain,(
% 0.13/0.50 ![X0]: (~pred_attacker(tuple_enc_oracle_in_1(X0))|pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_concat(X0,constr_C(X0)),constr_RC4(name_v,name_Kab)))))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.50 fof(f194,plain,(
% 0.13/0.50 pred_attacker(tuple_B_out_1(name_v,constr_xor(constr_concat(name_objective,constr_C(name_objective)),constr_RC4(name_v,name_Kab))))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f83])).
% 0.13/0.50 fof(f195,plain,(
% 0.13/0.50 ~pred_attacker(name_objective)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.50 fof(f197,plain,(
% 0.13/0.50 ![X0,X1,X2,X3]: (constr_xor(constr_concat(X0,constr_C(X1)),constr_concat(X2,constr_C(X3)))=constr_concat(constr_xor(X0,X2),constr_C(constr_xor(X1,X3))))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f133,f132])).
% 0.13/0.50 fof(f199,plain,(
% 0.13/0.50 ![X0]: (constr_C(constr_xor(X0,X0))=constr_ZERO)),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f133,f134])).
% 0.13/0.51 fof(f203,plain,(
% 0.13/0.51 constr_C(constr_ZERO)=constr_ZERO),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f134,f199])).
% 0.13/0.51 fof(f210,plain,(
% 0.13/0.51 ![X0]: (X0=constr_xor(constr_ZERO,X0))),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f135,f136])).
% 0.13/0.51 fof(f234,plain,(
% 0.13/0.51 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=constr_xor(constr_ZERO,X1))),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f134,f137])).
% 0.13/0.51 fof(f252,plain,(
% 0.13/0.51 ![X0,X1]: (~pred_attacker(constr_concat(X0,X1))|pred_attacker(tuple_2(X0,X1)))),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f131,f142])).
% 0.13/0.51 fof(f278,plain,(
% 0.13/0.51 ![X0]: (~pred_attacker(tuple_enc_oracle_in_1(X0))|pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_RC4(name_v,name_Kab),constr_concat(X0,constr_C(X0))))))),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f136,f193])).
% 0.13/0.51 fof(f279,plain,(
% 0.13/0.51 ![X0]: (pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_RC4(name_v,name_Kab),constr_concat(X0,constr_C(X0)))))|~pred_attacker(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f278,f153])).
% 0.13/0.51 fof(f280,plain,(
% 0.13/0.51 pred_attacker(tuple_B_out_1(name_v,constr_xor(constr_RC4(name_v,name_Kab),constr_concat(name_objective,constr_C(name_objective)))))),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f136,f194])).
% 0.13/0.51 fof(f281,plain,(
% 0.13/0.51 pred_attacker(constr_xor(constr_RC4(name_v,name_Kab),constr_concat(name_objective,constr_C(name_objective))))),
% 0.13/0.51 inference(resolution,[status(thm)],[f280,f175])).
% 0.13/0.51 fof(f332,plain,(
% 0.13/0.51 ![X0,X1]: (constr_ZERO=constr_concat(constr_xor(X0,X0),constr_C(constr_xor(X1,X1))))),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f134,f197])).
% 0.13/0.51 fof(f344,plain,(
% 0.13/0.51 ![X0]: (constr_ZERO=constr_concat(constr_ZERO,constr_C(constr_xor(X0,X0))))),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f134,f332])).
% 0.13/0.51 fof(f345,plain,(
% 0.13/0.51 constr_ZERO=constr_concat(constr_ZERO,constr_C(constr_ZERO))),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f134,f344])).
% 0.13/0.51 fof(f346,plain,(
% 0.13/0.51 constr_ZERO=constr_concat(constr_ZERO,constr_ZERO)),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f203,f345])).
% 0.13/0.51 fof(f568,plain,(
% 0.13/0.51 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=X1)),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f210,f234])).
% 0.13/0.51 fof(f593,plain,(
% 0.13/0.51 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(constr_xor(X0,X1))|pred_attacker(X1))),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f568,f139])).
% 0.13/0.51 fof(f1604,plain,(
% 0.13/0.51 pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_RC4(name_v,name_Kab),constr_concat(constr_ZERO,constr_ZERO))))|~pred_attacker(constr_ZERO)),
% 0.13/0.51 inference(paramodulation,[status(thm)],[f203,f279])).
% 0.13/0.51 fof(f1605,plain,(
% 0.13/0.51 pred_attacker(tuple_enc_oracle_out_2(name_v,constr_xor(constr_RC4(name_v,name_Kab),constr_ZERO)))|~pred_attacker(constr_ZERO)),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f346,f1604])).
% 0.13/0.51 fof(f1606,plain,(
% 0.13/0.51 pred_attacker(tuple_enc_oracle_out_2(name_v,constr_RC4(name_v,name_Kab)))|~pred_attacker(constr_ZERO)),
% 0.13/0.51 inference(forward_demodulation,[status(thm)],[f135,f1605])).
% 0.13/0.51 fof(f1607,plain,(
% 0.13/0.51 pred_attacker(tuple_enc_oracle_out_2(name_v,constr_RC4(name_v,name_Kab)))),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1606,f158])).
% 0.13/0.51 fof(f1608,plain,(
% 0.13/0.51 pred_attacker(constr_RC4(name_v,name_Kab))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1607,f151])).
% 0.13/0.51 fof(f1613,plain,(
% 0.13/0.51 ~pred_attacker(constr_RC4(name_v,name_Kab))|pred_attacker(constr_concat(name_objective,constr_C(name_objective)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f281,f593])).
% 0.13/0.51 fof(f1615,plain,(
% 0.13/0.51 pred_attacker(constr_concat(name_objective,constr_C(name_objective)))),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1613,f1608])).
% 0.13/0.51 fof(f1688,plain,(
% 0.13/0.51 pred_attacker(tuple_2(name_objective,constr_C(name_objective)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1615,f252])).
% 0.13/0.51 fof(f1691,plain,(
% 0.13/0.51 pred_attacker(name_objective)),
% 0.13/0.51 inference(resolution,[status(thm)],[f1688,f180])).
% 0.13/0.51 fof(f1693,plain,(
% 0.13/0.51 $false),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1691,f195])).
% 0.13/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.70/0.52 % Elapsed time: 0.143630 seconds
% 0.70/0.52 % CPU time: 0.850445 seconds
% 0.70/0.52 % Total memory used: 78.710 MB
% 0.70/0.52 % Net memory used: 77.883 MB
%------------------------------------------------------------------------------