%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW948+1 : TPTP v9.3.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:34 PM UTC 2026
% Result : Theorem 3.62s 0.90s
% Output : CNFRefutation 3.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of formulae : 72 ( 37 unt; 0 def)
% Number of atoms : 114 ( 18 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 85 ( 43 ~; 32 |; 2 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 88 ( 88 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f67,axiom,
! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [VAR_X_7,VAR_Y_8] : constr_xor(VAR_X_7,VAR_Y_8) = constr_xor(VAR_Y_8,VAR_X_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [VAR_V_30X30,VAR_V_31] :
( ( pred_attacker(VAR_V_31)
& pred_attacker(VAR_V_30X30) )
=> pred_attacker(constr_xor(VAR_V_30X30,VAR_V_31)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [VAR_V_59] :
( pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_59))
=> pred_attacker(VAR_V_59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [VAR_V_67] :
( pred_attacker(tuple_R_out_4(VAR_V_67))
=> pred_attacker(VAR_V_67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [VAR_V_79] :
( pred_attacker(tuple_R_out_1(VAR_V_79))
=> pred_attacker(VAR_V_79) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [VAR_V_83,VAR_V_84] :
( ( pred_attacker(VAR_V_84)
& pred_attacker(VAR_V_83) )
=> pred_attacker(tuple_R_in_2(VAR_V_83,VAR_V_84)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r0x30_from_1st)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
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)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
pred_attacker(tuple_R_out_1(name_r0x30)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,axiom,
! [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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,conjecture,
pred_attacker(name_objective_R),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
~ pred_attacker(name_objective_R),
inference(negated_conjecture,[status(cth)],[f108]) ).
fof(f176,plain,
! [X0] : constr_xor(X0,X0) = constr_ZERO,
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f177,plain,
! [X0] : constr_xor(X0,constr_ZERO) = X0,
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f178,plain,
! [X0,X1] : constr_xor(X0,X1) = constr_xor(X1,X0),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f179,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(constr_xor(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f180,plain,
! [VAR_V_30X30,VAR_V_31] :
( pred_attacker(constr_xor(VAR_V_30X30,VAR_V_31))
| ~ pred_attacker(VAR_V_31)
| ~ pred_attacker(VAR_V_30X30) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f181,plain,
! [X0,X1] :
( pred_attacker(constr_xor(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f189,plain,
! [VAR_V_49,VAR_V_50X30] :
( pred_attacker(VAR_V_49)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_49,VAR_V_50X30)) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f190,plain,
! [VAR_V_49] :
( pred_attacker(VAR_V_49)
| ! [VAR_V_50X30] : ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_49,VAR_V_50X30)) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f191,plain,
! [X0,X1] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f192,plain,
! [VAR_V_52,VAR_V_53] :
( pred_attacker(VAR_V_53)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_52,VAR_V_53)) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f193,plain,
! [VAR_V_53] :
( pred_attacker(VAR_V_53)
| ! [VAR_V_52] : ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_52,VAR_V_53)) ),
inference(miniscoping,[status(thm)],[f192]) ).
fof(f194,plain,
! [X0,X1] :
( pred_attacker(X1)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
! [VAR_V_59] :
( pred_attacker(VAR_V_59)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_59)) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f198,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f205,plain,
! [VAR_V_67] :
( pred_attacker(VAR_V_67)
| ~ pred_attacker(tuple_R_out_4(VAR_V_67)) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f206,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_R_out_4(X0)) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f213,plain,
! [VAR_V_79] :
( pred_attacker(VAR_V_79)
| ~ pred_attacker(tuple_R_out_1(VAR_V_79)) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f214,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_R_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f215,plain,
! [VAR_V_83,VAR_V_84] :
( pred_attacker(tuple_R_in_2(VAR_V_83,VAR_V_84))
| ~ pred_attacker(VAR_V_84)
| ~ pred_attacker(VAR_V_83) ),
inference(pre_NNF_transformation,[status(thm)],[f89]) ).
fof(f216,plain,
! [X0,X1] :
( pred_attacker(tuple_R_in_2(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f236,plain,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r0x30_from_1st)),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f237,plain,
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)))),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f239,plain,
pred_attacker(tuple_R_out_1(name_r0x30)),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f242,plain,
! [VAR_R1_IN_244] :
( pred_attacker(tuple_R_out_4(name_objective_R))
| ~ pred_attacker(tuple_R_in_2(VAR_R1_IN_244,constr_h(constr_xor(constr_xor(name_r0x30,VAR_R1_IN_244),name_k)))) ),
inference(pre_NNF_transformation,[status(thm)],[f107]) ).
fof(f243,plain,
( pred_attacker(tuple_R_out_4(name_objective_R))
| ! [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)))) ),
inference(miniscoping,[status(thm)],[f242]) ).
fof(f244,plain,
! [X0] :
( pred_attacker(tuple_R_out_4(name_objective_R))
| ~ pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(constr_xor(name_r0x30,X0),name_k)))) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
~ pred_attacker(name_objective_R),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f246,plain,
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))))),
inference(forward_demodulation,[status(thm)],[f179,f237]) ).
fof(f252,plain,
! [X0] :
( pred_attacker(tuple_R_out_4(name_objective_R))
| ~ pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(name_r0x30,constr_xor(X0,name_k))))) ),
inference(forward_demodulation,[status(thm)],[f179,f244]) ).
fof(f255,plain,
! [X0] : X0 = constr_xor(constr_ZERO,X0),
inference(paramodulation,[status(thm)],[f177,f178]) ).
fof(f264,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(X2,constr_xor(X0,X1)),
inference(paramodulation,[status(thm)],[f178,f179]) ).
fof(f269,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(constr_xor(X1,X0),X2),
inference(paramodulation,[status(thm)],[f178,f179]) ).
fof(f271,plain,
! [X0,X1] : constr_xor(X0,constr_xor(X0,X1)) = constr_xor(constr_ZERO,X1),
inference(paramodulation,[status(thm)],[f176,f179]) ).
fof(f278,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(X1,constr_xor(X0,X2)),
inference(forward_demodulation,[status(thm)],[f179,f269]) ).
fof(f280,plain,
! [X0,X1] : constr_xor(X0,constr_xor(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f255,f271]) ).
fof(f298,plain,
pred_attacker(name_r0x30_from_1st),
inference(resolution,[status(thm)],[f198,f236]) ).
fof(f302,plain,
pred_attacker(name_r0x30),
inference(resolution,[status(thm)],[f214,f239]) ).
fof(f310,plain,
! [X0,X1] : constr_xor(X0,constr_xor(X1,X0)) = X1,
inference(paramodulation,[status(thm)],[f178,f280]) ).
fof(f338,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(constr_xor(X1,X0),X2)) = constr_xor(X1,X2),
inference(paramodulation,[status(thm)],[f310,f179]) ).
fof(f344,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,constr_xor(X0,X2))) = constr_xor(X1,X2),
inference(forward_demodulation,[status(thm)],[f179,f338]) ).
fof(f485,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(X0,constr_xor(X2,X1)),
inference(paramodulation,[status(thm)],[f264,f278]) ).
fof(f1198,plain,
pred_attacker(constr_h(constr_xor(name_r0x30_from_1st,constr_xor(name_r1_from_1st,name_k)))),
inference(resolution,[status(thm)],[f246,f194]) ).
fof(f1199,plain,
pred_attacker(name_r1_from_1st),
inference(resolution,[status(thm)],[f246,f191]) ).
fof(f1211,plain,
pred_attacker(constr_h(constr_xor(name_k,constr_xor(name_r0x30_from_1st,name_r1_from_1st)))),
inference(paramodulation,[status(thm)],[f264,f1198]) ).
fof(f1260,plain,
! [X0] :
( pred_attacker(name_objective_R)
| ~ pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(name_r0x30,constr_xor(X0,name_k))))) ),
inference(resolution,[status(thm)],[f252,f206]) ).
fof(f1261,plain,
! [X0] : ~ pred_attacker(tuple_R_in_2(X0,constr_h(constr_xor(name_r0x30,constr_xor(X0,name_k))))),
inference(forward_subsumption_resolution,[status(thm)],[f1260,f245]) ).
fof(f1262,plain,
! [X0] :
( ~ pred_attacker(constr_h(constr_xor(name_r0x30,constr_xor(X0,name_k))))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f1261,f216]) ).
fof(f1287,plain,
! [X0] :
( ~ pred_attacker(constr_h(constr_xor(name_r0x30,constr_xor(name_k,X0))))
| ~ pred_attacker(X0) ),
inference(paramodulation,[status(thm)],[f485,f1262]) ).
fof(f1600,plain,
! [X0] :
( ~ pred_attacker(constr_h(constr_xor(name_k,X0)))
| ~ pred_attacker(constr_xor(name_r0x30,X0)) ),
inference(paramodulation,[status(thm)],[f344,f1287]) ).
fof(f2568,plain,
! [X0] :
( ~ pred_attacker(X0)
| ~ pred_attacker(name_r0x30)
| ~ pred_attacker(constr_h(constr_xor(name_k,X0))) ),
inference(resolution,[status(thm)],[f1600,f181]) ).
fof(f2587,plain,
! [X0] :
( ~ pred_attacker(X0)
| ~ pred_attacker(constr_h(constr_xor(name_k,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2568,f302]) ).
fof(f2678,plain,
~ pred_attacker(constr_xor(name_r0x30_from_1st,name_r1_from_1st)),
inference(resolution,[status(thm)],[f2587,f1211]) ).
fof(f2699,plain,
( ~ pred_attacker(name_r1_from_1st)
| ~ pred_attacker(name_r0x30_from_1st) ),
inference(resolution,[status(thm)],[f2678,f181]) ).
fof(f2701,plain,
~ pred_attacker(name_r1_from_1st),
inference(forward_subsumption_resolution,[status(thm)],[f2699,f298]) ).
fof(f2702,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f1199,f2701]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW948+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n008.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 10:20:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 3.62/0.90 % Refutation found
% 3.62/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.62/0.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.76/0.92 % Elapsed time: 0.561585 seconds
% 1.76/0.92 % CPU time: 4.251491 seconds
% 1.76/0.92 % Total memory used: 117.235 MB
% 1.76/0.92 % Net memory used: 115.065 MB
%------------------------------------------------------------------------------