%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWW949+1 : TPTP v9.2.1. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:33:27 PM UTC 2026
% Result : Theorem 19.84s 13.34s
% Output : CNFRefutation 19.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 62 ( 31 unt; 0 def)
% Number of atoms : 102 ( 15 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 73 ( 33 ~; 30 |; 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 : 71 ( 2 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax81,axiom,
! [X5,X6,X7] : constr_xor(X5,constr_xor(X6,X7)) = constr_xor(constr_xor(X5,X6),X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax81) ).
fof(ax80,axiom,
! [X3,X4] : constr_xor(X3,X4) = constr_xor(X4,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax80) ).
fof(ax79,axiom,
! [X2] : constr_xor(X2,constr_ZERO) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax79) ).
fof(ax122,axiom,
! [X45] :
( pred_attacker(tuple_R_in_2(X45,constr_f(constr_xor(name_r1,constr_xor(X45,name_t)),name_t)))
=> pred_attacker(tuple_R_out_4(name_objective)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax122) ).
fof(ax78,axiom,
! [X1] : constr_xor(X1,X1) = constr_ZERO,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax78) ).
fof(ax104,axiom,
! [X32,X33] :
( ( pred_attacker(X32)
& pred_attacker(X33) )
=> pred_attacker(tuple_R_in_2(X32,X33)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax104) ).
fof(ax82,axiom,
! [X8,X9] :
( ( pred_attacker(X8)
& pred_attacker(X9) )
=> pred_attacker(constr_xor(X8,X9)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax82) ).
fof(ax103,axiom,
! [X31] :
( pred_attacker(tuple_R_out_1(X31))
=> pred_attacker(X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax103) ).
fof(ax120,axiom,
pred_attacker(tuple_R_out_1(name_r1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax120) ).
fof(ax88,axiom,
! [X16,X17] :
( pred_attacker(tuple_knowledge_from_1st_round_out_2(X16,X17))
=> pred_attacker(X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax88) ).
fof(ax118,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/sandbox2/benchmark/theBenchmark.p',ax118) ).
fof(ax99,axiom,
! [X27] :
( pred_attacker(tuple_R_out_4(X27))
=> pred_attacker(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax99) ).
fof(co0,conjecture,
pred_attacker(name_objective),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co0) ).
fof(ax87,axiom,
! [X14,X15] :
( pred_attacker(tuple_knowledge_from_1st_round_out_2(X14,X15))
=> pred_attacker(X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax87) ).
fof(ax90,axiom,
! [X19] :
( pred_attacker(tuple_knowledge_from_1st_round_out_1(X19))
=> pred_attacker(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax90) ).
fof(ax117,axiom,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r1_from_1st)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax117) ).
fof(c_0_16,plain,
! [X95,X96,X97] : constr_xor(X95,constr_xor(X96,X97)) = constr_xor(constr_xor(X95,X96),X97),
inference(variable_rename,[status(thm)],[ax81]) ).
fof(c_0_17,plain,
! [X93,X94] : constr_xor(X93,X94) = constr_xor(X94,X93),
inference(variable_rename,[status(thm)],[ax80]) ).
fof(c_0_18,plain,
! [X92] : constr_xor(X92,constr_ZERO) = X92,
inference(variable_rename,[status(thm)],[ax79]) ).
fof(c_0_19,plain,
! [X135] :
( ~ pred_attacker(tuple_R_in_2(X135,constr_f(constr_xor(name_r1,constr_xor(X135,name_t)),name_t)))
| pred_attacker(tuple_R_out_4(name_objective)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax122])]) ).
cnf(c_0_20,plain,
constr_xor(X1,constr_xor(X2,X3)) = constr_xor(constr_xor(X1,X2),X3),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_21,plain,
constr_xor(X1,X2) = constr_xor(X2,X1),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
fof(c_0_22,plain,
! [X91] : constr_xor(X91,X91) = constr_ZERO,
inference(variable_rename,[status(thm)],[ax78]) ).
cnf(c_0_23,plain,
constr_xor(X1,constr_ZERO) = X1,
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_24,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(X1,constr_f(constr_xor(name_r1,constr_xor(X1,name_t)),name_t))) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_25,plain,
constr_xor(X1,constr_xor(X2,X3)) = constr_xor(X2,constr_xor(X3,X1)),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_26,plain,
constr_xor(X1,X1) = constr_ZERO,
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_27,plain,
constr_xor(constr_ZERO,X1) = X1,
inference(spm,[status(thm)],[c_0_23,c_0_21]) ).
cnf(c_0_28,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(X1,constr_f(constr_xor(name_t,constr_xor(name_r1,X1)),name_t))) ),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_29,plain,
constr_xor(X1,constr_xor(X1,X2)) = X2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_26]),c_0_27]) ).
cnf(c_0_30,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(constr_xor(name_r1,X1),constr_f(constr_xor(name_t,X1),name_t))) ),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
fof(c_0_31,plain,
! [X122,X123] :
( ~ pred_attacker(X122)
| ~ pred_attacker(X123)
| pred_attacker(tuple_R_in_2(X122,X123)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax104])]) ).
fof(c_0_32,plain,
! [X98,X99] :
( ~ pred_attacker(X98)
| ~ pred_attacker(X99)
| pred_attacker(constr_xor(X98,X99)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax82])]) ).
fof(c_0_33,plain,
! [X121] :
( ~ pred_attacker(tuple_R_out_1(X121))
| pred_attacker(X121) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax103])]) ).
cnf(c_0_34,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(tuple_R_in_2(constr_xor(name_t,constr_xor(X1,name_r1)),constr_f(X1,name_t))) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_29]),c_0_25]) ).
cnf(c_0_35,plain,
( pred_attacker(tuple_R_in_2(X1,X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(X2) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_36,plain,
( pred_attacker(constr_xor(X1,X2))
| ~ pred_attacker(X1)
| ~ pred_attacker(X2) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_37,plain,
( pred_attacker(X1)
| ~ pred_attacker(tuple_R_out_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_38,plain,
pred_attacker(tuple_R_out_1(name_r1)),
inference(split_conjunct,[status(thm)],[ax120]) ).
fof(c_0_39,plain,
! [X106,X107] :
( ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X106,X107))
| pred_attacker(X107) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax88])]) ).
cnf(c_0_40,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(split_conjunct,[status(thm)],[ax118]) ).
cnf(c_0_41,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(constr_xor(name_t,constr_xor(X1,name_r1)))
| ~ pred_attacker(constr_f(X1,name_t)) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_42,plain,
( pred_attacker(constr_xor(X1,constr_xor(X2,X3)))
| ~ pred_attacker(constr_xor(X1,X2))
| ~ pred_attacker(X3) ),
inference(spm,[status(thm)],[c_0_36,c_0_20]) ).
cnf(c_0_43,plain,
pred_attacker(name_r1),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_44,plain,
( pred_attacker(X2)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_45,plain,
pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_t,name_r2_from_1st),constr_f(constr_xor(name_r2_from_1st,name_r1_from_1st),name_t))),
inference(rw,[status(thm)],[c_0_40,c_0_21]) ).
fof(c_0_46,plain,
! [X117] :
( ~ pred_attacker(tuple_R_out_4(X117))
| pred_attacker(X117) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax99])]) ).
cnf(c_0_47,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(constr_f(X1,name_t))
| ~ pred_attacker(constr_xor(name_t,X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_42]),c_0_43])]) ).
cnf(c_0_48,plain,
pred_attacker(constr_f(constr_xor(name_r2_from_1st,name_r1_from_1st),name_t)),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
fof(c_0_49,negated_conjecture,
~ pred_attacker(name_objective),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[co0])]) ).
fof(c_0_50,plain,
! [X104,X105] :
( ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X104,X105))
| pred_attacker(X104) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax87])]) ).
fof(c_0_51,plain,
! [X109] :
( ~ pred_attacker(tuple_knowledge_from_1st_round_out_1(X109))
| pred_attacker(X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax90])]) ).
cnf(c_0_52,plain,
( pred_attacker(X1)
| ~ pred_attacker(tuple_R_out_4(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_53,plain,
( pred_attacker(tuple_R_out_4(name_objective))
| ~ pred_attacker(constr_xor(name_t,constr_xor(name_r2_from_1st,name_r1_from_1st))) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_54,negated_conjecture,
~ pred_attacker(name_objective),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
cnf(c_0_55,plain,
( pred_attacker(X1)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_56,plain,
( pred_attacker(X1)
| ~ pred_attacker(tuple_knowledge_from_1st_round_out_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_57,plain,
pred_attacker(tuple_knowledge_from_1st_round_out_1(name_r1_from_1st)),
inference(split_conjunct,[status(thm)],[ax117]) ).
cnf(c_0_58,plain,
~ pred_attacker(constr_xor(name_t,constr_xor(name_r2_from_1st,name_r1_from_1st))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_54]) ).
cnf(c_0_59,plain,
pred_attacker(constr_xor(name_t,name_r2_from_1st)),
inference(spm,[status(thm)],[c_0_55,c_0_45]) ).
cnf(c_0_60,plain,
pred_attacker(name_r1_from_1st),
inference(spm,[status(thm)],[c_0_56,c_0_57]) ).
cnf(c_0_61,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_42]),c_0_59]),c_0_60])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWW949+1 : TPTP v9.2.1. Released v7.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n022.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 07:35:51 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 19.84/13.34 % Version : CSE_E---1.7
% 19.84/13.34 % Problem : theBenchmark.p
% 19.84/13.34 % SZS status Theorem for theBenchmark.p
% 19.84/13.34 % SZS output start CNFRefutation
% See solution above
% 19.94/13.41 % Total time : 10.383s
%------------------------------------------------------------------------------