%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV011+1 : TPTP v9.2.1. Released v2.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 : n019.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:20:35 PM UTC 2026
% Result : Theorem 0.25s 1.62s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 17
% Syntax : Number of formulae : 37 ( 33 unt; 0 def)
% Number of atoms : 41 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 9 ( 5 ~; 2 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-1 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-4 aty)
% Number of variables : 4 ( 0 sgn 1 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
? [X1] :
( a_holds(key(X1,b))
& b_holds(key(X1,a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(ax4,axiom,
message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(ax2,axiom,
message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(ax5,axiom,
message(sent(b,t,triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(a_sent_message_i_to_b,axiom,
message(sent(a,b,pair(a,an_a_nonce))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_sent_message_i_to_b) ).
fof(ax1,axiom,
b_holds(key(generate_key(an_a_nonce),a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(ax3,axiom,
a_holds(key(generate_key(an_a_nonce),b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(ax6,axiom,
b_stored(pair(a,an_a_nonce)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(t_holds_key_bt_for_b,axiom,
t_holds(key(bt,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_holds_key_bt_for_b) ).
fof(t_holds_key_at_for_a,axiom,
t_holds(key(at,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_holds_key_at_for_a) ).
fof(b_hold_key_bt_for_t,axiom,
b_holds(key(bt,t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_hold_key_bt_for_t) ).
fof(a_stored_message_i,axiom,
a_stored(pair(b,an_a_nonce)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_stored_message_i) ).
fof(a_holds_key_at_for_t,axiom,
a_holds(key(at,t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_holds_key_at_for_t) ).
fof(nonce_a_is_fresh_to_b,axiom,
fresh_to_b(an_a_nonce),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nonce_a_is_fresh_to_b) ).
fof(b_is_party_of_protocol,axiom,
party_of_protocol(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_is_party_of_protocol) ).
fof(a_is_party_of_protocol,axiom,
party_of_protocol(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_is_party_of_protocol) ).
fof(t_is_party_of_protocol,axiom,
party_of_protocol(t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t_is_party_of_protocol) ).
fof(i_0_17,negated_conjecture,
~ ? [X1] :
( a_holds(key(X1,b))
& b_holds(key(X1,a)) ),
inference(assume_negation,[status(cth)],[co1]) ).
fof(i_0_18,negated_conjecture,
! [X3] :
( ~ a_holds(key(X3,b))
| ~ b_holds(key(X3,a)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_17])]) ).
cnf(i_0_19,plain,
message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),at),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce)))),
inference(split_conjunct,[status(thm)],[ax4]),
[final] ).
cnf(i_0_20,plain,
message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))))),
inference(split_conjunct,[status(thm)],[ax2]),
[final] ).
cnf(i_0_21,plain,
message(sent(b,t,triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))),
inference(split_conjunct,[status(thm)],[ax5]),
[final] ).
cnf(i_0_22,plain,
message(sent(a,b,pair(a,an_a_nonce))),
inference(split_conjunct,[status(thm)],[a_sent_message_i_to_b]),
[final] ).
cnf(i_0_23,negated_conjecture,
( ~ a_holds(key(X1,b))
| ~ b_holds(key(X1,a)) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_24,plain,
b_holds(key(generate_key(an_a_nonce),a)),
inference(split_conjunct,[status(thm)],[ax1]),
[final] ).
cnf(i_0_25,plain,
a_holds(key(generate_key(an_a_nonce),b)),
inference(split_conjunct,[status(thm)],[ax3]),
[final] ).
cnf(i_0_26,plain,
b_stored(pair(a,an_a_nonce)),
inference(split_conjunct,[status(thm)],[ax6]),
[final] ).
cnf(i_0_27,plain,
t_holds(key(bt,b)),
inference(split_conjunct,[status(thm)],[t_holds_key_bt_for_b]),
[final] ).
cnf(i_0_28,plain,
t_holds(key(at,a)),
inference(split_conjunct,[status(thm)],[t_holds_key_at_for_a]),
[final] ).
cnf(i_0_29,plain,
b_holds(key(bt,t)),
inference(split_conjunct,[status(thm)],[b_hold_key_bt_for_t]),
[final] ).
cnf(i_0_30,plain,
a_stored(pair(b,an_a_nonce)),
inference(split_conjunct,[status(thm)],[a_stored_message_i]),
[final] ).
cnf(i_0_31,plain,
a_holds(key(at,t)),
inference(split_conjunct,[status(thm)],[a_holds_key_at_for_t]),
[final] ).
cnf(i_0_32,plain,
fresh_to_b(an_a_nonce),
inference(split_conjunct,[status(thm)],[nonce_a_is_fresh_to_b]),
[final] ).
cnf(i_0_33,plain,
party_of_protocol(b),
inference(split_conjunct,[status(thm)],[b_is_party_of_protocol]),
[final] ).
cnf(i_0_34,plain,
party_of_protocol(a),
inference(split_conjunct,[status(thm)],[a_is_party_of_protocol]),
[final] ).
cnf(i_0_35,plain,
party_of_protocol(t),
inference(split_conjunct,[status(thm)],[t_is_party_of_protocol]),
[final] ).
cnf(i_0_36,plain,
$false,
inference(scs_inference,[],[i_0_25,i_0_24,i_0_23]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SWV011+1 : TPTP v9.2.1. Released v2.4.0.
% 0.11/0.13 % 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.15/0.34 % Computer : n019.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 04:53:29 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 0.25/1.62 % Version : CSE_E---1.7
% 0.25/1.62 % Problem : theBenchmark.p
% 0.25/1.62 % SZS status Theorem for theBenchmark.p
% 0.25/1.62 % SZS output start CNFRefutation
% See solution above
% 0.25/1.64 % Total time : 1.272s
%------------------------------------------------------------------------------