%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV791-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 : n010.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 163.67s 22.31s
% Output : CNFRefutation 163.67s
% 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; 17 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_100,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_102,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(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_105,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(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_107,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_108,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
cnf(c_109,plain,
~ c_in(v_Aa,c_Event_Obad,tc_Message_Oagent),
inference(paramod,[status(thm)],[c_102,c_108]) ).
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_143,plain,
c_Message_Omsg_OMPair(A,B) != c_Message_Omsg_ONonce(C),
inference(clausify,[status(thm)],[cls_msg_Osimps_I35_J_0]) ).
cnf(c_144,plain,
c_Message_Omsg_ONonce(A) != c_Message_Omsg_OMPair(B,C),
inference(copy,[status(thm)],[c_143]) ).
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_166,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(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(c_Message_Omsg_OKey(VAR_2),c_Message_Omsg_OAgent(VAR_3))) ),
file('theBenchmark.p',cls_cert__A__form_1) ).
cnf(c_201,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(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(c_Message_Omsg_OKey(C),c_Message_Omsg_OAgent(D))) ),
inference(clausify,[status(thm)],[cls_cert__A__form_1]) ).
cnf(c_202,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(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(c_Message_Omsg_OKey(B),c_Message_Omsg_OAgent(C))) = D ),
inference(copy,[status(thm)],[c_201]) ).
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_264,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_29108,plain,
( c_Message_Omsg_ONonce(v_Nb) = B
| v_X != c_Message_Omsg_OCrypt(A,B) ),
inference(paramod,[status(thm)],[c_100,c_166]) ).
cnf(c_792,plain,
( c_Message_Omsg_ONonce(v_Nb) = B
| c_Message_Omsg_OCrypt(A,B) != v_X ),
inference(copy,[status(thm)],[c_29108]) ).
cnf(c_831,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(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(c_Message_Omsg_OKey(B),c_Message_Omsg_OAgent(C))) = D ),
inference(resolve,[status(thm)],[c_202,c_107]) ).
cnf(c_881,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(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_264,c_105]) ).
cnf(c_29109,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(c_Message_Omsg_OKey(v_Ka),c_Message_Omsg_OAgent(v_Aa))) = v_X ),
inference(resolve,[status(thm)],[c_881,c_831]) ).
cnf(c_12929,plain,
c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_Ba),c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_Ka),c_Message_Omsg_OAgent(v_Aa))) = v_X,
inference(resolve,[status(thm)],[c_109,c_29109]) ).
cnf(c_29110,plain,
c_Message_Omsg_ONonce(v_Nb) = c_Message_Omsg_OMPair(c_Message_Omsg_OKey(v_Ka),c_Message_Omsg_OAgent(v_Aa)),
inference(resolve,[status(thm)],[c_12929,c_792]) ).
cnf(c_29107,plain,
$false,
inference(resolve,[status(thm)],[c_144,c_29110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV791-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n010.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sat Sep 26 14:58:15 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.46 % Process 3581286 was started by sandbox on n010,
% 0.20/0.46 % Sat Sep 26 14:58:15 2026
% 0.20/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.20/0.48
% 0.20/0.48 % From the command line: assign(max_seconds, 300).
% 163.67/22.31
% 163.67/22.31 % given #500 (I,wt=20): 694 c_lessequals(c_Message_Oparts(c_Set_Oinsert(A,B,tc_Message_Omsg)),c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(C,B,tc_fun(tc_Message_Omsg,tc_bool))),tc_fun(tc_Message_Omsg,tc_bool)) | -c_in(A,C,tc_Message_Omsg). [back_rewrite(592),rewrite([665(9)])].
% 163.67/22.31
% 163.67/22.31 % given #1000 (F,wt=14): 6100 c_List_OdropWhile(c_Message_Oanalz(c_Set_Oinsert(c_Message_Omsg_OAgent(A),c_NS__Shared__Mirabelle_Ons__shared,tc_Message_Omsg)),B,C) != c_List_Olist_OCons(v_evs3,D,C). [para(449(a,1),6052(a,1,1))].
% 163.67/22.31
% 163.67/22.31 % given #1500 (A,wt=20): 830 c_List_Orev(c_List_Olist_OCons(A,c_List_Orev(B,C),C),C) != c_List_Orev(c_List_Olist_OCons(D,c_List_Orev(E,C),C),C) | A = D. [back_rewrite(232),rewrite([824(3),824(6)])].
% 163.67/22.31
% 163.67/22.31 % given #2000 (T,wt=9): 9949 hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Set_Oinsert(A,c_Event_Obad,B))),c_Message_Oagent_OSpy)). [resolve(1647,b,7187,a)].
% 163.67/22.31
% 163.67/22.31 % given #2500 (F,wt=13): 15339 c_List_OdropWhile(c_Message_OkeysFor(c_Message_Oparts(c_Event_Oused(v_evs3))),A,B) != c_List_Olist_OCons(c_Message_OinvKey(v_K),C,B). [resolve(15260,a,371,b)].
% 163.67/22.31
% 163.67/22.31 % given #3000 (T,wt=8): 17098 hBOOL(hAPP(c_Message_Oanalz(c_Event_Oused(c_List_Orev(v_evs3,tc_Event_Oevent))),v_X)). [resolve(17063,a,1647,b)].
% 163.67/22.31
% 163.67/22.31 % given #3500 (F,wt=15): 18847 c_List_OdropWhile(c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(c_Event_Obad,A,tc_fun(B,tc_bool))),C,D) != c_List_Olist_OCons(c_Message_Oagent_OSpy,E,D). [para(651(a,1),18829(a,1,1,1))].
% 163.67/22.31
% 163.67/22.31 % given #4000 (T,wt=10): 13068 c_List_Orev(A,B) != c_List_Orev(C,B) | C = A. [para(115(a,1),883(a,2,1)),rewrite([190(4),188(5)])].
% 163.67/22.31
% 163.67/22.31 % given #4500 (F,wt=15): 21785 c_List_OdropWhile(c_Message_Osynth(c_Message_OkeysFor(c_Message_Oparts(c_Message_Osynth(c_Event_Oused(v_evs3))))),A,B) != c_List_Olist_OCons(c_Message_OinvKey(v_K),C,B). [resolve(15717,a,371,b)].
% 163.67/22.31
% 163.67/22.31 % given #5000 (T,wt=10): 18960 c_in(c_Message_Omsg_OAgent(A),c_Message_Oanalz(c_Set_Oinsert(B,c_Message_Osynth(C),D)),E). [resolve(10331,a,172,b)].
% 163.67/22.31
% 163.67/22.31 % given #5500 (F,wt=18): 25063 c_List_OdropWhile(c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Message_Osynth(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared)),C),C)),D,E) != c_List_Olist_OCons(v_evs3,F,E). [para(3687(a,1),10447(a,1,1,1,2,2))].
% 163.67/22.31
% 163.67/22.31 % given #6000 (A,wt=27): 1415 c_Message_Oparts(c_Set_Oinsert(c_Message_Omsg_OKey(A),B,tc_Message_Omsg)) != c_Set_Oinsert(c_Message_Omsg_OKey(A),C,tc_Message_Omsg) | c_in(c_Message_Omsg_OKey(A),C,tc_Message_Omsg) | c_in(c_Message_Omsg_OKey(A),c_Message_Oparts(B),tc_Message_Omsg) | c_Message_Oparts(B) = C. [para(459(a,1),378(a,1))].
% 163.67/22.31
% 163.67/22.31 % given #6500 (T,wt=11): 8753 c_in(A,c_Set_Oinsert(B,c_Message_Oparts(c_Set_Oinsert(A,C,tc_Message_Omsg)),D),D). [resolve(7363,a,385,b)].
% 163.67/22.31
% 163.67/22.31 % given #7000 (F,wt=15): 28998 c_List_OdropWhile(c_Message_OkeysFor(c_Message_Osynth(c_Message_Oparts(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool))))),B,C) != c_List_Olist_OCons(D,E,C). [resolve(28989,a,371,b)].
% 163.67/22.31
% 163.67/22.31 % SZS status Unsatisfiable for theBenchmark
% 163.67/22.31
% 163.67/22.31 % Proof 1 at 17.66 (+ 3.84) seconds.
% 163.67/22.31 % Length of proof is 17.
% 163.67/22.31 % Level of proof is 4.
% 163.67/22.31 % Maximum clause weight is 39.000.
% 163.67/22.31 % Given clauses 7049.
% 163.67/22.31
% 163.67/22.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------