%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV299-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.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:17:00 PM UTC 2026
% Result : Unsatisfiable 32.36s 7.20s
% Output : CNFRefutation 32.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of formulae : 121 ( 49 unt; 28 def)
% Number of atoms : 526 ( 28 equ)
% Maximal formula atoms : 4 ( 4 avg)
% Number of connectives : 205 ( 106 ~; 99 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 32 ( 30 usr; 30 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 14 con; 0-3 aty)
% Number of variables : 142 ( 0 sgn 142 !; 0 ?; 119 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1473,axiom,
! [X2,X0,X1] :
( c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-0.ax',cls_Message_OMPair__analz_0) ).
fof(f1498,axiom,
! [X0,X1] :
( c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-0.ax',cls_Message_Oanalz_OInj_0) ).
fof(f1514,axiom,
! [X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(X1)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-0.ax',cls_Message_Oparts__partsD__dest_0) ).
fof(f1522,axiom,
! [X2,X3,X0,X1] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-1.ax',cls_Event_OSays__imp__analz__Spy__dest_0) ).
fof(f1525,axiom,
! [X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-1.ax',cls_Message_Oanalz__into__parts__dest_0) ).
fof(f1529,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(X1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X3,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X4),c_Message_Omsg_OAgent(X1))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-1.ax',cls_OtwayRees_Ono__nonce__OR1__OR2__dest_0) ).
fof(f1560,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Event_Oevent_OSays(X1,X3,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X3)))))))),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OAgent(X3)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_OtwayRees_OCrypt__imp__OR1__dest_0) ).
fof(f1563,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1564,negated_conjecture,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1566,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1567,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
tcf(c_2158,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X1,c_Message_Oanalz(X2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oanalz(X2),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1473]) ).
tcf(c_2177,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1498]) ).
tcf(c_2191,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(X1)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1514]) ).
tcf(c_2199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[],[f1522]) ).
tcf(c_2202,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oanalz(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1525]) ).
tcf(c_2206,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X4,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1529]) ).
tcf(c_2235,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(X0,X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))))))),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1560]) ).
tcf(c_2237,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[],[f1563]) ).
tcf(c_2238,negated_conjecture,
c_in(v_evs3,c_OtwayRees_Ootway,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[],[f1564]) ).
tcf(c_2240,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_A,v_B,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(v_B)))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[],[f1566]) ).
tcf(c_2241,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NB),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_OAgent(v_A)))))))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[],[f1567]) ).
tcf(c_15670,definition,
iPr_def_11 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_15675,definition,
iPr_def_16 = c_List_Oset(v_evs3,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_15676,definition,
iPr_def_17 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_15677,definition,
iPr_def_18 = c_Message_Oparts(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_15678,definition,
iPr_def_19 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_15679,definition,
iPr_def_20 = c_Message_Omsg_OAgent(v_Aa),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_15680,definition,
iPr_def_21 = c_Message_Omsg_OAgent(v_A),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_15681,definition,
iPr_def_22 = c_Public_OshrK(v_Aa),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_15682,definition,
iPr_def_23 = c_Message_Omsg_OMPair(iPr_def_20,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_15683,definition,
iPr_def_24 = c_Message_Omsg_OMPair(iPr_def_19,iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_15684,definition,
iPr_def_25 = c_Message_Omsg_OCrypt(iPr_def_22,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_15685,definition,
iPr_def_26 = c_Message_Omsg_OMPair(iPr_def_10,iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_15686,definition,
iPr_def_27 = c_Message_Omsg_OMPair(iPr_def_19,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_15687,definition,
iPr_def_28 = c_Message_Omsg_OCrypt(iPr_def_11,iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_15688,definition,
iPr_def_29 = c_Message_Omsg_OMPair(iPr_def_25,iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_15689,definition,
iPr_def_30 = c_Message_Omsg_OMPair(iPr_def_21,iPr_def_29),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_15690,definition,
iPr_def_31 = c_Message_Omsg_OMPair(iPr_def_20,iPr_def_30),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_15691,definition,
iPr_def_32 = c_Message_Omsg_OMPair(iPr_def_19,iPr_def_31),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_15692,definition,
iPr_def_33 = c_Event_Oevent_OSays(v_Aaa,c_Message_Oagent_OServer,iPr_def_32),
introduced(definition,[new_symbols(definition,[iPr_def_33])],[]) ).
tcf(c_15693,definition,
iPr_def_34 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_15694,definition,
iPr_def_35 = c_Message_Omsg_OMPair(iPr_def_21,iPr_def_34),
introduced(definition,[new_symbols(definition,[iPr_def_35])],[]) ).
tcf(c_15695,definition,
iPr_def_36 = c_Message_Omsg_OMPair(iPr_def_10,iPr_def_35),
introduced(definition,[new_symbols(definition,[iPr_def_36])],[]) ).
tcf(c_15696,definition,
iPr_def_37 = c_Message_Omsg_OCrypt(iPr_def_11,iPr_def_36),
introduced(definition,[new_symbols(definition,[iPr_def_37])],[]) ).
tcf(c_15697,definition,
iPr_def_38 = c_Message_Omsg_OMPair(iPr_def_34,iPr_def_37),
introduced(definition,[new_symbols(definition,[iPr_def_38])],[]) ).
tcf(c_15698,definition,
iPr_def_39 = c_Message_Omsg_OMPair(iPr_def_21,iPr_def_38),
introduced(definition,[new_symbols(definition,[iPr_def_39])],[]) ).
tcf(c_15699,definition,
iPr_def_40 = c_Message_Omsg_OMPair(iPr_def_10,iPr_def_39),
introduced(definition,[new_symbols(definition,[iPr_def_40])],[]) ).
tcf(c_15700,definition,
iPr_def_41 = c_Event_Oevent_OSays(v_A,v_B,iPr_def_40),
introduced(definition,[new_symbols(definition,[iPr_def_41])],[]) ).
tcf(c_15702,definition,
iPr_def_43 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[iPr_def_43])],[]) ).
tcf(c_15706,negated_conjecture,
c_in(iPr_def_33,iPr_def_16,tc_Event_Oevent),
inference(demodulation,[status(thm)],[c_2241,c_15685,c_15686,c_15687,c_15682,c_15683,c_15681,c_15684,c_15688,c_15680,c_15689,c_15679,c_15690,c_15678,c_15691,c_15692]) ).
tcf(c_15707,negated_conjecture,
c_in(iPr_def_41,iPr_def_16,tc_Event_Oevent),
inference(demodulation,[status(thm)],[c_2240,c_15694,c_15695,c_15696,c_15693,c_15697,c_15698,c_15699,c_15700]) ).
tcf(c_15709,negated_conjecture,
c_in(v_evs3,c_OtwayRees_Ootway,iPr_def_43),
inference(demodulation,[status(thm)],[c_2238,c_15702]) ).
tcf(c_15710,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(demodulation,[status(thm)],[c_2237]) ).
tcf(c_23750,plain,
! [X0: $i] :
( c_in(X0,c_Message_Oparts(iPr_def_17),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(iPr_def_18),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15677,c_2191]) ).
tcf(c_23751,plain,
! [X0: $i] :
( c_in(X0,iPr_def_18,tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(iPr_def_18),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_23750,c_15677]) ).
tcf(c_24061,plain,
! [X0: $i] :
( c_in(iPr_def_28,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_29,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15688,c_2158]) ).
tcf(c_24062,plain,
! [X0: $i] :
( c_in(iPr_def_29,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_30,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15689,c_2158]) ).
tcf(c_24063,plain,
! [X0: $i] :
( c_in(iPr_def_30,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_31,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15690,c_2158]) ).
tcf(c_24064,plain,
! [X0: $i] :
( c_in(iPr_def_31,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15691,c_2158]) ).
tcf(c_24067,plain,
! [X0: $i] :
( c_in(iPr_def_37,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_38,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15697,c_2158]) ).
tcf(c_24068,plain,
! [X0: $i] :
( c_in(iPr_def_38,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_39,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15698,c_2158]) ).
tcf(c_24069,plain,
! [X0: $i] :
( c_in(iPr_def_39,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_40,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15699,c_2158]) ).
tcf(c_27071,plain,
! [X0: $i] :
( c_in(iPr_def_31,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_2177,c_24064]) ).
tcf(c_27081,plain,
! [X0: $i] :
( c_in(iPr_def_30,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_27071,c_24063]) ).
tcf(c_28070,plain,
! [X0: $i] :
( c_in(iPr_def_29,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_27081,c_24062]) ).
tcf(c_28243,plain,
! [X0: $i] :
( c_in(iPr_def_28,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_28070,c_24061]) ).
tcf(c_28305,plain,
! [X0: $i] :
( c_in(iPr_def_28,c_Message_Oparts(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_32,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_28243,c_2202]) ).
tcf(c_28470,plain,
( c_in(iPr_def_28,iPr_def_18,tc_Message_Omsg)
| ~ c_in(iPr_def_32,iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_28305,c_23751]) ).
tcf(c_28974,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),iPr_def_16,tc_Event_Oevent) ),
inference(superposition,[status(thm)],[c_15675,c_2199]) ).
tcf(c_28980,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X2,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OSays(X0,X1,X2),iPr_def_16,tc_Event_Oevent) ),
inference(light_normalisation,[status(thm)],[c_28974,c_15676]) ).
tcf(c_29718,plain,
! [X0: $i] :
( c_in(iPr_def_38,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_39,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_2177,c_24068]) ).
tcf(c_29728,plain,
! [X0: $i] :
( c_in(iPr_def_37,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_39,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29718,c_24067]) ).
tcf(c_29763,plain,
! [X0: $i] :
( c_in(iPr_def_37,c_Message_Oparts(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_39,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29728,c_2202]) ).
tcf(c_29779,plain,
( c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg)
| ~ c_in(iPr_def_39,iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29763,c_23751]) ).
tcf(c_29870,plain,
! [X0: $i] :
( c_in(iPr_def_39,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_40,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_2177,c_24069]) ).
tcf(c_29880,plain,
! [X0: $i] :
( c_in(iPr_def_38,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_40,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29870,c_24068]) ).
tcf(c_29955,plain,
! [X0: $i] :
( c_in(iPr_def_37,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_40,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29880,c_24067]) ).
tcf(c_29996,plain,
! [X0: $i] :
( c_in(iPr_def_37,c_Message_Oparts(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_40,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29955,c_2202]) ).
tcf(c_30312,plain,
( c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg)
| ~ c_in(iPr_def_40,iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_29996,c_23751]) ).
tcf(c_36240,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X4,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_2206,c_15702]) ).
tcf(c_36263,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),c_Message_Oparts(iPr_def_17),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15676,c_36240]) ).
tcf(c_36264,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_36263,c_15676,c_15677]) ).
tcf(c_36265,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X4)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X3),c_Message_Omsg_OAgent(X0))))),iPr_def_18,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36264,c_15709]) ).
tcf(c_36441,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(X3)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),iPr_def_21)))),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15680,c_36265]) ).
tcf(c_36452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X3)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),iPr_def_21)))),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_36441,c_15670,c_15680]) ).
tcf(c_36453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X3)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),iPr_def_21)))),iPr_def_18,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36452,c_15710]) ).
tcf(c_36481,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X2)))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(iPr_def_20,iPr_def_21)))),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15679,c_36453]) ).
tcf(c_36482,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X2,c_Message_Omsg_OMPair(X0,iPr_def_23))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_36481,c_15682]) ).
tcf(c_37242,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(X0,X2,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))))))),c_List_Oset(X3,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X3,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OAgent(X2)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X3)),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_2235,c_15702]) ).
tcf(c_37264,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(v_A,X1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X2,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_A),c_Message_Omsg_OAgent(X1)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15680,c_37242]) ).
tcf(c_37311,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(v_A,X1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X2,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_37264,c_15670,c_15680]) ).
tcf(c_37312,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(c_Event_Oevent_OSays(v_A,X1,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))))))),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X2,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_37311,c_15710]) ).
tcf(c_37642,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1))))))),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_37312,c_2199]) ).
tcf(c_38973,plain,
! [X0: $i,X1: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1))))))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15676,c_37642]) ).
tcf(c_38983,plain,
! [X0: $i,X1: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1))))))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(v_evs3,c_OtwayRees_Ootway,iPr_def_43)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_38973,c_15676,c_15677]) ).
tcf(c_38984,plain,
! [X0: $i,X1: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1))))))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(X1)))),iPr_def_18,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_38983,c_15709]) ).
tcf(c_39179,plain,
! [X0: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(iPr_def_34,c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,iPr_def_34)))))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OAgent(v_B)))),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15693,c_38984]) ).
tcf(c_39191,plain,
! [X0: $i] :
( c_in(c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(iPr_def_34,c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,iPr_def_35))))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,iPr_def_35)),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_39179,c_15693,c_15694]) ).
tcf(c_39373,plain,
! [X0: $i,X1: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X1,c_Message_Omsg_OMPair(iPr_def_21,iPr_def_34))),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,iPr_def_23))),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15693,c_36482]) ).
tcf(c_39377,plain,
! [X0: $i,X1: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X1,iPr_def_35)),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,c_Message_Omsg_OMPair(X1,iPr_def_23))),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_39373,c_15694]) ).
tcf(c_39660,plain,
( c_in(c_Message_Omsg_OMPair(iPr_def_10,c_Message_Omsg_OMPair(iPr_def_21,c_Message_Omsg_OMPair(iPr_def_34,c_Message_Omsg_OCrypt(iPr_def_11,iPr_def_36)))),c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(iPr_def_10,iPr_def_35)),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15695,c_39191]) ).
tcf(c_39664,plain,
( c_in(iPr_def_40,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_39660,c_15695,c_15696,c_15697,c_15698,c_15699]) ).
tcf(c_39858,plain,
( c_in(iPr_def_39,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_39664,c_24069]) ).
tcf(c_41849,plain,
( c_in(iPr_def_39,c_Message_Oparts(iPr_def_17),tc_Message_Omsg)
| ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_39858,c_2202]) ).
tcf(c_41856,plain,
( c_in(iPr_def_39,iPr_def_18,tc_Message_Omsg)
| ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_41849,c_15677]) ).
tcf(c_44061,plain,
! [X0: $i] :
( ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(iPr_def_10,iPr_def_35)),iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,iPr_def_26)),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15685,c_39377]) ).
tcf(c_44062,plain,
! [X0: $i] :
( ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,c_Message_Omsg_OMPair(X0,iPr_def_26)),iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_44061,c_15695,c_15696]) ).
tcf(c_49169,plain,
( ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_11,iPr_def_27),iPr_def_18,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15686,c_44062]) ).
tcf(c_49170,plain,
( ~ c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg)
| ~ c_in(iPr_def_28,iPr_def_18,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_49169,c_15687]) ).
tcf(c_96325,plain,
( c_in(iPr_def_32,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(iPr_def_33,iPr_def_16,tc_Event_Oevent) ),
inference(superposition,[status(thm)],[c_15692,c_28980]) ).
tcf(c_96326,plain,
( c_in(iPr_def_40,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg)
| ~ c_in(iPr_def_41,iPr_def_16,tc_Event_Oevent) ),
inference(superposition,[status(thm)],[c_15700,c_28980]) ).
tcf(c_96327,plain,
c_in(iPr_def_40,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_96326,c_15707]) ).
tcf(c_96328,plain,
c_in(iPr_def_32,c_Message_Oanalz(iPr_def_17),tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_96325,c_15706]) ).
tcf(c_96487,plain,
c_in(iPr_def_40,c_Message_Oparts(iPr_def_17),tc_Message_Omsg),
inference(superposition,[status(thm)],[c_96327,c_2202]) ).
tcf(c_96494,plain,
c_in(iPr_def_40,iPr_def_18,tc_Message_Omsg),
inference(light_normalisation,[status(thm)],[c_96487,c_15677]) ).
tcf(c_96500,plain,
c_in(iPr_def_37,iPr_def_18,tc_Message_Omsg),
inference(backward_subsumption_resolution,[status(thm)],[c_30312,c_96494]) ).
tcf(c_96554,plain,
c_in(iPr_def_39,iPr_def_18,tc_Message_Omsg),
inference(backward_subsumption_resolution,[status(thm)],[c_41856,c_96500]) ).
tcf(c_96570,plain,
c_in(iPr_def_32,c_Message_Oparts(iPr_def_17),tc_Message_Omsg),
inference(superposition,[status(thm)],[c_96328,c_2202]) ).
tcf(c_96579,plain,
c_in(iPr_def_32,iPr_def_18,tc_Message_Omsg),
inference(light_normalisation,[status(thm)],[c_96570,c_15677]) ).
tcf(c_96580,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_96579,c_96554,c_49170,c_29779,c_28470]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV299-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 19:08:54 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 32.36/7.20 % SZS status Started for theBenchmark.p
% 32.36/7.20 % SZS status Unsatisfiable for theBenchmark.p
% 32.36/7.20
% 32.36/7.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 32.36/7.20
% 32.36/7.20 % ------ iProver source info
% 32.36/7.20
% 32.36/7.20 % git: date: 2026-07-19 20:42:38 +0200
% 32.36/7.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 32.36/7.20 % git: non_committed_changes: false
% 32.36/7.20
% 32.36/7.20 % ------ Parsing...% successful
% 32.36/7.20
% 32.36/7.20
% 32.36/7.20 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 32.36/7.20
% 32.36/7.20 % ------ Preprocessing... sup_sim: 1 sf_s rm: 18 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 30 0s sf_e pe_s pe_e %
% 32.36/7.20
% 32.36/7.20 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 32.36/7.20
% 32.36/7.20 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 32.36/7.20 % ------ Proving...
% 32.36/7.20 % ------ Problem Properties
% 32.36/7.20
% 32.36/7.20 %
% 32.36/7.20 % clauses 432
% 32.36/7.20 % conjectures 8
% 32.36/7.20 % EPR 37
% 32.36/7.20 % Horn 397
% 32.36/7.20 % unary 150
% 32.36/7.20 % binary 219
% 32.36/7.20 % lits 781
% 32.36/7.20 % lits eq 258
% 32.36/7.20 % fd_pure 0
% 32.36/7.20 % fd_pseudo 0
% 32.36/7.20 % fd_cond 21
% 32.36/7.20 % fd_pseudo_cond 62
% 32.36/7.20 % AC symbols 0
% 32.36/7.20
% 32.36/7.20 % ------ Schedule dynamic 5 is on
% 32.36/7.20
% 32.36/7.20 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 32.36/7.20
% 32.36/7.20
% 32.36/7.20 % ------
% 32.36/7.20 % Current options:
% 32.36/7.20 % ------
% 32.36/7.20
% 32.36/7.20
% 32.36/7.20 %
% 32.36/7.20
% 32.36/7.20 % ------ Proving...
% 32.36/7.20 %
% 32.36/7.20
% 32.36/7.20 % SZS status Unsatisfiable for theBenchmark.p
% 32.36/7.20
% 32.36/7.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 32.36/7.20
% 32.36/7.20
%------------------------------------------------------------------------------