%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW948+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:49 PM UTC 2026
% Result : Theorem 95.94s 12.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW948+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 10:20:19 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 95.94/12.83 % Refutation found
% 95.94/12.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 95.94/12.83 % SZS output start CNFRefutation for theBenchmark
% 95.94/12.83 fof(f67,axiom,(
% 95.94/12.83 (! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f68,axiom,(
% 95.94/12.83 (! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9 )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f69,axiom,(
% 95.94/12.83 (! [VAR_X_7,VAR_Y_8] : constr_xor(VAR_X_7,VAR_Y_8) = constr_xor(VAR_Y_8,VAR_X_7) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f70,axiom,(
% 95.94/12.83 (! [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) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f71,axiom,(
% 95.94/12.83 (! [VAR_V_30X30,VAR_V_31] :( ( pred_attacker(VAR_V_30X30)& pred_attacker(VAR_V_31) )=> pred_attacker(constr_xor(VAR_V_30X30,VAR_V_31)) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f76,axiom,(
% 95.94/12.83 (! [VAR_V_49,VAR_V_50X30] :( pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_49,VAR_V_50X30))=> pred_attacker(VAR_V_49) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f77,axiom,(
% 95.94/12.83 (! [VAR_V_52,VAR_V_53] :( pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_52,VAR_V_53))=> pred_attacker(VAR_V_53) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f79,axiom,(
% 95.94/12.83 (! [VAR_V_59] :( pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_59))=> pred_attacker(VAR_V_59) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f82,axiom,(
% 95.94/12.83 pred_attacker(constr_ZERO) ),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f84,axiom,(
% 95.94/12.83 (! [VAR_V_67] :( pred_attacker(tuple_R_out_4(VAR_V_67))=> pred_attacker(VAR_V_67) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f88,axiom,(
% 95.94/12.83 (! [VAR_V_79] :( pred_attacker(tuple_R_out_1(VAR_V_79))=> pred_attacker(VAR_V_79) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f89,axiom,(
% 95.94/12.83 (! [VAR_V_83,VAR_V_84] :( ( pred_attacker(VAR_V_83)& pred_attacker(VAR_V_84) )=> pred_attacker(tuple_R_in_2(VAR_V_83,VAR_V_84)) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f102,axiom,(
% 95.94/12.83 pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r0x30_from_1st)) ),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f103,axiom,(
% 95.94/12.83 pred_attacker(tuple_knowledge_from_1st_round_out_2(name_r1_from_1st,constr_h(constr_xor(constr_xor(name_r0x30_from_1st,name_r1_from_1st),name_k)))) ),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f105,axiom,(
% 95.94/12.83 pred_attacker(tuple_R_out_1(name_r0x30)) ),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f107,axiom,(
% 95.94/12.83 (! [VAR_R1_IN_244] :( pred_attacker(tuple_R_in_2(VAR_R1_IN_244,constr_h(constr_xor(constr_xor(name_r0x30,VAR_R1_IN_244),name_k))))=> pred_attacker(tuple_R_out_4(name_objective_R)) ) )),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f108,conjecture,(
% 95.94/12.83 pred_attacker(name_objective_R) ),
% 95.94/12.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.94/12.83 fof(f109,negated_conjecture,(
% 95.94/12.83 ~(pred_attacker(name_objective_R) )),
% 95.94/12.83 inference(negated_conjecture,[status(cth)],[f108])).
% 95.94/12.83 fof(f176,plain,(
% 95.94/12.83 ![X0]: (constr_xor(X0,X0)=constr_ZERO)),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f67])).
% 95.94/12.83 fof(f177,plain,(
% 95.94/12.83 ![X0]: (constr_xor(X0,constr_ZERO)=X0)),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f68])).
% 95.94/12.83 fof(f178,plain,(
% 95.94/12.83 ![X0,X1]: (constr_xor(X0,X1)=constr_xor(X1,X0))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f69])).
% 95.94/12.83 fof(f179,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(constr_xor(X0,X1),X2))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f70])).
% 95.94/12.83 fof(f180,plain,(
% 95.94/12.83 ![VAR_V_30X30,VAR_V_31]: ((~pred_attacker(VAR_V_30X30)|~pred_attacker(VAR_V_31))|pred_attacker(constr_xor(VAR_V_30X30,VAR_V_31)))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 95.94/12.83 fof(f181,plain,(
% 95.94/12.83 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(constr_xor(X0,X1)))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f180])).
% 95.94/12.83 fof(f189,plain,(
% 95.94/12.83 ![VAR_V_49,VAR_V_50X30]: (~pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_49,VAR_V_50X30))|pred_attacker(VAR_V_49))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 95.94/12.83 fof(f190,plain,(
% 95.94/12.83 ![VAR_V_49]: ((![VAR_V_50X30]: ~pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_49,VAR_V_50X30)))|pred_attacker(VAR_V_49))),
% 95.94/12.83 inference(miniscoping,[status(thm)],[f189])).
% 95.94/12.83 fof(f191,plain,(
% 95.94/12.83 ![X0,X1]: (~pred_attacker(tuple_knowledge_from_1st_round_out_2(X0,X1))|pred_attacker(X0))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f190])).
% 95.94/12.83 fof(f192,plain,(
% 95.94/12.83 ![VAR_V_52,VAR_V_53]: (~pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_52,VAR_V_53))|pred_attacker(VAR_V_53))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 95.94/12.83 fof(f193,plain,(
% 95.94/12.83 ![VAR_V_53]: ((![VAR_V_52]: ~pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_52,VAR_V_53)))|pred_attacker(VAR_V_53))),
% 95.94/12.83 inference(miniscoping,[status(thm)],[f192])).
% 95.94/12.83 fof(f194,plain,(
% 95.94/12.83 ![X0,X1]: (~pred_attacker(tuple_knowledge_from_1st_round_out_2(X0,X1))|pred_attacker(X1))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f193])).
% 95.94/12.83 fof(f197,plain,(
% 95.94/12.83 ![VAR_V_59]: (~pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_59))|pred_attacker(VAR_V_59))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 95.94/12.83 fof(f198,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_knowledge_from_1st_round_out_1(X0))|pred_attacker(X0))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f197])).
% 95.94/12.83 fof(f202,plain,(
% 95.94/12.83 pred_attacker(constr_ZERO)),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f82])).
% 95.94/12.83 fof(f205,plain,(
% 95.94/12.83 ![VAR_V_67]: (~pred_attacker(tuple_R_out_4(VAR_V_67))|pred_attacker(VAR_V_67))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 95.94/12.83 fof(f206,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_R_out_4(X0))|pred_attacker(X0))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f205])).
% 95.94/12.83 fof(f213,plain,(
% 95.94/12.83 ![VAR_V_79]: (~pred_attacker(tuple_R_out_1(VAR_V_79))|pred_attacker(VAR_V_79))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 95.94/12.83 fof(f214,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_R_out_1(X0))|pred_attacker(X0))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f213])).
% 95.94/12.83 fof(f215,plain,(
% 95.94/12.83 ![VAR_V_83,VAR_V_84]: ((~pred_attacker(VAR_V_83)|~pred_attacker(VAR_V_84))|pred_attacker(tuple_R_in_2(VAR_V_83,VAR_V_84)))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 95.94/12.83 fof(f216,plain,(
% 95.94/12.83 ![X0,X1]: (~pred_attacker(X0)|~pred_attacker(X1)|pred_attacker(tuple_R_in_2(X0,X1)))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f215])).
% 95.94/12.83 fof(f236,plain,(
% 95.94/12.83 pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r0x30_from_1st))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f102])).
% 95.94/12.83 fof(f237,plain,(
% 95.94/12.83 pred_attacker(tuple_knowledge_from_1st_round_out_2(name_r1_from_1st,constr_h(constr_xor(constr_xor(name_r0x30_from_1st,name_r1_from_1st),name_k))))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f103])).
% 95.94/12.83 fof(f239,plain,(
% 95.94/12.83 pred_attacker(tuple_R_out_1(name_r0x30))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f105])).
% 95.94/12.83 fof(f242,plain,(
% 95.94/12.83 ![VAR_R1_IN_244]: (~pred_attacker(tuple_R_in_2(VAR_R1_IN_244,constr_h(constr_xor(constr_xor(name_r0x30,VAR_R1_IN_244),name_k))))|pred_attacker(tuple_R_out_4(name_objective_R)))),
% 95.94/12.83 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 95.94/12.83 fof(f243,plain,(
% 95.94/12.83 (![VAR_R1_IN_244]: ~pred_attacker(tuple_R_in_2(VAR_R1_IN_244,constr_h(constr_xor(constr_xor(name_r0x30,VAR_R1_IN_244),name_k)))))|pred_attacker(tuple_R_out_4(name_objective_R))),
% 95.94/12.83 inference(miniscoping,[status(thm)],[f242])).
% 95.94/12.83 fof(f244,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(constr_xor(name_r0x30,X0),name_k))))|pred_attacker(tuple_R_out_4(name_objective_R)))),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f243])).
% 95.94/12.83 fof(f245,plain,(
% 95.94/12.83 ~pred_attacker(name_objective_R)),
% 95.94/12.83 inference(cnf_transformation,[status(thm)],[f109])).
% 95.94/12.83 fof(f246,definition,(
% 95.94/12.83 ![X0]: (sQ0_spl <=> (~pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(constr_xor(name_r0x30,X0),name_k))))))),
% 95.94/12.83 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 95.94/12.83 fof(f247,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(constr_xor(name_r0x30,X0),name_k))))|~sQ0_spl)),
% 95.94/12.83 inference(component_clause,[status(thm)],[f246])).
% 95.94/12.83 fof(f249,definition,(
% 95.94/12.83 sQ1_spl <=> (pred_attacker(tuple_R_out_4(name_objective_R)))),
% 95.94/12.83 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 95.94/12.83 fof(f250,plain,(
% 95.94/12.83 pred_attacker(tuple_R_out_4(name_objective_R))|~sQ1_spl),
% 95.94/12.83 inference(component_clause,[status(thm)],[f249])).
% 95.94/12.83 fof(f252,plain,(
% 95.94/12.83 sQ0_spl|sQ1_spl),
% 95.94/12.83 inference(split_clause,[status(thm)],[f244,f246,f249])).
% 95.94/12.83 fof(f255,plain,(
% 95.94/12.83 ![X0]: (X0=constr_xor(constr_ZERO,X0))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f177,f178])).
% 95.94/12.83 fof(f272,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(X2,constr_xor(X0,X1)))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f179])).
% 95.94/12.83 fof(f278,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(constr_xor(X1,X0),X2))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f179])).
% 95.94/12.83 fof(f280,plain,(
% 95.94/12.83 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=constr_xor(constr_ZERO,X1))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f176,f179])).
% 95.94/12.83 fof(f287,plain,(
% 95.94/12.83 ![X0,X1]: (constr_xor(X0,constr_xor(X0,X1))=X1)),
% 95.94/12.83 inference(forward_demodulation,[status(thm)],[f255,f280])).
% 95.94/12.83 fof(f325,plain,(
% 95.94/12.83 pred_attacker(name_r0x30_from_1st)),
% 95.94/12.83 inference(resolution,[status(thm)],[f198,f236])).
% 95.94/12.83 fof(f331,plain,(
% 95.94/12.83 pred_attacker(name_r0x30)),
% 95.94/12.83 inference(resolution,[status(thm)],[f214,f239])).
% 95.94/12.83 fof(f339,plain,(
% 95.94/12.83 ![X0,X1]: (constr_xor(X0,constr_xor(X1,X0))=X1)),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f287])).
% 95.94/12.83 fof(f402,plain,(
% 95.94/12.83 pred_attacker(tuple_knowledge_from_1st_round_out_2(name_r1_from_1st,constr_h(constr_xor(name_r0x30_from_1st,constr_xor(name_r1_from_1st,name_k)))))),
% 95.94/12.83 inference(forward_demodulation,[status(thm)],[f179,f237])).
% 95.94/12.83 fof(f403,plain,(
% 95.94/12.83 pred_attacker(constr_h(constr_xor(name_r0x30_from_1st,constr_xor(name_r1_from_1st,name_k))))),
% 95.94/12.83 inference(resolution,[status(thm)],[f402,f194])).
% 95.94/12.83 fof(f404,plain,(
% 95.94/12.83 pred_attacker(name_r1_from_1st)),
% 95.94/12.83 inference(resolution,[status(thm)],[f402,f191])).
% 95.94/12.83 fof(f435,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(constr_xor(X0,X1),X2)=constr_xor(X1,constr_xor(X2,X0)))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f272])).
% 95.94/12.83 fof(f464,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(X0,constr_xor(X1,X2))=constr_xor(X2,constr_xor(X1,X0)))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f272])).
% 95.94/12.83 fof(f476,plain,(
% 95.94/12.83 ![X0,X1,X2]: (~pred_attacker(X0)|~pred_attacker(constr_xor(X1,X2))|pred_attacker(constr_xor(X2,constr_xor(X0,X1))))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f272,f181])).
% 95.94/12.83 fof(f566,plain,(
% 95.94/12.83 ![X0,X1,X2]: (~pred_attacker(constr_xor(X0,X1))|~pred_attacker(X2)|pred_attacker(constr_xor(X1,constr_xor(X0,X2))))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f278,f181])).
% 95.94/12.83 fof(f745,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(X0,constr_xor(name_r0x30,name_k)))))|~sQ0_spl)),
% 95.94/12.83 inference(forward_demodulation,[status(thm)],[f278,f247])).
% 95.94/12.83 fof(f746,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_h(constr_xor(X0,constr_xor(name_r0x30,name_k))))|~sQ0_spl)),
% 95.94/12.83 inference(resolution,[status(thm)],[f745,f216])).
% 95.94/12.83 fof(f814,plain,(
% 95.94/12.83 pred_attacker(name_objective_R)|~sQ1_spl),
% 95.94/12.83 inference(resolution,[status(thm)],[f250,f206])).
% 95.94/12.83 fof(f815,plain,(
% 95.94/12.83 $false|~sQ1_spl),
% 95.94/12.83 inference(forward_subsumption_resolution,[status(thm)],[f814,f245])).
% 95.94/12.83 fof(f816,plain,(
% 95.94/12.83 ~sQ1_spl),
% 95.94/12.83 inference(contradiction_clause,[status(thm)],[f815])).
% 95.94/12.83 fof(f1206,plain,(
% 95.94/12.83 ![X0,X1,X2]: (constr_xor(constr_xor(X0,X1),X2)=constr_xor(X0,constr_xor(X2,X1)))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f178,f435])).
% 95.94/12.83 fof(f2057,plain,(
% 95.94/12.83 pred_attacker(constr_h(constr_xor(name_k,constr_xor(name_r1_from_1st,name_r0x30_from_1st))))),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f464,f403])).
% 95.94/12.83 fof(f2625,plain,(
% 95.94/12.83 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_h(constr_xor(name_k,constr_xor(name_r0x30,X0))))|~sQ0_spl)),
% 95.94/12.83 inference(paramodulation,[status(thm)],[f464,f746])).
% 95.94/12.89 fof(f11755,plain,(
% 95.94/12.89 ![X0,X1]: (~pred_attacker(constr_xor(X0,X1))|pred_attacker(constr_xor(X1,constr_xor(X0,name_r1_from_1st))))),
% 95.94/12.89 inference(resolution,[status(thm)],[f566,f404])).
% 95.94/12.89 fof(f11788,plain,(
% 95.94/12.89 ![X0,X1]: (~pred_attacker(constr_xor(X0,X1))|pred_attacker(constr_xor(X1,constr_xor(X0,constr_ZERO))))),
% 95.94/12.89 inference(resolution,[status(thm)],[f566,f202])).
% 95.94/12.89 fof(f11795,plain,(
% 95.94/12.89 ![X0,X1]: (~pred_attacker(constr_xor(X0,X1))|pred_attacker(constr_xor(X1,X0)))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f177,f11788])).
% 95.94/12.89 fof(f15055,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,constr_xor(constr_ZERO,name_r1_from_1st))))),
% 95.94/12.89 inference(paramodulation,[status(thm)],[f255,f11755])).
% 95.94/12.89 fof(f15098,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,name_r1_from_1st)))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f255,f15055])).
% 95.94/12.89 fof(f15206,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(name_r1_from_1st,X0)))),
% 95.94/12.89 inference(resolution,[status(thm)],[f15098,f11795])).
% 95.94/12.89 fof(f15261,plain,(
% 95.94/12.89 pred_attacker(constr_xor(name_r1_from_1st,name_r0x30))),
% 95.94/12.89 inference(resolution,[status(thm)],[f15206,f331])).
% 95.94/12.89 fof(f15278,plain,(
% 95.94/12.89 pred_attacker(constr_xor(name_r1_from_1st,name_r0x30_from_1st))),
% 95.94/12.89 inference(resolution,[status(thm)],[f15206,f325])).
% 95.94/12.89 fof(f15329,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(name_r0x30,constr_xor(X0,name_r1_from_1st))))),
% 95.94/12.89 inference(resolution,[status(thm)],[f15261,f476])).
% 95.94/12.89 fof(f23392,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(constr_xor(X0,name_r1_from_1st),constr_xor(name_r0x30,name_r1_from_1st))))),
% 95.94/12.89 inference(resolution,[status(thm)],[f15329,f11755])).
% 95.94/12.89 fof(f23430,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,constr_xor(constr_xor(name_r0x30,name_r1_from_1st),name_r1_from_1st))))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f1206,f23392])).
% 95.94/12.89 fof(f23431,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,constr_xor(name_r0x30,constr_xor(name_r1_from_1st,name_r1_from_1st)))))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f1206,f23430])).
% 95.94/12.89 fof(f23432,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,constr_xor(name_r0x30,constr_ZERO))))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f176,f23431])).
% 95.94/12.89 fof(f23433,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|pred_attacker(constr_xor(X0,name_r0x30)))),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f177,f23432])).
% 95.94/12.89 fof(f23504,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_h(constr_xor(name_k,constr_xor(name_r0x30,constr_xor(X0,name_r0x30)))))|~sQ0_spl)),
% 95.94/12.89 inference(resolution,[status(thm)],[f23433,f2625])).
% 95.94/12.89 fof(f23534,plain,(
% 95.94/12.89 ![X0]: (~pred_attacker(X0)|~pred_attacker(constr_h(constr_xor(name_k,X0)))|~sQ0_spl)),
% 95.94/12.89 inference(forward_demodulation,[status(thm)],[f339,f23504])).
% 95.94/12.89 fof(f24298,plain,(
% 95.94/12.89 ~pred_attacker(constr_xor(name_r1_from_1st,name_r0x30_from_1st))|~sQ0_spl),
% 95.94/12.89 inference(resolution,[status(thm)],[f23534,f2057])).
% 95.94/12.89 fof(f24338,plain,(
% 95.94/12.89 $false|~sQ0_spl),
% 95.94/12.89 inference(forward_subsumption_resolution,[status(thm)],[f24298,f15278])).
% 95.94/12.89 fof(f24339,plain,(
% 95.94/12.89 ~sQ0_spl),
% 95.94/12.89 inference(contradiction_clause,[status(thm)],[f24338])).
% 95.94/12.89 fof(f24340,plain,(
% 95.94/12.89 $false),
% 95.94/12.89 inference(sat_refutation,[status(thm)],[f252,f816,f24339])).
% 95.94/12.89 % SZS output end CNFRefutation for theBenchmark.p
% 36.51/12.94 % Elapsed time: 12.565413 seconds
% 36.51/12.94 % CPU time: 98.883242 seconds
% 36.51/12.94 % Total memory used: 560.662 MB
% 36.51/12.94 % Net memory used: 535.735 MB
%------------------------------------------------------------------------------