%------------------------------------------------------------------------------
% File : iProver-SAT---3.9.4
% Problem : SWV017-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% Computer : n002.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 : Fri Sep 25 03:24:45 PM UTC 2026
% Result : Satisfiable 3.81s 1.27s
% Output : Saturation 3.81s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
party_of_protocol(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_is_party_of_protocol_2) ).
fof(f2,axiom,
message(sent(a,b,pair(a,an_a_nonce))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_sent_message_i_to_b_3) ).
fof(f3,axiom,
a_stored(pair(b,an_a_nonce)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_stored_message_i_4) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ message(sent(t,a,triple(encrypt(quadruple(X0,X4,X3,X5),at),X1,X2)))
| ~ a_stored(pair(X0,X4))
| message(sent(a,X0,pair(X1,encrypt(X2,X3)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_forwards_secure_5) ).
fof(f5,axiom,
party_of_protocol(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_is_party_of_protocol_8) ).
fof(f6,axiom,
fresh_to_b(an_a_nonce),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nonce_a_is_fresh_to_b_9) ).
fof(f7,axiom,
! [X0,X1] :
( ~ message(sent(X1,b,pair(X1,X0)))
| ~ fresh_to_b(X0)
| message(sent(b,t,triple(b,generate_b_nonce(X0),encrypt(triple(X1,X0,generate_expiration_time(X0)),bt)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_creates_freash_nonces_in_time_10) ).
fof(f8,axiom,
t_holds(key(at,a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_holds_key_at_for_a_13) ).
fof(f9,axiom,
t_holds(key(bt,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_holds_key_bt_for_b_14) ).
fof(f10,axiom,
party_of_protocol(t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_is_party_of_protocol_15) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ t_holds(key(X5,X1))
| ~ t_holds(key(X4,X0))
| ~ message(sent(X1,t,triple(X1,X6,encrypt(triple(X0,X2,X3),X5))))
| ~ a_nonce(X2)
| message(sent(t,X0,triple(encrypt(quadruple(X1,X2,generate_key(X2),X3),X4),encrypt(triple(X0,generate_key(X2),X3),X5),X6))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',server_t_generates_key_16) ).
fof(f12,axiom,
! [X2,X0,X1] :
( ~ message(sent(X1,X2,X0))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_can_record_17) ).
fof(f13,axiom,
! [X0,X1] :
( ~ intruder_message(pair(X0,X1))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_pairs_18) ).
fof(f14,axiom,
! [X0,X1] :
( ~ intruder_message(pair(X1,X0))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_pairs_19) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ~ intruder_message(triple(X0,X1,X2))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_triples_20) ).
fof(f16,axiom,
! [X2,X0,X1] :
( ~ intruder_message(triple(X1,X0,X2))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_triples_21) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ intruder_message(triple(X1,X2,X0))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_triples_22) ).
fof(f18,axiom,
! [X2,X3,X0,X1] :
( ~ intruder_message(quadruple(X0,X1,X2,X3))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_quadruples_23) ).
fof(f19,axiom,
! [X2,X3,X0,X1] :
( ~ intruder_message(quadruple(X1,X0,X2,X3))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_quadruples_24) ).
fof(f20,axiom,
! [X2,X3,X0,X1] :
( ~ intruder_message(quadruple(X1,X2,X0,X3))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_quadruples_25) ).
fof(f21,axiom,
! [X2,X3,X0,X1] :
( ~ intruder_message(quadruple(X1,X2,X3,X0))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_decomposes_quadruples_26) ).
fof(f22,axiom,
! [X0,X1] :
( ~ intruder_message(X0)
| ~ intruder_message(X1)
| intruder_message(pair(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_composes_pairs_27) ).
fof(f23,axiom,
! [X2,X0,X1] :
( ~ intruder_message(X0)
| ~ intruder_message(X1)
| ~ intruder_message(X2)
| intruder_message(triple(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_composes_triples_28) ).
fof(f24,axiom,
! [X2,X3,X0,X1] :
( ~ intruder_message(X0)
| ~ intruder_message(X1)
| ~ intruder_message(X2)
| ~ intruder_message(X3)
| intruder_message(quadruple(X0,X1,X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_composes_quadruples_29) ).
fof(f25,axiom,
! [X2,X0,X1] :
( ~ party_of_protocol(X1)
| ~ intruder_message(encrypt(X2,X0))
| ~ intruder_holds(key(X0,X1))
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_interception_30) ).
fof(f26,axiom,
! [X2,X0,X1] :
( ~ party_of_protocol(X0)
| ~ party_of_protocol(X1)
| ~ intruder_message(X2)
| message(sent(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_message_sent_31) ).
fof(f27,axiom,
! [X0,X1] :
( ~ party_of_protocol(X1)
| ~ intruder_message(X0)
| intruder_holds(key(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_holds_key_32) ).
fof(f28,axiom,
! [X2,X0,X1] :
( ~ party_of_protocol(X2)
| ~ intruder_message(X0)
| ~ intruder_holds(key(X1,X2))
| intruder_message(encrypt(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_key_encrypts_33) ).
fof(f29,axiom,
a_nonce(an_a_nonce),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_a_nonce_is_a_nonce_34) ).
fof(f30,axiom,
! [X0] : a_nonce(generate_expiration_time(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',generated_times_and_nonces_are_nonces_36) ).
fof(f31,axiom,
! [X0] : a_nonce(generate_b_nonce(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',generated_times_and_nonces_are_nonces_37) ).
fof(f32,axiom,
! [X0] :
( ~ a_nonce(X0)
| ~ a_key(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_is_a_nonce_and_a_key_38) ).
fof(f33,axiom,
! [X0] : a_key(generate_key(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',generated_keys_are_keys_39) ).
fof(f34,axiom,
fresh_intruder_nonce(an_intruder_nonce),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_intruder_nonce_is_a_fresh_intruder_nonce_40) ).
fof(f35,axiom,
! [X0] :
( ~ fresh_intruder_nonce(X0)
| fresh_intruder_nonce(generate_intruder_nonce(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',can_generate_more_fresh_intruder_nonces_41) ).
fof(f36,axiom,
! [X0] :
( ~ fresh_intruder_nonce(X0)
| fresh_to_b(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fresh_intruder_nonces_are_fresh_to_b_42) ).
fof(f37,axiom,
! [X0] :
( ~ fresh_intruder_nonce(X0)
| intruder_message(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fresh_intruder_nonces_are_fresh_to_b_43) ).
tcf(c_86,plain,
party_of_protocol(a),
inference(cnf_transformation,[],[f1]) ).
tcf(c_87,plain,
message(sent(a,b,pair(a,an_a_nonce))),
inference(cnf_transformation,[],[f2]) ).
tcf(c_88,plain,
a_stored(pair(b,an_a_nonce)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(a,X0,pair(X4,encrypt(X5,X2))))
| ~ a_stored(pair(X0,X1))
| ~ message(sent(t,a,triple(encrypt(quadruple(X0,X1,X2,X3),at),X4,X5))) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_90,plain,
party_of_protocol(b),
inference(cnf_transformation,[],[f5]) ).
tcf(c_91,plain,
fresh_to_b(an_a_nonce),
inference(cnf_transformation,[],[f6]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt))))
| ~ fresh_to_b(X1)
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_93,plain,
t_holds(key(at,a)),
inference(cnf_transformation,[],[f8]) ).
tcf(c_94,plain,
t_holds(key(bt,b)),
inference(cnf_transformation,[],[f9]) ).
tcf(c_95,plain,
party_of_protocol(t),
inference(cnf_transformation,[],[f10]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1)))
| ~ a_nonce(X3)
| ~ t_holds(key(X6,X2))
| ~ t_holds(key(X5,X0))
| ~ message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(X2)
| ~ message(sent(X0,X1,X2)) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] :
( intruder_message(X0)
| ~ intruder_message(pair(X0,X1)) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] :
( intruder_message(X1)
| ~ intruder_message(pair(X0,X1)) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(X0)
| ~ intruder_message(triple(X0,X1,X2)) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(X1)
| ~ intruder_message(triple(X0,X1,X2)) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(X2)
| ~ intruder_message(triple(X0,X1,X2)) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( intruder_message(X0)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( intruder_message(X1)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( intruder_message(X2)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( intruder_message(X3)
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] :
( intruder_message(pair(X0,X1))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(triple(X0,X1,X2))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( intruder_message(quadruple(X0,X1,X2,X3))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(X1)
| ~ party_of_protocol(X2)
| ~ intruder_holds(key(X1,X2))
| ~ intruder_message(encrypt(X0,X1)) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(X0,X1,X2))
| ~ intruder_message(X2)
| ~ party_of_protocol(X1)
| ~ party_of_protocol(X0) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( intruder_holds(key(X1,X0))
| ~ intruder_message(X1)
| ~ party_of_protocol(X0) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(X2,X0))
| ~ intruder_message(X2)
| ~ party_of_protocol(X1)
| ~ intruder_holds(key(X0,X1)) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_114,plain,
a_nonce(an_a_nonce),
inference(cnf_transformation,[],[f29]) ).
tcf(c_115,plain,
! [X0: $i] : a_nonce(generate_expiration_time(X0)),
inference(cnf_transformation,[],[f30]) ).
tcf(c_116,plain,
! [X0: $i] : a_nonce(generate_b_nonce(X0)),
inference(cnf_transformation,[],[f31]) ).
tcf(c_117,plain,
! [X0: $i] :
( ~ a_key(X0)
| ~ a_nonce(X0) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_118,plain,
! [X0: $i] : a_key(generate_key(X0)),
inference(cnf_transformation,[],[f33]) ).
tcf(c_119,plain,
fresh_intruder_nonce(an_intruder_nonce),
inference(cnf_transformation,[],[f34]) ).
tcf(c_120,plain,
! [X0: $i] :
( fresh_intruder_nonce(generate_intruder_nonce(X0))
| ~ fresh_intruder_nonce(X0) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_121,plain,
! [X0: $i] :
( fresh_to_b(X0)
| ~ fresh_intruder_nonce(X0) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_122,plain,
! [X0: $i] :
( intruder_message(X0)
| ~ fresh_intruder_nonce(X0) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_150,plain,
! [X0: $i] :
( message(sent(b,t,triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(X0,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))))
| ~ fresh_to_b(an_a_nonce)
| ~ message(sent(X0,b,pair(X0,an_a_nonce))) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_183,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))))
| ~ fresh_to_b(an_a_nonce)
| ~ message(sent(a,b,pair(a,an_a_nonce))) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_227,plain,
( intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))
| ~ 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(instantiation,[status(thm)],[c_97]) ).
tcf(c_324,plain,
( intruder_message(b)
| ~ intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_438,plain,
fresh_to_b(an_intruder_nonce),
inference(superposition,[status(thm)],[c_119,c_121]) ).
tcf(c_451,plain,
intruder_message(an_intruder_nonce),
inference(superposition,[status(thm)],[c_119,c_122]) ).
tcf(c_531,plain,
! [X0: $i] : ~ a_nonce(generate_key(X0)),
inference(superposition,[status(thm)],[c_118,c_117]) ).
tcf(c_542,plain,
! [X0: $i] :
( intruder_message(generate_intruder_nonce(X0))
| ~ fresh_intruder_nonce(X0) ),
inference(superposition,[status(thm)],[c_120,c_122]) ).
tcf(c_543,plain,
! [X0: $i] :
( fresh_to_b(generate_intruder_nonce(X0))
| ~ fresh_intruder_nonce(X0) ),
inference(superposition,[status(thm)],[c_120,c_121]) ).
tcf(c_601,plain,
intruder_message(pair(a,an_a_nonce)),
inference(superposition,[status(thm)],[c_87,c_97]) ).
tcf(c_632,plain,
intruder_message(an_a_nonce),
inference(superposition,[status(thm)],[c_601,c_99]) ).
tcf(c_633,plain,
intruder_message(a),
inference(superposition,[status(thm)],[c_601,c_98]) ).
tcf(c_783,plain,
! [X0: $i,X1: $i] :
( message(sent(a,X0,X1))
| ~ intruder_message(X1)
| ~ party_of_protocol(X0) ),
inference(superposition,[status(thm)],[c_86,c_111]) ).
tcf(c_784,plain,
! [X0: $i,X1: $i] :
( message(sent(b,X0,X1))
| ~ intruder_message(X1)
| ~ party_of_protocol(X0) ),
inference(superposition,[status(thm)],[c_90,c_111]) ).
tcf(c_785,plain,
! [X0: $i,X1: $i] :
( message(sent(t,X0,X1))
| ~ intruder_message(X1)
| ~ party_of_protocol(X0) ),
inference(superposition,[status(thm)],[c_95,c_111]) ).
tcf(c_888,plain,
! [X0: $i] :
( message(sent(a,a,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_86,c_783]) ).
tcf(c_889,plain,
! [X0: $i] :
( message(sent(a,b,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_90,c_783]) ).
tcf(c_890,plain,
! [X0: $i] :
( message(sent(a,t,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_95,c_783]) ).
tcf(c_1026,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(X2,X1))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ party_of_protocol(X0) ),
inference(superposition,[status(thm)],[c_112,c_113]) ).
tcf(c_1063,plain,
! [X0: $i] :
( message(sent(b,a,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_86,c_784]) ).
tcf(c_1064,plain,
! [X0: $i] :
( message(sent(b,b,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_90,c_784]) ).
tcf(c_1065,plain,
! [X0: $i] :
( message(sent(b,t,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_95,c_784]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i] :
( intruder_message(triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))
| ~ fresh_to_b(X1)
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_92,c_97]) ).
tcf(c_1219,plain,
! [X0: $i] :
( message(sent(t,a,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_86,c_785]) ).
tcf(c_1220,plain,
! [X0: $i] :
( message(sent(t,b,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_90,c_785]) ).
tcf(c_1221,plain,
! [X0: $i] :
( message(sent(t,t,X0))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_95,c_785]) ).
tcf(c_1313,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(a,X0,pair(X4,encrypt(X5,X2))))
| ~ a_stored(pair(X0,X1))
| ~ intruder_message(triple(encrypt(quadruple(X0,X1,X2,X3),at),X4,X5)) ),
inference(superposition,[status(thm)],[c_1219,c_89]) ).
tcf(c_1393,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,X0,triple(encrypt(quadruple(b,X1,generate_key(X1),generate_expiration_time(X1)),X2),encrypt(triple(X0,generate_key(X1),generate_expiration_time(X1)),bt),generate_b_nonce(X1))))
| ~ a_nonce(X1)
| ~ fresh_to_b(X1)
| ~ t_holds(key(bt,b))
| ~ t_holds(key(X2,X0))
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_92,c_96]) ).
tcf(c_1394,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(t,X1,triple(encrypt(quadruple(a,X2,generate_key(X2),X3),X5),encrypt(triple(X1,generate_key(X2),X3),X4),X0)))
| ~ a_nonce(X2)
| ~ t_holds(key(X4,a))
| ~ t_holds(key(X5,X1))
| ~ intruder_message(triple(a,X0,encrypt(triple(X1,X2,X3),X4))) ),
inference(superposition,[status(thm)],[c_890,c_96]) ).
tcf(c_1395,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(t,X1,triple(encrypt(quadruple(b,X2,generate_key(X2),X3),X5),encrypt(triple(X1,generate_key(X2),X3),X4),X0)))
| ~ a_nonce(X2)
| ~ t_holds(key(X4,b))
| ~ t_holds(key(X5,X1))
| ~ intruder_message(triple(b,X0,encrypt(triple(X1,X2,X3),X4))) ),
inference(superposition,[status(thm)],[c_1065,c_96]) ).
tcf(c_1406,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,X0,triple(encrypt(quadruple(b,X1,generate_key(X1),generate_expiration_time(X1)),X2),encrypt(triple(X0,generate_key(X1),generate_expiration_time(X1)),bt),generate_b_nonce(X1))))
| ~ a_nonce(X1)
| ~ fresh_to_b(X1)
| ~ t_holds(key(X2,X0))
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1393,c_94]) ).
tcf(c_1457,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(t,X1,triple(encrypt(quadruple(t,X2,generate_key(X2),X3),X5),encrypt(triple(X1,generate_key(X2),X3),X4),X0)))
| ~ a_nonce(X2)
| ~ t_holds(key(X4,t))
| ~ t_holds(key(X5,X1))
| ~ intruder_message(triple(t,X0,encrypt(triple(X1,X2,X3),X4))) ),
inference(superposition,[status(thm)],[c_1221,c_96]) ).
tcf(c_1674,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(X1,X0))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_86,c_1026]) ).
tcf(c_1725,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(X0,X1,generate_expiration_time(X1)),bt))
| ~ fresh_to_b(X1)
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_1184,c_102]) ).
tcf(c_1726,plain,
! [X0: $i,X1: $i] :
( intruder_message(generate_b_nonce(X1))
| ~ fresh_to_b(X1)
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_1184,c_101]) ).
tcf(c_1727,plain,
! [X0: $i,X1: $i] :
( intruder_message(b)
| ~ fresh_to_b(X1)
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_1184,c_100]) ).
tcf(c_1843,plain,
intruder_message(b),
inference(global_subsumption_just,[status(thm)],[c_1727,c_91,c_87,c_183,c_227,c_324]) ).
tcf(c_1883,plain,
( intruder_message(generate_b_nonce(an_a_nonce))
| ~ fresh_to_b(an_a_nonce) ),
inference(superposition,[status(thm)],[c_87,c_1726]) ).
tcf(c_1884,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(X0))
| ~ fresh_to_b(X0)
| ~ intruder_message(pair(a,X0)) ),
inference(superposition,[status(thm)],[c_889,c_1726]) ).
tcf(c_1885,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(X0))
| ~ fresh_to_b(X0)
| ~ intruder_message(pair(b,X0)) ),
inference(superposition,[status(thm)],[c_1064,c_1726]) ).
tcf(c_1886,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(X0))
| ~ fresh_to_b(X0)
| ~ intruder_message(pair(t,X0)) ),
inference(superposition,[status(thm)],[c_1220,c_1726]) ).
tcf(c_1887,plain,
intruder_message(generate_b_nonce(an_a_nonce)),
inference(forward_subsumption_resolution,[status(thm)],[c_1883,c_91]) ).
tcf(c_1950,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(X0))
| ~ intruder_message(a)
| ~ intruder_message(X0)
| ~ fresh_to_b(X0) ),
inference(superposition,[status(thm)],[c_107,c_1884]) ).
tcf(c_1952,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(X0))
| ~ intruder_message(X0)
| ~ fresh_to_b(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1950,c_633]) ).
tcf(c_2044,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(bt)
| ~ fresh_to_b(X1)
| ~ party_of_protocol(X2)
| ~ intruder_holds(key(bt,X2))
| ~ message(sent(X0,b,pair(X0,X1))) ),
inference(superposition,[status(thm)],[c_1725,c_110]) ).
tcf(c_2081,plain,
! [X0: $i] :
( intruder_message(bt)
| ~ fresh_to_b(an_a_nonce)
| ~ party_of_protocol(X0)
| ~ intruder_holds(key(bt,X0)) ),
inference(superposition,[status(thm)],[c_87,c_2044]) ).
tcf(c_2085,plain,
! [X0: $i] :
( intruder_message(bt)
| ~ party_of_protocol(X0)
| ~ intruder_holds(key(bt,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2081,c_91]) ).
tcf(c_2160,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(a,X0,pair(X4,encrypt(X5,X2))))
| ~ intruder_message(X5)
| ~ intruder_message(X4)
| ~ a_stored(pair(X0,X1))
| ~ intruder_message(encrypt(quadruple(X0,X1,X2,X3),at)) ),
inference(superposition,[status(thm)],[c_108,c_1313]) ).
tcf(c_2189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(a,X0,pair(X4,encrypt(X5,X2))))
| ~ intruder_message(at)
| ~ intruder_message(X5)
| ~ intruder_message(X4)
| ~ a_stored(pair(X0,X1))
| ~ intruder_message(quadruple(X0,X1,X2,X3)) ),
inference(superposition,[status(thm)],[c_1674,c_2160]) ).
tcf(c_2224,plain,
! [X0: $i] :
( message(sent(t,a,triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),at),encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0))))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_93,c_1406]) ).
tcf(c_2225,plain,
! [X0: $i] :
( message(sent(t,b,triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(triple(b,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0))))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(b,b,pair(b,X0))) ),
inference(superposition,[status(thm)],[c_94,c_1406]) ).
tcf(c_2359,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( message(sent(a,X0,pair(X4,encrypt(X5,X2))))
| ~ intruder_message(at)
| ~ intruder_message(X5)
| ~ intruder_message(X4)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ a_stored(pair(X0,X1)) ),
inference(superposition,[status(thm)],[c_109,c_2189]) ).
tcf(c_2410,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,b,pair(X2,encrypt(X3,X0))))
| ~ intruder_message(at)
| ~ intruder_message(an_a_nonce)
| ~ intruder_message(b)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_88,c_2359]) ).
tcf(c_2411,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,b,pair(X2,encrypt(X3,X0))))
| ~ intruder_message(at)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2410,c_632,c_1843]) ).
tcf(c_2460,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(a,b,pair(X1,encrypt(X2,X0))))
| ~ intruder_message(at)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_1843,c_2411]) ).
tcf(c_2575,plain,
! [X0: $i] :
( message(sent(a,b,pair(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(generate_b_nonce(X0),generate_key(X0)))))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ a_stored(pair(b,X0))
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2224,c_89]) ).
tcf(c_2576,plain,
! [X0: $i] :
( intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),at),encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0)))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2224,c_97]) ).
tcf(c_2679,plain,
! [X0: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2576,c_101]) ).
tcf(c_2680,plain,
! [X0: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),at))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2576,c_100]) ).
tcf(c_2760,plain,
! [X0: $i,X1: $i] :
( intruder_message(at)
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ party_of_protocol(X1)
| ~ intruder_holds(key(at,X1))
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2680,c_110]) ).
tcf(c_2761,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(a,b,pair(X1,encrypt(X2,generate_key(X0)))))
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ a_stored(pair(b,X0))
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2680,c_2160]) ).
tcf(c_2812,plain,
! [X0: $i] :
( intruder_message(at)
| ~ a_nonce(an_a_nonce)
| ~ fresh_to_b(an_a_nonce)
| ~ party_of_protocol(X0)
| ~ intruder_holds(key(at,X0)) ),
inference(superposition,[status(thm)],[c_87,c_2760]) ).
tcf(c_2814,plain,
! [X0: $i] :
( intruder_message(at)
| ~ party_of_protocol(X0)
| ~ intruder_holds(key(at,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2812,c_114,c_91]) ).
tcf(c_2871,plain,
! [X0: $i,X1: $i] :
( message(sent(a,b,pair(X0,encrypt(X1,generate_key(an_a_nonce)))))
| ~ a_nonce(an_a_nonce)
| ~ fresh_to_b(an_a_nonce)
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ message(sent(a,b,pair(a,an_a_nonce))) ),
inference(superposition,[status(thm)],[c_88,c_2761]) ).
tcf(c_2872,plain,
! [X0: $i,X1: $i] :
( message(sent(a,b,pair(X0,encrypt(X1,generate_key(an_a_nonce)))))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2871,c_114,c_91,c_87]) ).
tcf(c_2902,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(a)
| ~ intruder_message(X0)
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce))) ),
inference(superposition,[status(thm)],[c_2872,c_1726]) ).
tcf(c_2903,plain,
! [X0: $i,X1: $i] :
( intruder_message(pair(X0,encrypt(X1,generate_key(an_a_nonce))))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_2872,c_97]) ).
tcf(c_2907,plain,
! [X0: $i] :
( intruder_message(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0)
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2902,c_633]) ).
tcf(c_2934,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(X1,generate_key(an_a_nonce)))
| ~ intruder_message(X1)
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_2903,c_99]) ).
tcf(c_3019,plain,
! [X0: $i] :
( intruder_message(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(X0) ),
inference(superposition,[status(thm)],[c_1843,c_2934]) ).
tcf(c_3194,plain,
! [X0: $i] :
( intruder_message(pair(encrypt(triple(a,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(generate_b_nonce(X0),generate_key(X0))))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ a_stored(pair(b,X0))
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_2575,c_97]) ).
tcf(c_3229,plain,
! [X0: $i] :
( intruder_message(encrypt(generate_b_nonce(X0),generate_key(X0)))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ a_stored(pair(b,X0))
| ~ message(sent(a,b,pair(a,X0))) ),
inference(superposition,[status(thm)],[c_3194,c_99]) ).
tcf(c_3286,plain,
( intruder_message(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce)))
| ~ a_nonce(an_a_nonce)
| ~ fresh_to_b(an_a_nonce)
| ~ a_stored(pair(b,an_a_nonce)) ),
inference(superposition,[status(thm)],[c_87,c_3229]) ).
tcf(c_3287,plain,
! [X0: $i] :
( intruder_message(encrypt(generate_b_nonce(X0),generate_key(X0)))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ intruder_message(pair(a,X0))
| ~ a_stored(pair(b,X0)) ),
inference(superposition,[status(thm)],[c_889,c_3229]) ).
tcf(c_3288,plain,
! [X0: $i] :
( intruder_message(encrypt(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),generate_key(encrypt(X0,generate_key(an_a_nonce)))))
| ~ intruder_message(a)
| ~ intruder_message(X0)
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce)))) ),
inference(superposition,[status(thm)],[c_2872,c_3229]) ).
tcf(c_3289,plain,
intruder_message(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))),
inference(forward_subsumption_resolution,[status(thm)],[c_3286,c_114,c_91,c_88]) ).
tcf(c_3295,plain,
! [X0: $i] :
( intruder_message(encrypt(generate_b_nonce(encrypt(X0,generate_key(an_a_nonce))),generate_key(encrypt(X0,generate_key(an_a_nonce)))))
| ~ intruder_message(X0)
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3288,c_633]) ).
tcf(c_3415,plain,
! [X0: $i] :
( intruder_message(generate_key(an_a_nonce))
| ~ party_of_protocol(X0)
| ~ intruder_holds(key(generate_key(an_a_nonce),X0)) ),
inference(superposition,[status(thm)],[c_3289,c_110]) ).
tcf(c_3448,plain,
! [X0: $i,X1: $i] :
( intruder_message(generate_key(X0))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ party_of_protocol(X1)
| ~ intruder_message(pair(a,X0))
| ~ a_stored(pair(b,X0))
| ~ intruder_holds(key(generate_key(X0),X1)) ),
inference(superposition,[status(thm)],[c_3287,c_110]) ).
tcf(c_3519,plain,
! [X0: $i,X1: $i] :
( intruder_message(generate_key(encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(X0)
| ~ party_of_protocol(X1)
| ~ a_nonce(encrypt(X0,generate_key(an_a_nonce)))
| ~ fresh_to_b(encrypt(X0,generate_key(an_a_nonce)))
| ~ a_stored(pair(b,encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_holds(key(generate_key(encrypt(X0,generate_key(an_a_nonce))),X1)) ),
inference(superposition,[status(thm)],[c_3295,c_110]) ).
tcf(c_3554,plain,
! [X0: $i] :
( intruder_message(triple(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),bt),encrypt(triple(b,generate_key(X0),generate_expiration_time(X0)),bt),generate_b_nonce(X0)))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(b,b,pair(b,X0))) ),
inference(superposition,[status(thm)],[c_2225,c_97]) ).
tcf(c_3582,plain,
! [X0: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),generate_expiration_time(X0)),bt))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(b,b,pair(b,X0))) ),
inference(superposition,[status(thm)],[c_3554,c_101]) ).
tcf(c_3583,plain,
! [X0: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),generate_expiration_time(X0)),bt))
| ~ a_nonce(X0)
| ~ fresh_to_b(X0)
| ~ message(sent(b,b,pair(b,X0))) ),
inference(superposition,[status(thm)],[c_3554,c_100]) ).
tcf(c_3783,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( message(sent(t,X1,triple(encrypt(quadruple(a,X2,generate_key(X2),X3),X4),encrypt(triple(X1,generate_key(X2),X3),at),X0)))
| ~ a_nonce(X2)
| ~ t_holds(key(X4,X1))
| ~ intruder_message(triple(a,X0,encrypt(triple(X1,X2,X3),at))) ),
inference(superposition,[status(thm)],[c_93,c_1394]) ).
tcf(c_3812,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,a,triple(encrypt(quadruple(a,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),at),X0)))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(a,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_93,c_3783]) ).
tcf(c_3813,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,b,triple(encrypt(quadruple(a,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),at),X0)))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(b,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_94,c_3783]) ).
tcf(c_3844,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(a,a,pair(encrypt(triple(a,generate_key(X1),X2),at),encrypt(X0,generate_key(X1)))))
| ~ a_nonce(X1)
| ~ a_stored(pair(a,X1))
| ~ intruder_message(triple(a,X0,encrypt(triple(a,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_3812,c_89]) ).
tcf(c_3845,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(triple(encrypt(quadruple(a,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),at),X0))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(a,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_3812,c_97]) ).
tcf(c_3877,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X1),X2),at))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(a,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_3845,c_101]) ).
tcf(c_3878,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X1,generate_key(X1),X2),at))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(a,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_3845,c_100]) ).
tcf(c_3963,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),at))
| ~ intruder_message(a)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_108,c_3877]) ).
tcf(c_3964,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),at))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3963,c_633]) ).
tcf(c_4021,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),at))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_3289,c_3964]) ).
tcf(c_4067,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),at))
| ~ intruder_message(a)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_108,c_3878]) ).
tcf(c_4068,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),at))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4067,c_633]) ).
tcf(c_4110,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),at))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_3289,c_4068]) ).
tcf(c_4130,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(triple(encrypt(quadruple(a,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),at),X0))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(b,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_3813,c_97]) ).
tcf(c_4166,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,a,pair(X2,encrypt(X3,generate_key(X0)))))
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ a_stored(pair(a,X0))
| ~ intruder_message(encrypt(triple(a,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_4110,c_2160]) ).
tcf(c_4675,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X1),X2),at))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(b,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_4130,c_101]) ).
tcf(c_4676,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X1,generate_key(X1),X2),bt))
| ~ a_nonce(X1)
| ~ intruder_message(triple(a,X0,encrypt(triple(b,X1,X2),at))) ),
inference(superposition,[status(thm)],[c_4130,c_100]) ).
tcf(c_4735,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),at))
| ~ intruder_message(a)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_108,c_4675]) ).
tcf(c_4736,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),at))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4735,c_633]) ).
tcf(c_4799,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),at))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_3289,c_4736]) ).
tcf(c_4821,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),bt))
| ~ intruder_message(a)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_108,c_4676]) ).
tcf(c_4822,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),bt))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4821,c_633]) ).
tcf(c_4871,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(quadruple(a,X0,generate_key(X0),X1),bt))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),at)) ),
inference(superposition,[status(thm)],[c_3289,c_4822]) ).
tcf(c_4945,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,a,pair(X2,encrypt(X3,generate_key(X0)))))
| ~ intruder_message(at)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ a_stored(pair(a,X0))
| ~ intruder_message(triple(a,X0,X1)) ),
inference(superposition,[status(thm)],[c_1674,c_4166]) ).
tcf(c_4968,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,a,pair(X2,encrypt(X3,generate_key(X0)))))
| ~ intruder_message(at)
| ~ intruder_message(a)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ a_nonce(X0)
| ~ a_stored(pair(a,X0)) ),
inference(superposition,[status(thm)],[c_108,c_4945]) ).
tcf(c_4969,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(a,a,pair(X2,encrypt(X3,generate_key(X0)))))
| ~ intruder_message(at)
| ~ intruder_message(X3)
| ~ intruder_message(X2)
| ~ intruder_message(X1)
| ~ intruder_message(X0)
| ~ a_nonce(X0)
| ~ a_stored(pair(a,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4968,c_633]) ).
tcf(c_5026,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(t,a,triple(encrypt(quadruple(b,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),X3),X0)))
| ~ a_nonce(X1)
| ~ t_holds(key(X3,b))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_93,c_1395]) ).
tcf(c_5027,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(t,b,triple(encrypt(quadruple(b,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),X3),X0)))
| ~ a_nonce(X1)
| ~ t_holds(key(X3,b))
| ~ intruder_message(triple(b,X0,encrypt(triple(b,X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_94,c_1395]) ).
tcf(c_5062,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,a,triple(encrypt(quadruple(b,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),bt),X0)))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_94,c_5026]) ).
tcf(c_5123,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(a,b,pair(encrypt(triple(a,generate_key(X1),X2),bt),encrypt(X0,generate_key(X1)))))
| ~ a_nonce(X1)
| ~ a_stored(pair(b,X1))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_5062,c_89]) ).
tcf(c_5124,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(triple(encrypt(quadruple(b,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),bt),X0))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_5062,c_97]) ).
tcf(c_5290,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X1),X2),bt))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_5124,c_101]) ).
tcf(c_5291,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X1,generate_key(X1),X2),at))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(a,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_5124,c_100]) ).
tcf(c_5413,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),bt))
| ~ intruder_message(b)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_108,c_5290]) ).
tcf(c_5415,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),bt))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),bt)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5413,c_1843]) ).
tcf(c_5451,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(a,generate_key(X0),X1),bt))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_3289,c_5415]) ).
tcf(c_5489,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),at))
| ~ intruder_message(b)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_108,c_5291]) ).
tcf(c_5491,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),at))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(a,X0,X1),bt)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5489,c_1843]) ).
tcf(c_5533,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),at))
| ~ intruder_message(bt)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(triple(a,X0,X1)) ),
inference(superposition,[status(thm)],[c_1674,c_5491]) ).
tcf(c_5556,plain,
! [X0: $i,X1: $i] :
( message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),X1),bt),encrypt(X0,generate_key(an_a_nonce)))))
| ~ a_nonce(an_a_nonce)
| ~ intruder_message(triple(b,X0,encrypt(triple(a,an_a_nonce,X1),bt))) ),
inference(superposition,[status(thm)],[c_88,c_5123]) ).
tcf(c_5557,plain,
! [X0: $i,X1: $i] :
( message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),X1),bt),encrypt(X0,generate_key(an_a_nonce)))))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,an_a_nonce,X1),bt))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5556,c_114]) ).
tcf(c_5619,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),at))
| ~ intruder_message(bt)
| ~ a_nonce(X0)
| ~ intruder_message(triple(a,X0,X1)) ),
inference(superposition,[status(thm)],[c_3289,c_5533]) ).
tcf(c_5689,plain,
! [X0: $i,X1: $i] :
( intruder_message(pair(encrypt(triple(a,generate_key(an_a_nonce),X1),bt),encrypt(X0,generate_key(an_a_nonce))))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,an_a_nonce,X1),bt))) ),
inference(superposition,[status(thm)],[c_5557,c_97]) ).
tcf(c_5697,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(X0,generate_key(an_a_nonce)))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,an_a_nonce,X1),bt))) ),
inference(superposition,[status(thm)],[c_5689,c_99]) ).
tcf(c_5698,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(a,generate_key(an_a_nonce),X1),bt))
| ~ intruder_message(triple(b,X0,encrypt(triple(a,an_a_nonce,X1),bt))) ),
inference(superposition,[status(thm)],[c_5689,c_98]) ).
tcf(c_5906,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(a,generate_key(an_a_nonce),X0),bt))
| ~ intruder_message(b)
| ~ intruder_message(X1)
| ~ intruder_message(encrypt(triple(a,an_a_nonce,X0),bt)) ),
inference(superposition,[status(thm)],[c_108,c_5698]) ).
tcf(c_5907,plain,
( intruder_message(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt))
| ~ fresh_to_b(an_a_nonce)
| ~ message(sent(a,b,pair(a,an_a_nonce))) ),
inference(superposition,[status(thm)],[c_1184,c_5698]) ).
tcf(c_5908,plain,
intruder_message(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)),
inference(forward_subsumption_resolution,[status(thm)],[c_5907,c_91,c_87]) ).
tcf(c_5909,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(a,generate_key(an_a_nonce),X0),bt))
| ~ intruder_message(X1)
| ~ intruder_message(encrypt(triple(a,an_a_nonce,X0),bt)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5906,c_1843]) ).
tcf(c_5982,plain,
! [X0: $i] :
( intruder_message(encrypt(triple(a,generate_key(an_a_nonce),X0),bt))
| ~ intruder_message(encrypt(triple(a,an_a_nonce,X0),bt)) ),
inference(superposition,[status(thm)],[c_5908,c_5909]) ).
tcf(c_6006,plain,
! [X0: $i,X1: $i,X2: $i] :
( message(sent(t,b,triple(encrypt(quadruple(b,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),bt),X0)))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(b,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_94,c_5027]) ).
tcf(c_6026,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(triple(encrypt(quadruple(b,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),bt),X0))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(b,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_6006,c_97]) ).
tcf(c_6038,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X1),X2),bt))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(b,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_6026,c_101]) ).
tcf(c_6039,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X1,generate_key(X1),X2),bt))
| ~ a_nonce(X1)
| ~ intruder_message(triple(b,X0,encrypt(triple(b,X1,X2),bt))) ),
inference(superposition,[status(thm)],[c_6026,c_100]) ).
tcf(c_6077,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),bt))
| ~ intruder_message(b)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_108,c_6038]) ).
tcf(c_6079,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),bt))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6077,c_1843]) ).
tcf(c_6141,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(triple(b,generate_key(X0),X1),bt))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_5908,c_6079]) ).
tcf(c_6241,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),bt))
| ~ intruder_message(b)
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_108,c_6039]) ).
tcf(c_6243,plain,
! [X0: $i,X1: $i,X2: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),bt))
| ~ intruder_message(X2)
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6241,c_1843]) ).
tcf(c_6306,plain,
! [X0: $i,X1: $i] :
( intruder_message(encrypt(quadruple(b,X0,generate_key(X0),X1),bt))
| ~ a_nonce(X0)
| ~ intruder_message(encrypt(triple(b,X0,X1),bt)) ),
inference(superposition,[status(thm)],[c_5908,c_6243]) ).
tcf(c_6333,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(t,a,triple(encrypt(quadruple(t,X1,generate_key(X1),X2),at),encrypt(triple(a,generate_key(X1),X2),X3),X0)))
| ~ a_nonce(X1)
| ~ t_holds(key(X3,t))
| ~ intruder_message(triple(t,X0,encrypt(triple(a,X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_93,c_1457]) ).
tcf(c_6334,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( message(sent(t,b,triple(encrypt(quadruple(t,X1,generate_key(X1),X2),bt),encrypt(triple(b,generate_key(X1),X2),X3),X0)))
| ~ a_nonce(X1)
| ~ t_holds(key(X3,t))
| ~ intruder_message(triple(t,X0,encrypt(triple(b,X1,X2),X3))) ),
inference(superposition,[status(thm)],[c_94,c_1457]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV017-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 18:20:36 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.10/0.40 Running model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fnt_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 3.81/1.27 % SZS status Started for theBenchmark.p
% 3.81/1.27 % SZS status Satisfiable for theBenchmark.p
% 3.81/1.27
% 3.81/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.81/1.27
% 3.81/1.27 ------ iProver source info
% 3.81/1.27
% 3.81/1.27 git: date: 2026-07-19 20:42:38 +0200
% 3.81/1.27 git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.81/1.27 git: non_committed_changes: false
% 3.81/1.27
% 3.81/1.27 ------ Parsing...successful
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27 ------ Clausification by vclausify_rel & Parsing by iProver...
% 3.81/1.27 ------ Proving...
% 3.81/1.27 ------ Problem Properties
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27 clauses 37
% 3.81/1.27 conjectures 0
% 3.81/1.27 EPR 9
% 3.81/1.27 Horn 37
% 3.81/1.27 unary 13
% 3.81/1.27 binary 14
% 3.81/1.27 lits 79
% 3.81/1.27 lits eq 0
% 3.81/1.27 fd_pure 0
% 3.81/1.27 fd_pseudo 0
% 3.81/1.27 fd_cond 0
% 3.81/1.27 fd_pseudo_cond 0
% 3.81/1.27 AC symbols 0
% 3.81/1.27
% 3.81/1.27 ------ Schedule Sat is on
% 3.81/1.27
% 3.81/1.27 ------ no conjectures: strip conj schedule
% 3.81/1.27
% 3.81/1.27 ------ no conjectures: strip conj schedule
% 3.81/1.27
% 3.81/1.27 ------ no equalities: superposition off
% 3.81/1.27
% 3.81/1.27 ------ Input Options sat_mode off stripped conjectures stripped conjectures Time Limit: 30.
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27 ------
% 3.81/1.27 Current options:
% 3.81/1.27 ------
% 3.81/1.27
% 3.81/1.27 ------ Input Options
% 3.81/1.27
% 3.81/1.27 --out_options all
% 3.81/1.27 --tptp_safe_out true
% 3.81/1.27 --problem_path ""
% 3.81/1.27 --include_path ""
% 3.81/1.27 --clausifier res/vclausify_rel
% 3.81/1.27 --clausifier_options --mode clausify -t 101.66 -updr off
% 3.81/1.27 --stdin false
% 3.81/1.27 --proof_out true
% 3.81/1.27 --proof_dot_file ""
% 3.81/1.27 --proof_reduce_dot []
% 3.81/1.27 --suppress_sat_res false
% 3.81/1.27 --suppress_unsat_res true
% 3.81/1.27 --stats_out none
% 3.81/1.27 --stats_mem false
% 3.81/1.27 --theory_stats_out false
% 3.81/1.27
% 3.81/1.27 ------ General Options
% 3.81/1.27
% 3.81/1.27 --fof false
% 3.81/1.27 --time_out_real 304.99
% 3.81/1.27 --time_out_virtual -1.
% 3.81/1.27 --rnd_seed 13
% 3.81/1.27 --symbol_type_check false
% 3.81/1.27 --clausify_out false
% 3.81/1.27 --sig_cnt_out false
% 3.81/1.27 --trig_cnt_out false
% 3.81/1.27 --trig_cnt_out_tolerance 1.
% 3.81/1.27 --trig_cnt_out_sk_spl false
% 3.81/1.27 --abstr_cl_out false
% 3.81/1.27
% 3.81/1.27 ------ Interactive Mode
% 3.81/1.27
% 3.81/1.27 --interactive_mode false
% 3.81/1.27 --external_ip_address ""
% 3.81/1.27 --external_port 0
% 3.81/1.27
% 3.81/1.27 ------ Global Options
% 3.81/1.27
% 3.81/1.27 --schedule sat
% 3.81/1.27 --add_important_lit false
% 3.81/1.27 --prop_solver_per_cl 500
% 3.81/1.27 --subs_bck_mult 8
% 3.81/1.27 --min_unsat_core false
% 3.81/1.27 --soft_assumptions false
% 3.81/1.27 --soft_lemma_size 3
% 3.81/1.27 --prop_impl_unit_size 0
% 3.81/1.27 --prop_impl_unit []
% 3.81/1.27 --share_sel_clauses true
% 3.81/1.27 --reset_solvers false
% 3.81/1.27 --bc_imp_inh [conj_cone]
% 3.81/1.27 --conj_cone_tolerance 3.
% 3.81/1.27 --extra_neg_conj none
% 3.81/1.27 --large_theory_mode true
% 3.81/1.27 --prolific_symb_bound 200
% 3.81/1.27 --lt_threshold 2000
% 3.81/1.27 --clause_weak_htbl true
% 3.81/1.27 --gc_record_bc_elim false
% 3.81/1.27
% 3.81/1.27 ------ Preprocessing Options
% 3.81/1.27
% 3.81/1.27 --preprocessing_flag false
% 3.81/1.27 --time_out_prep_mult 0.1
% 3.81/1.27 --splitting_mode input
% 3.81/1.27 --splitting_grd true
% 3.81/1.27 --splitting_cvd false
% 3.81/1.27 --splitting_cvd_svl false
% 3.81/1.27 --splitting_nvd 32
% 3.81/1.27 --sub_typing false
% 3.81/1.27 --prep_eq_flat_conj false
% 3.81/1.27 --prep_ineq_split false
% 3.81/1.27 --prep_eq_flat_all_gr false
% 3.81/1.27 --prep_gs_sim true
% 3.81/1.27 --prep_unflatten true
% 3.81/1.27 --prep_res_sim true
% 3.81/1.27 --prep_sup_sim_all true
% 3.81/1.27 --prep_sup_sim_sup false
% 3.81/1.27 --prep_upred true
% 3.81/1.27 --prep_well_definedness true
% 3.81/1.27 --prep_sem_filter exhaustive
% 3.81/1.27 --prep_sem_filter_out false
% 3.81/1.27 --pred_elim true
% 3.81/1.27 --res_sim_input true
% 3.81/1.27 --eq_ax_congr_red true
% 3.81/1.27 --pure_diseq_elim true
% 3.81/1.27 --brand_transform false
% 3.81/1.27 --non_eq_to_eq false
% 3.81/1.27 --prep_eq_proxy false
% 3.81/1.27 --prep_def_merge true
% 3.81/1.27 --prep_def_merge_prop_impl false
% 3.81/1.27 --prep_def_merge_mbd true
% 3.81/1.27 --prep_def_merge_tr_red false
% 3.81/1.27 --prep_def_merge_tr_cl false
% 3.81/1.27 --smt_preprocessing false
% 3.81/1.27 --smt_ac_axioms fast
% 3.81/1.27 --preprocessed_out false
% 3.81/1.27 --preprocessed_stats false
% 3.81/1.27
% 3.81/1.27 ------ Abstraction refinement Options
% 3.81/1.27
% 3.81/1.27 --abstr_ref []
% 3.81/1.27 --abstr_ref_prep false
% 3.81/1.27 --abstr_ref_until_sat false
% 3.81/1.27 --abstr_ref_sig_restrict funpre
% 3.81/1.27 --abstr_ref_af_restrict_to_split_sk false
% 3.81/1.27 --abstr_ref_under []
% 3.81/1.27
% 3.81/1.27 ------ SAT Options
% 3.81/1.27
% 3.81/1.27 --sat_mode false
% 3.81/1.27 --sat_fm_restart_options ""
% 3.81/1.27 --sat_gr_def false
% 3.81/1.27 --sat_epr_types true
% 3.81/1.27 --sat_non_cyclic_types false
% 3.81/1.27 --sat_finite_models false
% 3.81/1.27 --sat_fm_lemmas false
% 3.81/1.27 --sat_fm_prep false
% 3.81/1.27 --sat_fm_uc_incr true
% 3.81/1.27 --sat_out_model small
% 3.81/1.27 --sat_out_clauses false
% 3.81/1.27
% 3.81/1.27 ------ QBF Options
% 3.81/1.27
% 3.81/1.27 --qbf_mode false
% 3.81/1.27 --qbf_elim_univ false
% 3.81/1.27 --qbf_dom_inst none
% 3.81/1.27 --qbf_dom_pre_inst false
% 3.81/1.27 --qbf_sk_in false
% 3.81/1.27 --qbf_pred_elim true
% 3.81/1.27 --qbf_split 512
% 3.81/1.27
% 3.81/1.27 ------ BMC1 Options
% 3.81/1.27
% 3.81/1.27 --bmc1_incremental false
% 3.81/1.27 --bmc1_axioms reachable_all
% 3.81/1.27 --bmc1_min_bound 0
% 3.81/1.27 --bmc1_max_bound -1
% 3.81/1.27 --bmc1_max_bound_default -1
% 3.81/1.27 --bmc1_symbol_reachability true
% 3.81/1.27 --bmc1_property_lemmas false
% 3.81/1.27 --bmc1_k_induction false
% 3.81/1.27 --bmc1_non_equiv_states false
% 3.81/1.27 --bmc1_deadlock false
% 3.81/1.27 --bmc1_ucm false
% 3.81/1.27 --bmc1_add_unsat_core none
% 3.81/1.27 --bmc1_unsat_core_children false
% 3.81/1.27 --bmc1_unsat_core_extrapolate_axioms false
% 3.81/1.27 --bmc1_out_stat full
% 3.81/1.27 --bmc1_ground_init false
% 3.81/1.27 --bmc1_pre_inst_next_state false
% 3.81/1.27 --bmc1_pre_inst_state false
% 3.81/1.27 --bmc1_pre_inst_reach_state false
% 3.81/1.27 --bmc1_out_unsat_core false
% 3.81/1.27 --bmc1_aig_witness_out false
% 3.81/1.27 --bmc1_verbose false
% 3.81/1.27 --bmc1_dump_clauses_tptp false
% 3.81/1.27 --bmc1_dump_unsat_core_tptp false
% 3.81/1.27 --bmc1_dump_file -
% 3.81/1.27 --bmc1_ucm_expand_uc_limit 128
% 3.81/1.27 --bmc1_ucm_n_expand_iterations 6
% 3.81/1.27 --bmc1_ucm_extend_mode 1
% 3.81/1.27 --bmc1_ucm_init_mode 2
% 3.81/1.27 --bmc1_ucm_cone_mode none
% 3.81/1.27 --bmc1_ucm_reduced_relation_type 0
% 3.81/1.27 --bmc1_ucm_relax_model 4
% 3.81/1.27 --bmc1_ucm_full_tr_after_sat true
% 3.81/1.27 --bmc1_ucm_expand_neg_assumptions false
% 3.81/1.27 --bmc1_ucm_layered_model none
% 3.81/1.27 --bmc1_ucm_max_lemma_size 10
% 3.81/1.27
% 3.81/1.27 ------ AIG Options
% 3.81/1.27
% 3.81/1.27 --aig_mode false
% 3.81/1.27
% 3.81/1.27 ------ Instantiation Options
% 3.81/1.27
% 3.81/1.27 --instantiation_flag true
% 3.81/1.27 --inst_sos_flag false
% 3.81/1.27 --inst_sos_phase true
% 3.81/1.27 --inst_sos_sth_lit_sel [+prop;+non_prol_conj_symb;-eq;+ground;-num_var;-num_symb]
% 3.81/1.27 --inst_lit_sel [-sign;+ground;-num_var;-num_symb]
% 3.81/1.27 --inst_lit_sel_side num_symb
% 3.81/1.27 --inst_solver_per_active 1400
% 3.81/1.27 --inst_solver_calls_frac 1.
% 3.81/1.27 --inst_to_smt_solver true
% 3.81/1.27 --inst_passive_queue_type priority_queues
% 3.81/1.27 --inst_passive_queues [[-num_var];[+age;-num_symb]]
% 3.81/1.27 --inst_passive_queues_freq [25;2]
% 3.81/1.27 --inst_dismatching true
% 3.81/1.27 --inst_eager_unprocessed_to_passive true
% 3.81/1.27 --inst_unprocessed_bound 1000
% 3.81/1.27 --inst_prop_sim_given true
% 3.81/1.27 --inst_prop_sim_new false
% 3.81/1.27 --inst_subs_new false
% 3.81/1.27 --inst_eq_res_simp false
% 3.81/1.27 --inst_subs_given false
% 3.81/1.27 --inst_orphan_elimination true
% 3.81/1.27 --inst_learning_loop_flag true
% 3.81/1.27 --inst_learning_start 3000
% 3.81/1.27 --inst_learning_factor 2
% 3.81/1.27 --inst_start_prop_sim_after_learn 3
% 3.81/1.27 --inst_sel_renew solver
% 3.81/1.27 --inst_lit_activity_flag true
% 3.81/1.27 --inst_restr_to_given false
% 3.81/1.27 --inst_activity_threshold 500
% 3.81/1.27
% 3.81/1.27 ------ Resolution Options
% 3.81/1.27
% 3.81/1.27 --resolution_flag true
% 3.81/1.27 --res_lit_sel neg_min
% 3.81/1.27 --res_lit_sel_side none
% 3.81/1.27 --res_ordering kbo
% 3.81/1.27 --res_to_prop_solver active
% 3.81/1.27 --res_prop_simpl_new false
% 3.81/1.27 --res_prop_simpl_given true
% 3.81/1.27 --res_to_smt_solver true
% 3.81/1.27 --res_passive_queue_type priority_queues
% 3.81/1.27 --res_passive_queues [[-num_symb];[+age;-num_symb]]
% 3.81/1.27 --res_passive_queues_freq [15;5]
% 3.81/1.27 --res_forward_subs full
% 3.81/1.27 --res_backward_subs full
% 3.81/1.27 --res_forward_subs_resolution true
% 3.81/1.27 --res_backward_subs_resolution true
% 3.81/1.27 --res_orphan_elimination true
% 3.81/1.27 --res_time_limit 300.
% 3.81/1.27
% 3.81/1.27 ------ Superposition Options
% 3.81/1.27
% 3.81/1.27 --superposition_flag true
% 3.81/1.27 --sup_passive_queue_type priority_queues
% 3.81/1.27 --sup_passive_queues [[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]
% 3.81/1.27 --sup_passive_queues_freq [1;1;1]
% 3.81/1.27 --twee_lhs_weight 4
% 3.81/1.27 --sup_set_join false
% 3.81/1.27 --sup_set_join_goals true
% 3.81/1.27 --sup_set_join_limit 1000
% 3.81/1.27 --demod_completeness_check fast
% 3.81/1.27 --demod_use_ground true
% 3.81/1.27 --sup_unprocessed_bound 0
% 3.81/1.27 --sup_to_prop_solver passive
% 3.81/1.27 --sup_prop_simpl_new true
% 3.81/1.27 --sup_prop_simpl_given true
% 3.81/1.27 --sup_fun_splitting false
% 3.81/1.27 --sup_iter_deepening 2
% 3.81/1.27 --sup_restarts_mult 12
% 3.81/1.27 --sup_score sim_d_gen
% 3.81/1.27 --sup_share_score_frac 0.2
% 3.81/1.27 --sup_share_max_num_cl 500
% 3.81/1.27 --sup_ordering lpo
% 3.81/1.27 --sup_symb_ordering invfreq
% 3.81/1.27 --sup_term_weight default
% 3.81/1.27
% 3.81/1.27 ------ Superposition Simplification Setup
% 3.81/1.27
% 3.81/1.27 --sup_indices_passive [LightNormIndex;FwDemodIndex]
% 3.81/1.27 --sup_full_triv [SMTSimplify;PropSubs]
% 3.81/1.27 --sup_full_fw [ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 3.81/1.27 --sup_full_bw [BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 3.81/1.27 --sup_immed_triv []
% 3.81/1.27 --sup_immed_fw_main [ACNormalisation;FwLightNorm;FwUnitSubsAndRes]
% 3.81/1.27 --sup_immed_fw_immed [ACNormalisation;FwUnitSubsAndRes]
% 3.81/1.27 --sup_immed_bw_main [BwUnitSubsAndRes;BwDemod]
% 3.81/1.27 --sup_immed_bw_immed [BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 3.81/1.27 --sup_input_triv [Unflattening;SMTSimplify]
% 3.81/1.27 --sup_input_fw [FwACDemod;ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 3.81/1.27 --sup_input_bw [BwACDemod;BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 3.81/1.27 --sup_full_fixpoint true
% 3.81/1.27 --sup_main_fixpoint true
% 3.81/1.27 --sup_immed_fixpoint false
% 3.81/1.27 --sup_input_fixpoint true
% 3.81/1.27 --sup_cache_sim none
% 3.81/1.27 --sup_smt_interval 500
% 3.81/1.27 --sup_bw_gjoin_interval 0
% 3.81/1.27
% 3.81/1.27 ------ Combination Options
% 3.81/1.27
% 3.81/1.27 --comb_mode clause_based
% 3.81/1.27 --comb_inst_mult 5
% 3.81/1.27 --comb_res_mult 1
% 3.81/1.27 --comb_sup_mult 1
% 3.81/1.27 --comb_sup_deep_mult 1
% 3.81/1.27
% 3.81/1.27 ------ Debug Options
% 3.81/1.27
% 3.81/1.27 --dbg_backtrace false
% 3.81/1.27 --dbg_dump_prop_clauses false
% 3.81/1.27 --dbg_dump_prop_clauses_file -
% 3.81/1.27 --dbg_out_stat false
% 3.81/1.27 --dbg_just_parse false
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27 ------ Proving...
% 3.81/1.27
% 3.81/1.27
% 3.81/1.27 % SZS status Satisfiable for theBenchmark.p
% 3.81/1.27
% 3.81/1.27 % SZS output start Saturation for theBenchmark.p
% See solution above
% 3.81/1.27
% 3.81/1.27
%------------------------------------------------------------------------------