%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW949+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 : n014.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 118.97s 15.57s
% Output : CNFRefutation 118.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of formulae : 67 ( 31 unt; 0 def)
% Number of atoms : 111 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 89 ( 45 ~; 34 |; 2 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 77 ( 77 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f79,axiom,
! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,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(f82,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(f83,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(f88,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(f89,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(f91,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(f100,axiom,
! [VAR_V_77] :
( pred_attacker(tuple_R_out_4(VAR_V_77))
=> pred_attacker(VAR_V_77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [VAR_V_89] :
( pred_attacker(tuple_R_out_1(VAR_V_89))
=> pred_attacker(VAR_V_89) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [VAR_V_93,VAR_V_94] :
( ( pred_attacker(VAR_V_94)
& pred_attacker(VAR_V_93) )
=> pred_attacker(tuple_R_in_2(VAR_V_93,VAR_V_94)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,axiom,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r1_from_1st)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,axiom,
pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_t,name_r2_from_1st),constr_f(constr_xor(name_r1_from_1st,name_r2_from_1st),name_t))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
pred_attacker(tuple_R_out_1(name_r1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [VAR_M1_IN_250X30] :
( pred_attacker(tuple_R_in_2(VAR_M1_IN_250X30,constr_f(constr_xor(name_r1,constr_xor(VAR_M1_IN_250X30,name_t)),name_t)))
=> pred_attacker(tuple_R_out_4(name_objective)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,conjecture,
pred_attacker(name_objective),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,negated_conjecture,
~ pred_attacker(name_objective),
inference(negated_conjecture,[status(cth)],[f124]) ).
fof(f204,plain,
! [X0] : constr_xor(X0,X0) = constr_ZERO,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f205,plain,
! [X0] : X0 = constr_xor(X0,constr_ZERO),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f206,plain,
! [X0,X1] : constr_xor(X0,X1) = constr_xor(X1,X0),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f207,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(constr_xor(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f208,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)],[f83]) ).
fof(f209,plain,
! [X0,X1] :
( pred_attacker(constr_xor(X0,X1))
| ~ pred_attacker(X1)
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f217,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)],[f88]) ).
fof(f218,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)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,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)],[f89]) ).
fof(f221,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)],[f220]) ).
fof(f222,plain,
! [X0,X1] :
( ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X1,X0))
| pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f225,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)],[f91]) ).
fof(f226,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f241,plain,
! [VAR_V_77] :
( pred_attacker(VAR_V_77)
| ~ pred_attacker(tuple_R_out_4(VAR_V_77)) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f242,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_R_out_4(X0)) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f249,plain,
! [VAR_V_89] :
( pred_attacker(VAR_V_89)
| ~ pred_attacker(tuple_R_out_1(VAR_V_89)) ),
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f250,plain,
! [X0] :
( pred_attacker(X0)
| ~ pred_attacker(tuple_R_out_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f251,plain,
! [VAR_V_93,VAR_V_94] :
( pred_attacker(tuple_R_in_2(VAR_V_93,VAR_V_94))
| ~ pred_attacker(VAR_V_94)
| ~ pred_attacker(VAR_V_93) ),
inference(pre_NNF_transformation,[status(thm)],[f105]) ).
fof(f252,plain,
! [X0,X1] :
( ~ pred_attacker(X1)
| pred_attacker(tuple_R_in_2(X0,X1))
| ~ pred_attacker(X0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f272,plain,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r1_from_1st)),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f273,plain,
pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_t,name_r2_from_1st),constr_f(constr_xor(name_r1_from_1st,name_r2_from_1st),name_t))),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f275,plain,
pred_attacker(tuple_R_out_1(name_r1)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f278,plain,
! [VAR_M1_IN_250X30] :
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(VAR_M1_IN_250X30,constr_f(constr_xor(name_r1,constr_xor(VAR_M1_IN_250X30,name_t)),name_t))) ),
inference(pre_NNF_transformation,[status(thm)],[f123]) ).
fof(f279,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ! [VAR_M1_IN_250X30] : ~ pred_attacker(tuple_R_in_2(VAR_M1_IN_250X30,constr_f(constr_xor(name_r1,constr_xor(VAR_M1_IN_250X30,name_t)),name_t))) ),
inference(miniscoping,[status(thm)],[f278]) ).
fof(f280,plain,
! [X0] :
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(X0,constr_f(constr_xor(name_r1,constr_xor(X0,name_t)),name_t))) ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f281,plain,
~ pred_attacker(name_objective),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f282,plain,
pred_attacker(name_r1),
inference(resolution,[status(thm)],[f250,f275]) ).
fof(f283,plain,
pred_attacker(name_r1_from_1st),
inference(resolution,[status(thm)],[f226,f272]) ).
fof(f299,plain,
! [X0] : constr_xor(constr_ZERO,X0) = X0,
inference(paramodulation,[status(thm)],[f206,f205]) ).
fof(f320,plain,
! [X0,X1,X2] : constr_xor(X0,constr_xor(X1,X2)) = constr_xor(X1,constr_xor(X2,X0)),
inference(paramodulation,[status(thm)],[f206,f207]) ).
fof(f328,plain,
! [X0,X1] : constr_xor(X0,constr_xor(X0,X1)) = constr_xor(constr_ZERO,X1),
inference(paramodulation,[status(thm)],[f204,f207]) ).
fof(f330,plain,
! [X0,X1,X2] :
( pred_attacker(constr_xor(X0,constr_xor(X1,X2)))
| ~ pred_attacker(X2)
| ~ pred_attacker(constr_xor(X0,X1)) ),
inference(paramodulation,[status(thm)],[f207,f209]) ).
fof(f335,plain,
! [X0,X1] : X0 = constr_xor(X1,constr_xor(X1,X0)),
inference(forward_demodulation,[status(thm)],[f299,f328]) ).
fof(f346,plain,
! [X0,X1] : constr_xor(X0,constr_xor(X1,X0)) = X1,
inference(paramodulation,[status(thm)],[f206,f335]) ).
fof(f357,plain,
! [X0] :
( pred_attacker(name_objective)
| ~ pred_attacker(tuple_R_in_2(X0,constr_f(constr_xor(name_r1,constr_xor(X0,name_t)),name_t))) ),
inference(resolution,[status(thm)],[f280,f242]) ).
fof(f358,plain,
! [X0] : ~ pred_attacker(tuple_R_in_2(X0,constr_f(constr_xor(name_r1,constr_xor(X0,name_t)),name_t))),
inference(forward_subsumption_resolution,[status(thm)],[f357,f281]) ).
fof(f393,plain,
! [X0] :
( ~ pred_attacker(constr_f(constr_xor(name_r1,constr_xor(X0,name_t)),name_t))
| ~ pred_attacker(X0) ),
inference(resolution,[status(thm)],[f358,f252]) ).
fof(f415,plain,
pred_attacker(constr_f(constr_xor(name_r1_from_1st,name_r2_from_1st),name_t)),
inference(resolution,[status(thm)],[f273,f222]) ).
fof(f416,plain,
pred_attacker(constr_xor(name_t,name_r2_from_1st)),
inference(resolution,[status(thm)],[f273,f219]) ).
fof(f431,plain,
pred_attacker(constr_f(constr_xor(name_r2_from_1st,name_r1_from_1st),name_t)),
inference(paramodulation,[status(thm)],[f206,f415]) ).
fof(f433,plain,
! [X0] :
( ~ pred_attacker(X0)
| pred_attacker(constr_xor(name_t,constr_xor(name_r2_from_1st,X0))) ),
inference(resolution,[status(thm)],[f330,f416]) ).
fof(f1474,plain,
! [X0] :
( ~ pred_attacker(X0)
| ~ pred_attacker(constr_f(constr_xor(name_t,constr_xor(name_r1,X0)),name_t)) ),
inference(paramodulation,[status(thm)],[f320,f393]) ).
fof(f2850,plain,
! [X0] :
( ~ pred_attacker(constr_f(constr_xor(name_t,X0),name_t))
| ~ pred_attacker(constr_xor(X0,name_r1)) ),
inference(paramodulation,[status(thm)],[f346,f1474]) ).
fof(f5052,plain,
! [X0] :
( ~ pred_attacker(name_r1)
| ~ pred_attacker(X0)
| ~ pred_attacker(constr_f(constr_xor(name_t,X0),name_t)) ),
inference(resolution,[status(thm)],[f2850,f209]) ).
fof(f5059,plain,
! [X0] :
( ~ pred_attacker(constr_f(constr_xor(name_t,X0),name_t))
| ~ pred_attacker(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5052,f282]) ).
fof(f5245,plain,
! [X0] :
( ~ pred_attacker(constr_xor(name_t,X0))
| ~ pred_attacker(constr_f(X0,name_t)) ),
inference(paramodulation,[status(thm)],[f335,f5059]) ).
fof(f5530,plain,
~ pred_attacker(constr_xor(name_t,constr_xor(name_r2_from_1st,name_r1_from_1st))),
inference(resolution,[status(thm)],[f5245,f431]) ).
fof(f5533,plain,
~ pred_attacker(name_r1_from_1st),
inference(resolution,[status(thm)],[f5530,f433]) ).
fof(f5535,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5533,f283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW949+1 : TPTP v9.3.1. Released v7.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n014.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 10:20:04 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.44 % Drodi V4.1.1
% 118.97/15.57 % Refutation found
% 118.97/15.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 118.97/15.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.63/15.62 % Elapsed time: 15.177028 seconds
% 7.63/15.62 % CPU time: 119.688592 seconds
% 7.63/15.62 % Total memory used: 299.106 MB
% 7.63/15.62 % Net memory used: 289.332 MB
%------------------------------------------------------------------------------