%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV010+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 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 : Thu May 9 17:44:06 EDT 2024
% Result : Satisfiable 0.39s 0.57s
% Output : Saturation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SWV010+1 : TPTP v8.1.2. Released v2.4.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Thu May 9 05:15:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.39/0.57 % Version: 1.5
% 0.39/0.57 % SZS status Satisfiable
% 0.39/0.57 % SZS output start Saturation
% 0.39/0.57 fof(nonce_a_is_fresh_to_b,axiom,fresh_to_b(an_a_nonce),file('/export/starexec/sandbox/benchmark/theBenchmark.p', nonce_a_is_fresh_to_b)).
% 0.39/0.57 cnf(c16,plain,fresh_to_b(an_a_nonce),inference(split_conjunct,[status(thm)],[nonce_a_is_fresh_to_b])).
% 0.39/0.57 fof(a_sent_message_i_to_b,axiom,message(sent(a,b,pair(a,an_a_nonce))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a_sent_message_i_to_b)).
% 0.39/0.57 cnf(c27,plain,message(sent(a,b,pair(a,an_a_nonce))),inference(split_conjunct,[status(thm)],[a_sent_message_i_to_b])).
% 0.39/0.57 fof(b_creates_freash_nonces_in_time,axiom,(![U]:(![V]:((message(sent(U,b,pair(U,V)))&fresh_to_b(V))=>(message(sent(b,t,triple(b,generate_b_nonce(V),encrypt(triple(U,V,generate_expiration_time(V)),bt))))&b_stored(pair(U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', b_creates_freash_nonces_in_time)).
% 0.39/0.57 fof(c11,plain,(![U]:(![V]:((~message(sent(U,b,pair(U,V)))|~fresh_to_b(V))|(message(sent(b,t,triple(b,generate_b_nonce(V),encrypt(triple(U,V,generate_expiration_time(V)),bt))))&b_stored(pair(U,V)))))),inference(fof_nnf,[status(thm)],[b_creates_freash_nonces_in_time])).
% 0.39/0.57 fof(c12,plain,(![X12]:(![X13]:((~message(sent(X12,b,pair(X12,X13)))|~fresh_to_b(X13))|(message(sent(b,t,triple(b,generate_b_nonce(X13),encrypt(triple(X12,X13,generate_expiration_time(X13)),bt))))&b_stored(pair(X12,X13)))))),inference(variable_rename,[status(thm)],[c11])).
% 0.39/0.57 fof(c13,plain,(![X12]:(![X13]:(((~message(sent(X12,b,pair(X12,X13)))|~fresh_to_b(X13))|message(sent(b,t,triple(b,generate_b_nonce(X13),encrypt(triple(X12,X13,generate_expiration_time(X13)),bt)))))&((~message(sent(X12,b,pair(X12,X13)))|~fresh_to_b(X13))|b_stored(pair(X12,X13)))))),inference(distribute,[status(thm)],[c12])).
% 0.39/0.57 cnf(c15,plain,~message(sent(X30,b,pair(X30,X31)))|~fresh_to_b(X31)|b_stored(pair(X30,X31)),inference(split_conjunct,[status(thm)],[c13])).
% 0.39/0.57 cnf(c30,plain,~fresh_to_b(an_a_nonce)|b_stored(pair(a,an_a_nonce)),inference(resolution,[status(thm)],[c15, c27])).
% 0.39/0.57 cnf(c31,plain,b_stored(pair(a,an_a_nonce)),inference(resolution,[status(thm)],[c30, c16])).
% 0.39/0.57 fof(b_accepts_secure_session_key,axiom,(![V]:(![X]:(![Y]:((message(sent(X,b,pair(encrypt(triple(X,V,generate_expiration_time(Y)),bt),encrypt(generate_b_nonce(Y),V))))&b_stored(pair(X,Y)))=>b_holds(key(V,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', b_accepts_secure_session_key)).
% 0.39/0.57 fof(c6,plain,(![V]:(![X]:(![Y]:((~message(sent(X,b,pair(encrypt(triple(X,V,generate_expiration_time(Y)),bt),encrypt(generate_b_nonce(Y),V))))|~b_stored(pair(X,Y)))|b_holds(key(V,X)))))),inference(fof_nnf,[status(thm)],[b_accepts_secure_session_key])).
% 0.39/0.57 fof(c7,plain,(![V]:(![X]:((![Y]:(~message(sent(X,b,pair(encrypt(triple(X,V,generate_expiration_time(Y)),bt),encrypt(generate_b_nonce(Y),V))))|~b_stored(pair(X,Y))))|b_holds(key(V,X))))),inference(shift_quantors,[status(thm)],[c6])).
% 0.39/0.57 fof(c9,plain,(![X9]:(![X10]:(![X11]:((~message(sent(X10,b,pair(encrypt(triple(X10,X9,generate_expiration_time(X11)),bt),encrypt(generate_b_nonce(X11),X9))))|~b_stored(pair(X10,X11)))|b_holds(key(X9,X10)))))),inference(shift_quantors,[status(thm)],[fof(c8,plain,(![X9]:(![X10]:((![X11]:(~message(sent(X10,b,pair(encrypt(triple(X10,X9,generate_expiration_time(X11)),bt),encrypt(generate_b_nonce(X11),X9))))|~b_stored(pair(X10,X11))))|b_holds(key(X9,X10))))),inference(variable_rename,[status(thm)],[c7])).])).
% 0.39/0.57 cnf(c10,plain,~message(sent(X28,b,pair(encrypt(triple(X28,X27,generate_expiration_time(X29)),bt),encrypt(generate_b_nonce(X29),X27))))|~b_stored(pair(X28,X29))|b_holds(key(X27,X28)),inference(split_conjunct,[status(thm)],[c9])).
% 0.39/0.57 fof(a_stored_message_i,axiom,a_stored(pair(b,an_a_nonce)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a_stored_message_i)).
% 0.39/0.57 cnf(c26,plain,a_stored(pair(b,an_a_nonce)),inference(split_conjunct,[status(thm)],[a_stored_message_i])).
% 0.39/0.57 fof(a_forwards_secure,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:((message(sent(t,a,triple(encrypt(quadruple(Y,Z,W,V),at),X,U)))&a_stored(pair(Y,Z)))=>(message(sent(a,Y,pair(X,encrypt(U,W))))&a_holds(key(W,Y)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a_forwards_secure)).
% 0.39/0.57 fof(c19,plain,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:((~message(sent(t,a,triple(encrypt(quadruple(Y,Z,W,V),at),X,U)))|~a_stored(pair(Y,Z)))|(message(sent(a,Y,pair(X,encrypt(U,W))))&a_holds(key(W,Y)))))))))),inference(fof_nnf,[status(thm)],[a_forwards_secure])).
% 0.39/0.57 fof(c20,plain,(![U]:(![V]:(![W]:(![X]:(![Y]:((![Z]:(~message(sent(t,a,triple(encrypt(quadruple(Y,Z,W,V),at),X,U)))|~a_stored(pair(Y,Z))))|(message(sent(a,Y,pair(X,encrypt(U,W))))&a_holds(key(W,Y))))))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.39/0.57 fof(c22,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~message(sent(t,a,triple(encrypt(quadruple(X18,X19,X16,X15),at),X17,X14)))|~a_stored(pair(X18,X19)))|(message(sent(a,X18,pair(X17,encrypt(X14,X16))))&a_holds(key(X16,X18)))))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:((![X19]:(~message(sent(t,a,triple(encrypt(quadruple(X18,X19,X16,X15),at),X17,X14)))|~a_stored(pair(X18,X19))))|(message(sent(a,X18,pair(X17,encrypt(X14,X16))))&a_holds(key(X16,X18))))))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.39/0.57 fof(c23,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((~message(sent(t,a,triple(encrypt(quadruple(X18,X19,X16,X15),at),X17,X14)))|~a_stored(pair(X18,X19)))|message(sent(a,X18,pair(X17,encrypt(X14,X16)))))&((~message(sent(t,a,triple(encrypt(quadruple(X18,X19,X16,X15),at),X17,X14)))|~a_stored(pair(X18,X19)))|a_holds(key(X16,X18)))))))))),inference(distribute,[status(thm)],[c22])).
% 0.39/0.57 cnf(c24,plain,~message(sent(t,a,triple(encrypt(quadruple(X44,X42,X43,X40),at),X45,X41)))|~a_stored(pair(X44,X42))|message(sent(a,X44,pair(X45,encrypt(X41,X43)))),inference(split_conjunct,[status(thm)],[c23])).
% 0.39/0.57 fof(t_holds_key_bt_for_b,axiom,t_holds(key(bt,b)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t_holds_key_bt_for_b)).
% 0.39/0.57 cnf(c4,plain,t_holds(key(bt,b)),inference(split_conjunct,[status(thm)],[t_holds_key_bt_for_b])).
% 0.39/0.57 fof(t_holds_key_at_for_a,axiom,t_holds(key(at,a)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t_holds_key_at_for_a)).
% 0.39/0.57 cnf(c5,plain,t_holds(key(at,a)),inference(split_conjunct,[status(thm)],[t_holds_key_at_for_a])).
% 0.39/0.57 fof(server_t_generates_key,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(((message(sent(U,t,triple(U,V,encrypt(triple(W,X,Y),Z))))&t_holds(key(Z,U)))&t_holds(key(X1,W)))=>message(sent(t,W,triple(encrypt(quadruple(U,X,generate_key(X),Y),X1),encrypt(triple(W,generate_key(X),Y),Z),V))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', server_t_generates_key)).
% 0.39/0.57 fof(c0,plain,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(((~message(sent(U,t,triple(U,V,encrypt(triple(W,X,Y),Z))))|~t_holds(key(Z,U)))|~t_holds(key(X1,W)))|message(sent(t,W,triple(encrypt(quadruple(U,X,generate_key(X),Y),X1),encrypt(triple(W,generate_key(X),Y),Z),V))))))))))),inference(fof_nnf,[status(thm)],[server_t_generates_key])).
% 0.39/0.57 fof(c1,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(((~message(sent(X2,t,triple(X2,X3,encrypt(triple(X4,X5,X6),X7))))|~t_holds(key(X7,X2)))|~t_holds(key(X8,X4)))|message(sent(t,X4,triple(encrypt(quadruple(X2,X5,generate_key(X5),X6),X8),encrypt(triple(X4,generate_key(X5),X6),X7),X3))))))))))),inference(variable_rename,[status(thm)],[c0])).
% 0.39/0.57 cnf(c2,plain,~message(sent(X24,t,triple(X24,X21,encrypt(triple(X20,X22,X26),X25))))|~t_holds(key(X25,X24))|~t_holds(key(X23,X20))|message(sent(t,X20,triple(encrypt(quadruple(X24,X22,generate_key(X22),X26),X23),encrypt(triple(X20,generate_key(X22),X26),X25),X21))),inference(split_conjunct,[status(thm)],[c1])).
% 0.39/0.57 cnf(c14,plain,~message(sent(X38,b,pair(X38,X39)))|~fresh_to_b(X39)|message(sent(b,t,triple(b,generate_b_nonce(X39),encrypt(triple(X38,X39,generate_expiration_time(X39)),bt)))),inference(split_conjunct,[status(thm)],[c13])).
% 0.39/0.57 cnf(c32,plain,~fresh_to_b(an_a_nonce)|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(resolution,[status(thm)],[c14, c27])).
% 0.39/0.57 cnf(c33,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(resolution,[status(thm)],[c32, c16])).
% 0.39/0.57 cnf(c34,plain,~t_holds(key(bt,b))|~t_holds(key(X46,a))|message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),X46),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce)))),inference(resolution,[status(thm)],[c33, c2])).
% 0.39/0.57 cnf(c35,plain,~t_holds(key(bt,b))|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(resolution,[status(thm)],[c34, c5])).
% 0.39/0.57 cnf(c36,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(resolution,[status(thm)],[c35, c4])).
% 0.39/0.57 cnf(c38,plain,~a_stored(pair(b,an_a_nonce))|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(resolution,[status(thm)],[c36, c24])).
% 0.39/0.57 cnf(c40,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(resolution,[status(thm)],[c38, c26])).
% 0.39/0.57 cnf(c41,plain,~b_stored(pair(a,an_a_nonce))|b_holds(key(generate_key(an_a_nonce),a)),inference(resolution,[status(thm)],[c40, c10])).
% 0.39/0.57 cnf(c42,plain,b_holds(key(generate_key(an_a_nonce),a)),inference(resolution,[status(thm)],[c41, c31])).
% 0.39/0.57 cnf(c25,plain,~message(sent(t,a,triple(encrypt(quadruple(X36,X34,X35,X32),at),X37,X33)))|~a_stored(pair(X36,X34))|a_holds(key(X35,X36)),inference(split_conjunct,[status(thm)],[c23])).
% 0.39/0.57 cnf(c37,plain,~a_stored(pair(b,an_a_nonce))|a_holds(key(generate_key(an_a_nonce),b)),inference(resolution,[status(thm)],[c36, c25])).
% 0.39/0.57 cnf(c39,plain,a_holds(key(generate_key(an_a_nonce),b)),inference(resolution,[status(thm)],[c37, c26])).
% 0.39/0.57 fof(a_holds_key_at_for_t,axiom,a_holds(key(at,t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a_holds_key_at_for_t)).
% 0.39/0.57 cnf(c29,plain,a_holds(key(at,t)),inference(split_conjunct,[status(thm)],[a_holds_key_at_for_t])).
% 0.39/0.57 fof(b_hold_key_bt_for_t,axiom,b_holds(key(bt,t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', b_hold_key_bt_for_t)).
% 0.39/0.57 cnf(c18,plain,b_holds(key(bt,t)),inference(split_conjunct,[status(thm)],[b_hold_key_bt_for_t])).
% 0.39/0.57 fof(a_is_party_of_protocol,axiom,party_of_protocol(a),file('/export/starexec/sandbox/benchmark/theBenchmark.p', a_is_party_of_protocol)).
% 0.39/0.57 cnf(c28,plain,party_of_protocol(a),inference(split_conjunct,[status(thm)],[a_is_party_of_protocol])).
% 0.39/0.57 fof(b_is_party_of_protocol,axiom,party_of_protocol(b),file('/export/starexec/sandbox/benchmark/theBenchmark.p', b_is_party_of_protocol)).
% 0.39/0.57 cnf(c17,plain,party_of_protocol(b),inference(split_conjunct,[status(thm)],[b_is_party_of_protocol])).
% 0.39/0.57 fof(t_is_party_of_protocol,axiom,party_of_protocol(t),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t_is_party_of_protocol)).
% 0.39/0.57 cnf(c3,plain,party_of_protocol(t),inference(split_conjunct,[status(thm)],[t_is_party_of_protocol])).
% 0.39/0.57 % SZS output end Saturation
% 0.39/0.57
% 0.39/0.57 % Initial clauses : 16
% 0.39/0.57 % Processed clauses : 29
% 0.39/0.57 % Factors computed : 0
% 0.39/0.57 % Resolvents computed: 13
% 0.39/0.57 % Tautologies deleted: 0
% 0.39/0.57 % Forward subsumed : 0
% 0.39/0.57 % Backward subsumed : 6
% 0.39/0.57 % -------- CPU Time ---------
% 0.39/0.57 % User time : 0.180 s
% 0.39/0.57 % System time : 0.023 s
% 0.39/0.57 % Total time : 0.203 s
%------------------------------------------------------------------------------