%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV337-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 : n013.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:21 PM UTC 2026
% Result : Unsatisfiable 26.44s 6.36s
% Output : CNFRefutation 26.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 29
% Syntax : Number of formulae : 109 ( 41 unt; 16 def)
% Number of atoms : 403 ( 16 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 193 ( 97 ~; 96 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 17 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 14 con; 0-3 aty)
% Number of variables : 130 ( 0 sgn 130 !; 0 ?; 101 :)
% 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(f1474,axiom,
! [X2,X0,X1] :
( c_in(X0,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_1) ).
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(f1526,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-3.ax',cls_Message_Oanalz__into__parts__dest_0) ).
fof(f1528,axiom,
! [X2,X0,X1] :
( c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),X1),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X0,c_Event_Obad,tc_Message_Oagent) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-3.ax',cls_Public_OCrypt__Spy__analz__bad_0) ).
fof(f1558,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X1,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X4,X5)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OKey(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(c_Message_Omsg_OAgent(X2),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X3),c_Message_Omsg_OMPair(X4,X5)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-3.ax',cls_Yahalom_OA__trusts__YM3_0) ).
fof(f1560,axiom,
! [X2,X0,X1] :
( c_in(X2,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OGets(X1,X2),c_List_Oset(X0,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-3.ax',cls_Yahalom_OGets__imp__analz__Spy__dest_0) ).
fof(f1561,axiom,
! [X0,X1] :
( c_in(X1,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X1)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(X0,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV006-3.ax',cls_Yahalom_OSpy__see__shrK__D__dest_0) ).
fof(f1570,negated_conjecture,
c_in(v_evs4,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1574,negated_conjecture,
c_in(c_Event_Oevent_OGets(v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1577,negated_conjecture,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1579,negated_conjecture,
! [X2,X0,X1] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X2),c_Message_Omsg_ONonce(v_NB))))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(v_K))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_8) ).
tcf(c_2164,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_2165,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X0,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,[],[f1474]) ).
tcf(c_2183,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_2197,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_2209,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,[],[f1526]) ).
tcf(c_2211,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),X1),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1528]) ).
tcf(c_2240,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),c_List_Oset(X5,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X5,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X5)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1558]) ).
tcf(c_2242,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent) ),
inference(cnf_transformation,[],[f1560]) ).
tcf(c_2243,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X1,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(cnf_transformation,[],[f1561]) ).
tcf(c_2248,negated_conjecture,
c_in(v_evs4,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)),
inference(cnf_transformation,[],[f1570]) ).
tcf(c_2251,negated_conjecture,
c_in(c_Event_Oevent_OGets(v_A,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_ONonce(v_NB))))),v_X)),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[],[f1574]) ).
tcf(c_2254,negated_conjecture,
~ c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg),
inference(cnf_transformation,[],[f1577]) ).
tcf(c_2256,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X2),c_Message_Omsg_ONonce(v_NB))))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(v_K))))),c_List_Oset(v_evs4,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[],[f1579]) ).
tcf(c_15803,definition,
iPr_def_10 = c_Message_Omsg_OKey(v_K),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_15804,definition,
iPr_def_11 = c_Message_Omsg_ONonce(v_NB),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_15805,definition,
iPr_def_12 = c_List_Oset(v_evs4,tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_15807,definition,
iPr_def_14 = c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_15808,definition,
iPr_def_15 = c_Message_Oparts(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_15809,definition,
iPr_def_16 = c_Message_Oanalz(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_15811,definition,
iPr_def_18 = c_Message_Omsg_ONonce(v_NA),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_15814,definition,
iPr_def_21 = c_Public_OshrK(v_A),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_15815,definition,
iPr_def_22 = c_Message_Omsg_OAgent(v_B),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_15816,definition,
iPr_def_23 = c_Message_Omsg_OMPair(iPr_def_18,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_15817,definition,
iPr_def_24 = c_Message_Omsg_OMPair(iPr_def_10,iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_15818,definition,
iPr_def_25 = c_Message_Omsg_OMPair(iPr_def_22,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_15819,definition,
iPr_def_26 = c_Message_Omsg_OCrypt(iPr_def_21,iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_15820,definition,
iPr_def_27 = c_Message_Omsg_OMPair(iPr_def_26,v_X),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_15821,definition,
iPr_def_28 = c_Event_Oevent_OGets(v_A,iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_15822,definition,
iPr_def_29 = tc_List_Olist(tc_Event_Oevent),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_15823,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(iPr_def_10,c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(X2),iPr_def_11)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),iPr_def_10)))),iPr_def_12,tc_Event_Oevent),
inference(demodulation,[status(thm)],[c_2256,c_15805,c_15804,c_15803]) ).
tcf(c_15825,negated_conjecture,
~ c_in(iPr_def_11,iPr_def_16,tc_Message_Omsg),
inference(demodulation,[status(thm)],[c_2254,c_15809]) ).
tcf(c_15828,negated_conjecture,
c_in(iPr_def_28,iPr_def_12,tc_Event_Oevent),
inference(demodulation,[status(thm)],[c_2251,c_15816,c_15817,c_15815,c_15818,c_15814,c_15819,c_15820,c_15821]) ).
tcf(c_15831,negated_conjecture,
c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29),
inference(demodulation,[status(thm)],[c_2248,c_15822]) ).
tcf(c_22889,plain,
! [X0: $i,X1: $i] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(iPr_def_10,c_Message_Omsg_OMPair(iPr_def_18,iPr_def_11)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),iPr_def_10)))),iPr_def_12,tc_Event_Oevent),
inference(superposition,[status(thm)],[c_15811,c_15823]) ).
tcf(c_22890,plain,
! [X0: $i,X1: $i] : ~ c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),iPr_def_24)),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),iPr_def_10)))),iPr_def_12,tc_Event_Oevent),
inference(light_normalisation,[status(thm)],[c_22889,c_15816,c_15817]) ).
tcf(c_23483,plain,
! [X0: $i] :
( c_in(X0,c_Message_Oparts(iPr_def_14),tc_Message_Omsg)
| ~ c_in(X0,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_2209]) ).
tcf(c_23484,plain,
! [X0: $i] :
( c_in(X0,iPr_def_15,tc_Message_Omsg)
| ~ c_in(X0,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_23483,c_15808]) ).
tcf(c_23836,plain,
! [X0: $i] :
( c_in(X0,c_Message_Oparts(iPr_def_14),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(iPr_def_15),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15808,c_2197]) ).
tcf(c_23837,plain,
! [X0: $i] :
( c_in(X0,iPr_def_15,tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(iPr_def_15),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_23836,c_15808]) ).
tcf(c_24193,plain,
! [X0: $i] :
( c_in(iPr_def_26,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_27,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15820,c_2165]) ).
tcf(c_25488,plain,
! [X0: $i] :
( c_in(iPr_def_26,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_27,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_2183,c_24193]) ).
tcf(c_25489,plain,
( c_in(iPr_def_26,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg)
| ~ c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_24193]) ).
tcf(c_25490,plain,
( c_in(iPr_def_26,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_25489,c_15809]) ).
tcf(c_25505,plain,
! [X0: $i] :
( c_in(iPr_def_26,c_Message_Oparts(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_27,X0,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_25488,c_2209]) ).
tcf(c_25578,plain,
( c_in(iPr_def_26,iPr_def_15,tc_Message_Omsg)
| ~ c_in(iPr_def_27,iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_25505,c_23837]) ).
tcf(c_31271,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X2)),tc_Message_Omsg)
| ~ c_in(X2,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),c_List_Oset(X2,tc_Event_Oevent),tc_Event_Oevent) ),
inference(light_normalisation,[status(thm)],[c_2242,c_15822]) ).
tcf(c_31283,plain,
! [X0: $i,X1: $i] :
( c_in(X1,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),iPr_def_12,tc_Event_Oevent) ),
inference(superposition,[status(thm)],[c_15805,c_31271]) ).
tcf(c_31285,plain,
! [X0: $i,X1: $i] :
( c_in(X1,iPr_def_16,tc_Message_Omsg)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),iPr_def_12,tc_Event_Oevent) ),
inference(light_normalisation,[status(thm)],[c_31283,c_15807,c_15809]) ).
tcf(c_31286,plain,
! [X0: $i,X1: $i] :
( c_in(X1,iPr_def_16,tc_Message_Omsg)
| ~ c_in(c_Event_Oevent_OGets(X0,X1),iPr_def_12,tc_Event_Oevent) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31285,c_15831]) ).
tcf(c_31332,plain,
( c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_28,iPr_def_12,tc_Event_Oevent) ),
inference(superposition,[status(thm)],[c_15821,c_31286]) ).
tcf(c_31333,plain,
c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_31332,c_15828]) ).
tcf(c_31334,plain,
c_in(iPr_def_26,iPr_def_16,tc_Message_Omsg),
inference(backward_subsumption_resolution,[status(thm)],[c_25490,c_31333]) ).
tcf(c_31336,plain,
c_in(iPr_def_27,iPr_def_15,tc_Message_Omsg),
inference(superposition,[status(thm)],[c_31333,c_23484]) ).
tcf(c_31344,plain,
c_in(iPr_def_26,iPr_def_15,tc_Message_Omsg),
inference(backward_subsumption_resolution,[status(thm)],[c_25578,c_31336]) ).
tcf(c_37899,plain,
! [X0: $i] :
( c_in(iPr_def_11,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_23,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15816,c_2164]) ).
tcf(c_37900,plain,
! [X0: $i] :
( c_in(iPr_def_23,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_24,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15817,c_2164]) ).
tcf(c_37901,plain,
! [X0: $i] :
( c_in(iPr_def_24,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_25,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15818,c_2164]) ).
tcf(c_38111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),c_List_Oset(X5,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(X5,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X5)),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_2240,c_15822]) ).
tcf(c_38137,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15805,c_38111]) ).
tcf(c_38177,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_38137,c_15807,c_15808]) ).
tcf(c_38178,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(X3,X4)))),iPr_def_15,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_38177,c_15831]) ).
tcf(c_38274,plain,
! [X0: $i] :
( c_in(iPr_def_26,c_Message_Oanalz(X0),tc_Message_Omsg)
| ~ c_in(iPr_def_27,c_Message_Oanalz(X0),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15820,c_2165]) ).
tcf(c_38512,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),iPr_def_23))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),c_Message_Omsg_OMPair(iPr_def_18,iPr_def_11)))),iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15816,c_38178]) ).
tcf(c_38581,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),iPr_def_23))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),c_Message_Omsg_OKey(X2))))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(X2),iPr_def_23))),iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_38512,c_15816]) ).
tcf(c_39447,plain,
( c_in(iPr_def_11,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg)
| ~ c_in(iPr_def_23,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_37899]) ).
tcf(c_39448,plain,
( c_in(iPr_def_11,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_23,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_39447,c_15809]) ).
tcf(c_39449,plain,
~ c_in(iPr_def_23,iPr_def_16,tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_39448,c_15825]) ).
tcf(c_40362,plain,
( c_in(iPr_def_23,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg)
| ~ c_in(iPr_def_24,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_37900]) ).
tcf(c_40363,plain,
( c_in(iPr_def_23,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_24,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_40362,c_15809]) ).
tcf(c_40364,plain,
~ c_in(iPr_def_24,iPr_def_16,tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_40363,c_39449]) ).
tcf(c_41996,plain,
( c_in(iPr_def_24,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg)
| ~ c_in(iPr_def_25,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_37901]) ).
tcf(c_41997,plain,
( c_in(iPr_def_24,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_25,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_41996,c_15809]) ).
tcf(c_41998,plain,
~ c_in(iPr_def_25,iPr_def_16,tc_Message_Omsg),
inference(forward_subsumption_resolution,[status(thm)],[c_41997,c_40364]) ).
tcf(c_44731,plain,
( c_in(iPr_def_26,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg)
| ~ c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15809,c_38274]) ).
tcf(c_44732,plain,
( c_in(iPr_def_26,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_27,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_44731,c_15809]) ).
tcf(c_44813,plain,
c_in(iPr_def_26,iPr_def_16,tc_Message_Omsg),
inference(global_subsumption_just,[status(thm)],[c_44732,c_31334]) ).
tcf(c_54553,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(iPr_def_10,iPr_def_23))),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),iPr_def_10)))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_K),iPr_def_23))),iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15803,c_38581]) ).
tcf(c_54623,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,X0,c_Message_Omsg_OMPair(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),iPr_def_24)),c_Message_Omsg_OCrypt(c_Public_OshrK(X1),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X0),iPr_def_10)))),iPr_def_12,tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),iPr_def_24)),iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_54553,c_15803,c_15817]) ).
tcf(c_54624,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(X1),iPr_def_24)),iPr_def_15,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_54623,c_22890]) ).
tcf(c_54772,plain,
! [X0: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),c_Message_Omsg_OMPair(iPr_def_22,iPr_def_24)),iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15815,c_54624]) ).
tcf(c_54776,plain,
! [X0: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(X0),iPr_def_25),iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_54772,c_15818]) ).
tcf(c_54910,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_21,iPr_def_25),iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15814,c_54776]) ).
tcf(c_54911,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(iPr_def_26,iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_54910,c_15819]) ).
tcf(c_54912,plain,
c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(forward_subsumption_resolution,[status(thm)],[c_54911,c_31344]) ).
tcf(c_65410,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(X1,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_2243,c_15822]) ).
tcf(c_65422,plain,
! [X0: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Message_Oparts(iPr_def_14),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15807,c_65410]) ).
tcf(c_65423,plain,
! [X0: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(v_evs4,c_Yahalom_Oyahalom,iPr_def_29)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),iPr_def_15,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_65422,c_15808]) ).
tcf(c_65424,plain,
! [X0: $i] :
( c_in(X0,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),iPr_def_15,tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_65423,c_15831]) ).
tcf(c_66257,plain,
( c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OKey(iPr_def_21),iPr_def_15,tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15814,c_65424]) ).
tcf(c_66294,plain,
c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(global_subsumption_just,[status(thm)],[c_66257,c_54912]) ).
tcf(c_71273,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(v_A,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_21,X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15814,c_2211]) ).
tcf(c_71279,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OCrypt(iPr_def_21,X0),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(forward_subsumption_resolution,[status(thm)],[c_71273,c_66294]) ).
tcf(c_72002,plain,
! [X0: $i] :
( c_in(iPr_def_25,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg)
| ~ c_in(iPr_def_26,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,X0)),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15819,c_71279]) ).
tcf(c_72020,plain,
( c_in(iPr_def_25,c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs4)),tc_Message_Omsg)
| ~ c_in(iPr_def_26,c_Message_Oanalz(iPr_def_14),tc_Message_Omsg) ),
inference(superposition,[status(thm)],[c_15807,c_72002]) ).
tcf(c_72021,plain,
( c_in(iPr_def_25,iPr_def_16,tc_Message_Omsg)
| ~ c_in(iPr_def_26,iPr_def_16,tc_Message_Omsg) ),
inference(light_normalisation,[status(thm)],[c_72020,c_15807,c_15809]) ).
tcf(c_72022,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_72021,c_41998,c_44813]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV337-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.08/0.37 % Computer : n013.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 19:16:06 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.41 Running first-order theorem proving
% 0.08/0.41 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.08/0.42
% 0.08/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.42
% 0.08/0.42 % Detected problem language: tptp
% 0.08/0.44 % Proving...
% 26.44/6.36 % SZS status Started for theBenchmark.p
% 26.44/6.36 % SZS status Unsatisfiable for theBenchmark.p
% 26.44/6.36
% 26.44/6.36 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.44/6.36
% 26.44/6.36 % ------ iProver source info
% 26.44/6.36
% 26.44/6.36 % git: date: 2026-07-19 20:42:38 +0200
% 26.44/6.36 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.44/6.36 % git: non_committed_changes: false
% 26.44/6.36
% 26.44/6.36 % ------ Parsing...% successful
% 26.44/6.36
% 26.44/6.36
% 26.44/6.36 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.44/6.36
% 26.44/6.36 % ------ 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 %
% 26.44/6.36
% 26.44/6.36 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.44/6.36
% 26.44/6.36 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 26.44/6.36 % ------ Proving...
% 26.44/6.36 % ------ Problem Properties
% 26.44/6.36
% 26.44/6.36 %
% 26.44/6.36 % clauses 424
% 26.44/6.36 % conjectures 9
% 26.44/6.36 % EPR 38
% 26.44/6.36 % Horn 390
% 26.44/6.36 % unary 138
% 26.44/6.36 % binary 220
% 26.44/6.36 % lits 781
% 26.44/6.36 % lits eq 245
% 26.44/6.36 % fd_pure 0
% 26.44/6.36 % fd_pseudo 0
% 26.44/6.36 % fd_cond 21
% 26.44/6.36 % fd_pseudo_cond 65
% 26.44/6.36 % AC symbols 0
% 26.44/6.36
% 26.44/6.36 % ------ Schedule dynamic 5 is on
% 26.44/6.36
% 26.44/6.36 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 26.44/6.36
% 26.44/6.36
% 26.44/6.36 % ------
% 26.44/6.36 % Current options:
% 26.44/6.36 % ------
% 26.44/6.36
% 26.44/6.36
% 26.44/6.36 %
% 26.44/6.36
% 26.44/6.36 % ------ Proving...
% 26.44/6.36 %
% 26.44/6.36
% 26.44/6.36 % SZS status Unsatisfiable for theBenchmark.p
% 26.44/6.36
% 26.44/6.36 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 26.44/6.36
% 26.44/6.36
%------------------------------------------------------------------------------