%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV748-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 : n011.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:02 AM UTC 2026
% Result : Unsatisfiable 21.02s 3.11s
% Output : CNFRefutation 21.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 60 ( 14 unt; 0 def)
% Number of atoms : 147 ( 67 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 132 ( 45 ~; 87 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 16 con; 0-3 aty)
% Number of variables : 35 ( 6 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_conjecture_55,axiom,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_K = v_KAB ),
file('theBenchmark.p',cls_conjecture_55) ).
cnf(c_99,plain,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_K = v_KAB ),
inference(clausify,[status(thm)],[cls_conjecture_55]) ).
cnf(c_12016,plain,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_99]) ).
cnf(c_12017,plain,
( v_KAB = v_K
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12016]) ).
cnf(c_100,plain,
( ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12017]) ).
fof(cls_conjecture_45,axiom,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_K = v_KAB ),
file('theBenchmark.p',cls_conjecture_45) ).
cnf(c_114,plain,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_K = v_KAB ),
inference(clausify,[status(thm)],[cls_conjecture_45]) ).
cnf(c_12018,plain,
( v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_12019,plain,
( v_KAB = v_K
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12018]) ).
cnf(c_115,plain,
( ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| ~ hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12019]) ).
fof(cls_conjecture_44,axiom,
( v_K = v_KAB
| v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) != v_KAB ),
file('theBenchmark.p',cls_conjecture_44) ).
cnf(c_116,plain,
( v_K = v_KAB
| v_K = v_KAB
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) != v_KAB ),
inference(clausify,[status(thm)],[cls_conjecture_44]) ).
cnf(c_12020,plain,
( v_K = v_KAB
| v_KAB = v_K
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) != v_KAB ),
inference(copy,[status(thm)],[c_116]) ).
cnf(c_12021,plain,
( v_KAB = v_K
| v_KAB = v_K
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) != v_KAB ),
inference(copy,[status(thm)],[c_12020]) ).
cnf(c_117,plain,
( v_KAB = v_K
| ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) != v_KAB ),
inference(copy,[status(thm)],[c_12021]) ).
fof(cls_conjecture_32,axiom,
( hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
file('theBenchmark.p',cls_conjecture_32) ).
cnf(c_129,plain,
( hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(clausify,[status(thm)],[cls_conjecture_32]) ).
cnf(c_130,plain,
( hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(copy,[status(thm)],[c_129]) ).
fof(cls_conjecture_24,axiom,
( v_A = v_Aa
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A)))))))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)) ),
file('theBenchmark.p',cls_conjecture_24) ).
cnf(c_136,plain,
( v_A = v_Aa
| hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,v_B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Omsg_OAgent(v_A)))))))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)) ),
inference(clausify,[status(thm)],[cls_conjecture_24]) ).
fof(cls_conjecture_23,axiom,
( v_K = v_KAB
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
file('theBenchmark.p',cls_conjecture_23) ).
cnf(c_137,plain,
( v_K = v_KAB
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(clausify,[status(thm)],[cls_conjecture_23]) ).
cnf(c_138,plain,
( v_KAB = v_K
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(copy,[status(thm)],[c_137]) ).
fof(cls_conjecture_3,axiom,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)),
file('theBenchmark.p',cls_conjecture_3) ).
cnf(c_157,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg)),
inference(clausify,[status(thm)],[cls_conjecture_3]) ).
fof(cls_conjecture_0,axiom,
~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_160,plain,
~ hBOOL(c_in(v_A,c_Event_Obad,tc_Message_Oagent)),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_mem__def_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hBOOL(c_in(VAR_1,VAR_0,VAR_2))
| hBOOL(hAPP(VAR_0,VAR_1)) ),
file('theBenchmark.p',cls_mem__def_0) ).
cnf(c_188,plain,
( ~ hBOOL(c_in(B,A,C))
| hBOOL(hAPP(A,B)) ),
inference(clausify,[status(thm)],[cls_mem__def_0]) ).
fof(cls_mem__def_1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hBOOL(hAPP(VAR_1,VAR_0))
| hBOOL(c_in(VAR_0,VAR_1,VAR_2)) ),
file('theBenchmark.p',cls_mem__def_1) ).
cnf(c_189,plain,
( ~ hBOOL(hAPP(B,A))
| hBOOL(c_in(A,B,C)) ),
inference(clausify,[status(thm)],[cls_mem__def_1]) ).
fof(cls_Oops__parts__spies_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,VAR_2,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,VAR_2),c_Message_Omsg_OMPair(VAR_3,c_Message_Omsg_OMPair(VAR_4,c_Message_Omsg_OMPair(VAR_0,VAR_5))))),c_List_Oset(VAR_1,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(VAR_0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1)),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_Oops__parts__spies_0) ).
cnf(c_244,plain,
( ~ hBOOL(c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,C,c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,C),c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(E,c_Message_Omsg_OMPair(A,F))))),c_List_Oset(B,tc_Event_Oevent),tc_Event_Oevent))
| hBOOL(c_in(A,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,B)),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_Oops__parts__spies_0]) ).
fof(cls_parts_OInj_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_0,VAR_1,tc_Message_Omsg))
| hBOOL(c_in(VAR_0,c_Message_Oparts(VAR_1),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_parts_OInj_0) ).
cnf(c_283,plain,
( ~ hBOOL(c_in(A,B,tc_Message_Omsg))
| hBOOL(c_in(A,c_Message_Oparts(B),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_parts_OInj_0]) ).
fof(cls_parts__analz_0,axiom,
! [VAR_0] : c_Message_Oparts(c_Message_Oanalz(VAR_0)) = c_Message_Oparts(VAR_0),
file('theBenchmark.p',cls_parts__analz_0) ).
cnf(c_285,plain,
c_Message_Oparts(c_Message_Oanalz(A)) = c_Message_Oparts(A),
inference(clausify,[status(thm)],[cls_parts__analz_0]) ).
fof(cls_usedI_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(c_in(VAR_0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,VAR_1)),tc_Message_Omsg))
| hBOOL(c_in(VAR_0,c_Event_Oused(VAR_1),tc_Message_Omsg)) ),
file('theBenchmark.p',cls_usedI_0) ).
cnf(c_311,plain,
( ~ hBOOL(c_in(A,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,B)),tc_Message_Omsg))
| hBOOL(c_in(A,c_Event_Oused(B),tc_Message_Omsg)) ),
inference(clausify,[status(thm)],[cls_usedI_0]) ).
cnf(c_12022,plain,
( v_KAB = v_K
| hAPP(c_Public_OshrK,v_Ba) != v_KAB
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_138,c_117]) ).
cnf(c_781,plain,
( hAPP(c_Public_OshrK,v_Ba) != v_KAB
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12022]) ).
cnf(c_12023,plain,
( hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_138,c_100]) ).
cnf(c_782,plain,
( hAPP(c_Public_OshrK,v_Ba) = v_KAB
| hBOOL(c_in(v_Ba,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12023]) ).
cnf(c_872,plain,
( v_A = v_Aa
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) ),
inference(resolve,[status(thm)],[c_244,c_136]) ).
cnf(c_12024,plain,
( hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Message_Oparts(c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2))),tc_Message_Omsg)) ),
inference(resolve,[status(thm)],[c_283,c_130]) ).
cnf(c_925,plain,
( hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) ),
inference(paramod,[status(thm)],[c_285,c_12024]) ).
cnf(c_12025,plain,
( ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| v_KAB = v_K
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_782,c_115]) ).
cnf(c_5125,plain,
( ~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent))
| hAPP(c_Public_OshrK,v_Ba) = v_KAB
| v_KAB = v_K ),
inference(copy,[status(thm)],[c_12025]) ).
cnf(c_8640,plain,
( hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg))
| v_A = v_Aa ),
inference(resolve,[status(thm)],[c_872,c_311]) ).
cnf(c_12026,plain,
( hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_KAB),c_Event_Oused(v_evs2),tc_Message_Omsg))
| hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)) ),
inference(resolve,[status(thm)],[c_925,c_311]) ).
cnf(c_11142,plain,
hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)),
inference(resolve,[status(thm)],[c_157,c_12026]) ).
cnf(c_11143,plain,
( hAPP(c_Public_OshrK,v_Ba) = v_KAB
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_11142,c_5125]) ).
cnf(c_11167,plain,
hBOOL(hAPP(c_Event_Obad,v_Aa)),
inference(resolve,[status(thm)],[c_11142,c_188]) ).
cnf(c_11174,plain,
hBOOL(c_in(v_Aa,c_Event_Obad,A)),
inference(resolve,[status(thm)],[c_11167,c_189]) ).
cnf(c_12027,plain,
( v_KAB = v_K
| v_KAB = v_K ),
inference(resolve,[status(thm)],[c_11143,c_781]) ).
cnf(c_11345,plain,
v_KAB = v_K,
inference(copy,[status(thm)],[c_12027]) ).
cnf(c_12003,plain,
~ hBOOL(c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Event_Oused(v_evs2),tc_Message_Omsg)),
inference(paramod,[status(thm)],[c_11345,c_157]) ).
cnf(c_12006,plain,
v_A = v_Aa,
inference(resolve,[status(thm)],[c_12003,c_8640]) ).
cnf(c_12028,plain,
~ hBOOL(c_in(v_Aa,c_Event_Obad,tc_Message_Oagent)),
inference(paramod,[status(thm)],[c_12006,c_160]) ).
cnf(c_12015,plain,
$false,
inference(resolve,[status(thm)],[c_11174,c_12028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV748-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 14:53:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 830867 was started by sandbox2 on n011,
% 0.09/0.36 % Sat Sep 26 14:53:45 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 21.02/3.11
% 21.02/3.11 % given #500 (F,wt=12): 2357 c_Message_Oparts(c_Set_Oinsert(c_Message_Omsg_OCrypt(A,B),C,tc_Message_Omsg)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(479(a,1),627(a,1))].
% 21.02/3.11
% 21.02/3.11 % given #1000 (T,wt=7): 5307 hBOOL(hAPP(c_Message_Osynth(c_Message_Oanalz(c_Message_Osynth(c_Message_OsymKeys))),v_KAB)). [resolve(3928,a,188,b)].
% 21.02/3.11
% 21.02/3.11 % given #1500 (F,wt=19): 4254 c_Message_Oparts(c_Message_Osynth(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Message_Oanalz(c_Set_Oinsert(c_Message_Omsg_OAgent(C),D,tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg))) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(456(a,1),3317(a,1,1,1,2,2))].
% 21.02/3.11
% 21.02/3.11 % given #2000 (T,wt=10): 3325 hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oanalz(c_NS__Shared__Mirabelle_Ons__shared),A,tc_fun(B,tc_bool)),v_evs2)). [resolve(3303,a,578,b)].
% 21.02/3.11
% 21.02/3.11 % SZS status Unsatisfiable for theBenchmark
% 21.02/3.11
% 21.02/3.11 % Proof 1 at 2.17 (+ 0.47) seconds.
% 21.02/3.11 % Length of proof is 33.
% 21.02/3.11 % Level of proof is 8.
% 21.02/3.11 % Maximum clause weight is 35.000.
% 21.02/3.11 % Given clauses 2188.
% 21.02/3.11
% 21.02/3.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------