%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV724-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:00 AM UTC 2026
% Result : Unsatisfiable 54.23s 7.38s
% Output : CNFRefutation 54.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 22 ( 7 unt; 0 def)
% Number of atoms : 39 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 16 ~; 17 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 19 ( 3 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_2,axiom,
( hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_conjecture_2) ).
cnf(c_89,plain,
( hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_conjecture_2]) ).
fof(cls_conjecture_1,axiom,
( ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg))
| ~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(c_90,plain,
( ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg))
| ~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
fof(cls_conjecture_0,axiom,
hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_91,plain,
hBOOL(c_in(v_evs,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_Spy__spies__bad__shrK_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_0,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,VAR_0)),c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_Spy__spies__bad__shrK_0) ).
cnf(c_97,plain,
( ~ hBOOL(c_in(A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,A)),c_Event_Oknows(c_Message_Oagent_OSpy,B),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_Spy__spies__bad__shrK_0]) ).
fof(cls_analz_OInj_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_0,VAR_1,tc_Message_Omsg))
| hBOOL(c_in(VAR_0,c_Message_Oanalz(VAR_1),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_analz_OInj_0) ).
cnf(c_100,plain,
( ~ hBOOL(c_in(A,B,tc_Message_Omsg))
| hBOOL(c_in(A,c_Message_Oanalz(B),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_analz_OInj_0]) ).
fof(cls_Spy__see__shrK_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_1,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,VAR_0)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1)),tc_Message_Omsg))
| hBOOL(c_in(VAR_0,c_Event_Obad,tc_Message_Oagent)) ),
file('theBenchmark.p',cls_Spy__see__shrK_0) ).
cnf(c_102,plain,
( ~ hBOOL(c_in(B,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent)))
| ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,B)),tc_Message_Omsg))
| hBOOL(c_in(A,c_Event_Obad,tc_Message_Oagent)) ),
inference(clausify,[status(thm)],[cls_Spy__see__shrK_0]) ).
fof(cls_analz__conj__parts_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_0,c_Message_Oanalz(VAR_1),tc_Message_Omsg))
| hBOOL(c_in(VAR_0,c_Message_Oparts(VAR_1),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_analz__conj__parts_0) ).
cnf(c_121,plain,
( ~ hBOOL(c_in(A,c_Message_Oanalz(B),tc_Message_Omsg))
| hBOOL(c_in(A,c_Message_Oparts(B),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_analz__conj__parts_0]) ).
cnf(c_724,plain,
( ~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg))
| hBOOL(c_in(A,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolve,[status(thm)],[c_102,c_91]) ).
cnf(c_744,plain,
( hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)) ),
inference(resolve,[status(thm)],[c_121,c_89]) ).
cnf(c_18809,plain,
( hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolve,[status(thm)],[c_744,c_724]) ).
cnf(c_5312,plain,
hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
inference(copy,[status(thm)],[c_18809]) ).
cnf(c_5313,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg)),
inference(resolve,[status(thm)],[c_5312,c_90]) ).
cnf(c_5328,plain,
hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Event_Oknows(c_Message_Oagent_OSpy,A),tc_Message_Omsg)),
inference(resolve,[status(thm)],[c_5312,c_97]) ).
cnf(c_18807,plain,
hBOOL(c_in(hAPP(c_Message_Omsg_OKey,hAPP(c_Public_OshrK,v_A)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)),
inference(resolve,[status(thm)],[c_5328,c_100]) ).
cnf(c_18808,plain,
$false,
inference(resolve,[status(thm)],[c_18807,c_5313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV724-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 14:52:54 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 3138936 was started by sandbox2 on n003,
% 0.11/0.37 % Sat Sep 26 14:52:54 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.39
% 0.11/0.39 % From the command line: assign(max_seconds, 300).
% 54.23/7.38
% 54.23/7.38 % given #500 (T,wt=6): 1710 hBOOL(hAPP(c_Message_Osynth(A),c_Message_Omsg_OAgent(B))). [resolve(520,a,93,b)].
% 54.23/7.38
% 54.23/7.38 % given #1000 (F,wt=22): 3434 c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Message_Oanalz(c_Set_Oinsert(C,c_Set_Oinsert(c_Message_Omsg_OMPair(D,E),F,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(572(a,1),2803(a,1,1,2,2,1))].
% 54.23/7.38
% 54.23/7.38 % given #1500 (T,wt=9): 3848 hBOOL(c_in(c_Message_Oagent_OSpy,c_Set_Oinsert(A,c_Message_Oanalz(c_Event_Obad),B),C)). [resolve(2635,a,94,b)].
% 54.23/7.38
% 54.23/7.38 % given #2000 (F,wt=23): 7270 c_Message_Oanalz(c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,c_Message_Osynth(D),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool))) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(548(a,1),6799(a,1,1,2))].
% 54.23/7.38
% 54.23/7.38 % given #2500 (T,wt=10): 4475 hBOOL(hAPP(c_Set_Oinsert(A,c_Message_Oanalz(c_Message_Osynth(c_Event_Obad)),B),c_Message_Omsg_OHash(c_Message_Oagent_OSpy))). [resolve(4474,a,516,b)].
% 54.23/7.38
% 54.23/7.38 % given #3000 (F,wt=22): 14670 c_Message_Oanalz(c_Message_Osynth(c_Set_Oinsert(A,c_Message_Oanalz(c_Set_Oinsert(B,c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(c_Message_Osynth(C),D,tc_fun(tc_Message_Omsg,tc_bool))),tc_Message_Omsg)),tc_Message_Omsg))) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(378(a,1),14667(a,1,1,1,2,1,2,1))].
% 54.23/7.38
% 54.23/7.38 % given #3500 (T,wt=10): 9775 hBOOL(hAPP(c_Message_Oparts(c_Message_Osynth(c_Set_Oinsert(A,c_Message_Oparts(c_Event_Obad),B))),v_A)). [resolve(5680,a,1311,b)].
% 54.23/7.38
% 54.23/7.38 % given #4000 (F,wt=20): 17287 c_Message_Oparts(c_Message_Osynth(c_Message_Oanalz(c_Set_Oinsert(A,c_Set_Oinsert(c_Message_Omsg_OHash(B),c_Set_Oinsert(C,c_Message_Osynth(D),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)))) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(572(a,1),17271(a,1,1,1,1))].
% 54.23/7.38
% 54.23/7.38 % given #4500 (A,wt=32): 1223 hBOOL(c_in(A,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(B,C,tc_Event_Oevent))),tc_Message_Omsg)) | -hBOOL(c_in(c_Event_Oevent_OSays(D,E,c_Message_Omsg_OCrypt(F,c_Message_Omsg_OMPair(V6,c_Message_Omsg_OMPair(V7,c_Message_Omsg_OMPair(V8,A))))),c_Set_Oinsert(B,c_List_Oset(C,tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)). [para(216(a,1),417(b,1,2))].
% 54.23/7.38
% 54.23/7.38 % SZS status Unsatisfiable for theBenchmark
% 54.23/7.38
% 54.23/7.38 % Proof 1 at 5.65 (+ 1.25) seconds.
% 54.23/7.38 % Length of proof is 14.
% 54.23/7.38 % Level of proof is 5.
% 54.23/7.38 % Maximum clause weight is 23.000.
% 54.23/7.38 % Given clauses 4697.
% 54.23/7.38
% 54.23/7.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------