%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV792-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 09:09:07 AM UTC 2026
% Result : Unsatisfiable 259.72s 34.85s
% Output : CNFRefutation 259.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of formulae : 29 ( 18 unt; 0 def)
% Number of atoms : 47 ( 22 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 37 ( 19 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 18 con; 0-3 aty)
% Number of variables : 52 ( 15 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_9,axiom,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)) = v_X,
file('theBenchmark.p',cls_conjecture_9) ).
cnf(c_102,plain,
c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)) = v_X,
inference(clausify,[status(thm)],[cls_conjecture_9]) ).
fof(cls_conjecture_7,axiom,
v_B = v_Aa,
file('theBenchmark.p',cls_conjecture_7) ).
cnf(c_104,plain,
v_B = v_Aa,
inference(clausify,[status(thm)],[cls_conjecture_7]) ).
fof(cls_conjecture_4,axiom,
c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
file('theBenchmark.p',cls_conjecture_4) ).
cnf(c_107,plain,
c_in(c_Event_Oevent_OSays(v_S,v_Aa,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X))))),c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent),
inference(clausify,[status(thm)],[cls_conjecture_4]) ).
fof(cls_conjecture_2,axiom,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
file('theBenchmark.p',cls_conjecture_2) ).
cnf(c_109,plain,
c_in(v_evs3,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)),
inference(clausify,[status(thm)],[cls_conjecture_2]) ).
fof(cls_conjecture_1,axiom,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(c_110,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
cnf(c_111,plain,
~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent),
inference(paramod,[status(thm)],[c_104,c_110]) ).
fof(cls_msg_Osimps_I35_J_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_Message_Omsg_OMPair(VAR_0,VAR_1) != c_Message_Omsg_ONonce(VAR_2),
file('theBenchmark.p',cls_msg_Osimps_I35_J_0) ).
cnf(c_127,plain,
c_Message_Omsg_OMPair(A,B) != c_Message_Omsg_ONonce(C),
inference(clausify,[status(thm)],[cls_msg_Osimps_I35_J_0]) ).
cnf(c_128,plain,
c_Message_Omsg_ONonce(A) != c_Message_Omsg_OMPair(B,C),
inference(copy,[status(thm)],[c_127]) ).
fof(cls_msg_Osimps_I7_J_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_1 = VAR_3
| c_Message_Omsg_OCrypt(VAR_0,VAR_1) != c_Message_Omsg_OCrypt(VAR_2,VAR_3) ),
file('theBenchmark.p',cls_msg_Osimps_I7_J_1) ).
cnf(c_139,plain,
( B = D
| c_Message_Omsg_OCrypt(A,B) != c_Message_Omsg_OCrypt(C,D) ),
inference(clausify,[status(thm)],[cls_msg_Osimps_I7_J_1]) ).
fof(cls_cert__A__form_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,VAR_3),c_Message_Omsg_OMPair(VAR_5,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(VAR_1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,VAR_2),VAR_0)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_4)),tc_Message_Omsg)
| c_in(VAR_3,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(VAR_4,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| VAR_0 = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,VAR_1),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,VAR_2),c_Message_Omsg_OAgent(VAR_3))) ),
file('theBenchmark.p',cls_cert__A__form_1) ).
cnf(c_163,plain,
( ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,D),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,C),A)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,E)),tc_Message_Omsg)
| c_in(D,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(E,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| A = c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,C),c_Message_Omsg_OAgent(D))) ),
inference(clausify,[status(thm)],[cls_cert__A__form_1]) ).
cnf(c_164,plain,
( ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,C),c_Message_Omsg_OMPair(F,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,B),D)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,E)),tc_Message_Omsg)
| c_in(C,c_Event_Obad,tc_Message_Oagent)
| ~ c_in(E,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,B),c_Message_Omsg_OAgent(C))) = D ),
inference(copy,[status(thm)],[c_163]) ).
fof(cls_Says__imp__parts__knows__Spy_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_in(c_Event_Oevent_OSays(VAR_2,VAR_3,VAR_0),c_List_Oset(VAR_1,tc_Event_Oevent),tc_Event_Oevent)
| c_in(VAR_0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1)),tc_Message_Omsg) ),
file('theBenchmark.p',cls_Says__imp__parts__knows__Spy_0) ).
cnf(c_188,plain,
( ~ c_in(c_Event_Oevent_OSays(C,D,A),c_List_Oset(B,tc_Event_Oevent),tc_Event_Oevent)
| c_in(A,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,B)),tc_Message_Omsg) ),
inference(clausify,[status(thm)],[cls_Says__imp__parts__knows__Spy_0]) ).
cnf(c_36272,plain,
( c_Message_Omsg_ONonce(v_Nb) = B
| v_X != c_Message_Omsg_OCrypt(A,B) ),
inference(paramod,[status(thm)],[c_102,c_139]) ).
cnf(c_847,plain,
( c_Message_Omsg_ONonce(v_Nb) = B
| c_Message_Omsg_OCrypt(A,B) != v_X ),
inference(copy,[status(thm)],[c_36272]) ).
cnf(c_862,plain,
( ~ c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,C),c_Message_Omsg_OMPair(E,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,B),D)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg)
| c_in(C,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,A),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,B),c_Message_Omsg_OAgent(C))) = D ),
inference(resolve,[status(thm)],[c_164,c_109]) ).
cnf(c_891,plain,
c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Aa),c_Message_Omsg_OMPair(c_Message_Omsg_ONonce(v_NA),c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),tc_Message_Omsg),
inference(resolve,[status(thm)],[c_188,c_107]) ).
cnf(c_36273,plain,
( c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)
| c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa))) = v_X ),
inference(resolve,[status(thm)],[c_891,c_862]) ).
cnf(c_8628,plain,
c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa))) = v_X,
inference(resolve,[status(thm)],[c_111,c_36273]) ).
cnf(c_36274,plain,
c_Message_Omsg_ONonce(v_Nb) = c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_Ka),c_Message_Omsg_OAgent(v_Aa)),
inference(resolve,[status(thm)],[c_8628,c_847]) ).
cnf(c_36271,plain,
$false,
inference(resolve,[status(thm)],[c_128,c_36274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV792-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n026.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 15:00:55 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 1303948 was started by sandbox on n026,
% 0.12/0.36 % Sat Sep 26 15:00:55 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.38
% 0.12/0.38 % From the command line: assign(max_seconds, 300).
% 259.72/34.85
% 259.72/34.85 % given #500 (I,wt=16): 729 c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(tc_Message_Omsg,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(A),c_Message_Oparts(B),tc_fun(tc_Message_Omsg,tc_bool)) # tptp_name(cls_parts__Un_0) # clausal_fof(1). [assumption].
% 259.72/34.85
% 259.72/34.85 % given #1000 (T,wt=8): 4302 c_in(v_X,c_Set_Oinsert(A,c_Event_Oused(v_evs3),tc_Message_Omsg),tc_Message_Omsg). [resolve(4295,a,378,b)].
% 259.72/34.85
% 259.72/34.85 % given #1500 (F,wt=15): 9013 c_List_OdropWhile(c_Message_Oanalz(c_Set_Oinsert(A,c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),B)),C,D) != c_List_Olist_OCons(c_List_Olist_ONil(tc_Event_Oevent),E,D). [para(4242(a,1),7053(a,1,1,1,2))].
% 259.72/34.85
% 259.72/34.85 % given #2000 (T,wt=7): 12483 c_in(c_Message_OinvKey(v_K),c_Message_OkeysFor(c_Event_Oused(v_evs3)),A). [resolve(12473,a,145,b)].
% 259.72/34.85
% 259.72/34.85 % given #2500 (F,wt=14): 14544 c_List_OdropWhile(c_Message_Oparts(c_Message_OkeysFor(c_Event_Oused(v_evs3))),A,B) != c_List_Olist_OCons(hAPP(c_Public_OshrK,v_Aa),C,B). [resolve(14479,a,587,b)].
% 259.72/34.85
% 259.72/34.85 % given #3000 (T,wt=10): 10320 hBOOL(hAPP(c_Message_Osynth(c_Message_Oparts(c_Set_Oinsert(A,c_Message_Oparts(c_NS__Shared__Mirabelle_Ons__shared),B))),v_evs3)). [resolve(8198,a,1980,b)].
% 259.72/34.85
% 259.72/34.85 % given #3500 (F,wt=15): 18422 c_List_OdropWhile(c_Set_Oinsert(A,c_Message_Oparts(c_Event_Oused(v_evs3)),B),C,D) != c_List_Olist_OCons(c_Message_Omsg_ONonce(v_NA),E,D). [resolve(14744,a,587,b)].
% 259.72/34.85
% 259.72/34.85 % given #4000 (A,wt=22): 1188 c_List_Olength__unique(c_List_Olist_OCons(A,B,C),C) = c_List_Olength__unique(B,C) | c_List_Olist__inter(c_List_Olist_OCons(A,D,C),B,C) = c_List_Olist__inter(D,B,C). [resolve(307,b,303,b)].
% 259.72/34.85
% 259.72/34.85 % given #4500 (T,wt=11): 6176 c_in(v_X,c_Set_Oinsert(A,c_Set_Oinsert(B,c_Event_Oused(v_evs3),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg). [resolve(4302,a,378,b)].
% 259.72/34.85
% 259.72/34.85 % given #5000 (F,wt=18): 21760 c_List_OdropWhile(c_Message_Osynth(c_Lattices_Oupper__semilattice__class_Osup(A,c_Message_Oparts(c_Event_Oused(v_evs3)),tc_fun(tc_Message_Omsg,tc_bool))),B,C) != c_List_Olist_OCons(c_Message_Omsg_ONonce(v_Nb),D,C). [para(7828(a,1),6588(a,1,1,1,2))].
% 259.72/34.85
% 259.72/34.85 % given #5500 (T,wt=11): 14212 c_in(A,c_Message_Oanalz(c_COMBC(c_fequal(B),A,C,D,E)),tc_Message_Omsg). [resolve(5424,a,189,b)].
% 259.72/34.85
% 259.72/34.85 % given #6000 (F,wt=18): 24510 c_List_OdropWhile(c_Message_Oanalz(c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Event_Oused(v_evs3)),A,tc_fun(tc_Message_Omsg,tc_bool))),B,C) != c_List_Olist_OCons(c_Message_Omsg_ONonce(v_NA),D,C). [para(14792(a,1),16473(a,1,1,1,1))].
% 259.72/34.85
% 259.72/34.85 % given #6500 (T,wt=11): 18347 c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Ba),c_Message_Omsg_ONonce(v_NA)),c_Message_Osynth(c_Message_Oparts(c_Event_Oused(v_evs3))),tc_Message_Omsg). [resolve(14589,a,364,b)].
% 259.72/34.85
% 259.72/34.85 % given #7000 (F,wt=14): 27515 c_Message_Osynth(c_Message_Oanalz(c_Set_Oimage(A,c_List_Oset(v_evs3,tc_Event_Oevent),tc_Event_Oevent,tc_Message_Omsg))) != c_List_Oset(c_List_Olist_ONil(tc_Message_Omsg),tc_Message_Omsg). [para(1992(a,1),26564(a,1))].
% 259.72/34.85
% 259.72/34.85 % given #7500 (T,wt=11): 22278 c_in(A,c_Message_Osynth(c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),E)),F). [resolve(12408,a,145,b)].
% 259.72/34.85
% 259.72/34.85 % given #8000 (F,wt=19): 22302 c_List_OdropWhile(c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Set_Oinsert(C,D,E),E),F)),V6,V7) != c_List_Olist_OCons(C,V8,V7). [para(541(a,1),22292(a,1,1,1,2))].
% 259.72/34.85
% 259.72/34.85 % given #8500 (A,wt=16): 2004 c_List_Oappend(A,c_List_Oappend(B,C,D),D) != c_List_Oappend(A,B,D) | c_List_Olist_ONil(D) = C. [para(470(a,1),510(a,1))].
% 259.72/34.85
% 259.72/34.85 % given #9000 (T,wt=11): 29596 c_Set_Oinsert(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),v_evs3),c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared),B) = c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared). [resolve(29588,a,370,b)].
% 259.72/34.85
% 259.72/34.85 % given #9500 (F,wt=19): 29035 c_List_OdropWhile(c_Set_Oinsert(A,c_Message_Oparts(c_Set_Oinsert(B,c_Message_Oanalz(c_Event_Oused(v_evs3)),C)),D),E,F) != c_List_Olist_OCons(c_Message_Omsg_OAgent(v_Ba),V6,F). [para(14750(a,1),21107(a,1,1,2,1,2))].
% 259.72/34.85
% 259.72/34.85 % given #10000 (T,wt=11): 34532 c_in(c_Message_Omsg_OMPair(c_Message_Oagent_OSpy,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(A),c_Message_Omsg_OAgent(B))),c_Message_Osynth(c_Event_Obad),C). [resolve(34513,a,145,b)].
% 259.72/34.85
% 259.72/34.85 % given #10500 (F,wt=14): 35377 c_List_Oset(c_List_Olist_ONil(A),A) != c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs3)),B,tc_fun(A,tc_bool)). [para(4904(a,1),2891(a,2,1))].
% 259.72/34.85
% 259.72/34.85 % SZS status Unsatisfiable for theBenchmark
% 259.72/34.85
% 259.72/34.85 % Proof 1 at 28.52 (+ 5.12) seconds.
% 259.72/34.85 % Length of proof is 17.
% 259.72/34.85 % Level of proof is 4.
% 259.72/34.85 % Maximum clause weight is 41.000.
% 259.72/34.85 % Given clauses 10550.
% 259.72/34.85
% 259.72/34.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------