%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV796-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 : n012.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 130.96s 17.96s
% Output : CNFRefutation 130.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 10
% Syntax : Number of formulae : 44 ( 29 unt; 0 def)
% Number of atoms : 64 ( 39 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 28 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 141 ( 57 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_bot1E_0,axiom,
! [VAR_0,VAR_1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(VAR_0,tc_bool)),VAR_1)),
file('theBenchmark.p',cls_bot1E_0) ).
cnf(c_116,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B)),
inference(clausify,[status(thm)],[cls_bot1E_0]) ).
fof(cls_keymode_Oinduct_0,axiom,
! [VAR_0,VAR_1] :
( ~ hBOOL(hAPP(VAR_0,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(VAR_0,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(VAR_0,VAR_1)) ),
file('theBenchmark.p',cls_keymode_Oinduct_0) ).
cnf(c_142,plain,
( ~ hBOOL(hAPP(A,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(A,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(A,B)) ),
inference(clausify,[status(thm)],[cls_keymode_Oinduct_0]) ).
fof(cls_eq__Nil__appendI_0,axiom,
! [VAR_0,VAR_1] : VAR_0 = c_List_Oappend(c_List_Olist_ONil(VAR_1),VAR_0,VAR_1),
file('theBenchmark.p',cls_eq__Nil__appendI_0) ).
cnf(c_156,plain,
A = c_List_Oappend(c_List_Olist_ONil(B),A,B),
inference(clausify,[status(thm)],[cls_eq__Nil__appendI_0]) ).
cnf(c_157,plain,
c_List_Oappend(c_List_Olist_ONil(A),B,A) = B,
inference(copy,[status(thm)],[c_156]) ).
fof(cls_append__eq__Cons__conv_5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : c_List_Oappend(c_List_Olist_OCons(VAR_0,VAR_1,VAR_2),VAR_3,VAR_2) = c_List_Olist_OCons(VAR_0,c_List_Oappend(VAR_1,VAR_3,VAR_2),VAR_2),
file('theBenchmark.p',cls_append__eq__Cons__conv_5) ).
cnf(c_204,plain,
c_List_Oappend(c_List_Olist_OCons(A,B,C),D,C) = c_List_Olist_OCons(A,c_List_Oappend(B,D,C),C),
inference(clausify,[status(thm)],[cls_append__eq__Cons__conv_5]) ).
fof(cls_neq__Nil__conv_1,axiom,
! [VAR_0,VAR_1,VAR_2] : c_List_Olist_OCons(VAR_0,VAR_1,VAR_2) != c_List_Olist_ONil(VAR_2),
file('theBenchmark.p',cls_neq__Nil__conv_1) ).
cnf(c_212,plain,
c_List_Olist_OCons(A,B,C) != c_List_Olist_ONil(C),
inference(clausify,[status(thm)],[cls_neq__Nil__conv_1]) ).
fof(cls_append__self__conv2_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = c_List_Olist_ONil(VAR_2)
| c_List_Oappend(VAR_0,VAR_1,VAR_2) != VAR_1 ),
file('theBenchmark.p',cls_append__self__conv2_0) ).
cnf(c_303,plain,
( A = c_List_Olist_ONil(C)
| c_List_Oappend(A,B,C) != B ),
inference(clausify,[status(thm)],[cls_append__self__conv2_0]) ).
cnf(c_304,plain,
( c_List_Olist_ONil(C) = A
| c_List_Oappend(A,B,C) != B ),
inference(copy,[status(thm)],[c_303]) ).
fof(cls_insert__code_1,axiom,
! [VAR_0,VAR_1,VAR_2] : hBOOL(hAPP(c_Set_Oinsert(VAR_0,VAR_1,VAR_2),VAR_0)),
file('theBenchmark.p',cls_insert__code_1) ).
cnf(c_474,plain,
hBOOL(hAPP(c_Set_Oinsert(A,B,C),A)),
inference(clausify,[status(thm)],[cls_insert__code_1]) ).
fof(cls_insert__code_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ hBOOL(hAPP(c_Set_Oinsert(VAR_2,VAR_0,VAR_3),VAR_1))
| VAR_2 = VAR_1
| hBOOL(hAPP(VAR_0,VAR_1)) ),
file('theBenchmark.p',cls_insert__code_0) ).
cnf(c_477,plain,
( ~ hBOOL(hAPP(c_Set_Oinsert(C,A,D),B))
| C = B
| hBOOL(hAPP(A,B)) ),
inference(clausify,[status(thm)],[cls_insert__code_0]) ).
fof(cls_insert__code_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ hBOOL(hAPP(VAR_1,VAR_3))
| hBOOL(hAPP(c_Set_Oinsert(VAR_0,VAR_1,VAR_2),VAR_3)) ),
file('theBenchmark.p',cls_insert__code_2) ).
cnf(c_482,plain,
( ~ hBOOL(hAPP(B,D))
| hBOOL(hAPP(c_Set_Oinsert(A,B,C),D)) ),
inference(clausify,[status(thm)],[cls_insert__code_2]) ).
fof(cls_not__Cons__self_0,axiom,
! [VAR_0,VAR_1,VAR_2] : VAR_0 != c_List_Olist_OCons(VAR_1,VAR_0,VAR_2),
file('theBenchmark.p',cls_not__Cons__self_0) ).
cnf(c_549,plain,
A != c_List_Olist_OCons(B,A,C),
inference(clausify,[status(thm)],[cls_not__Cons__self_0]) ).
cnf(c_550,plain,
c_List_Olist_OCons(A,B,C) != B,
inference(copy,[status(thm)],[c_549]) ).
cnf(c_34662,plain,
( c_List_Olist_ONil(D) = c_List_Olist_OCons(A,B,D)
| c_List_Olist_OCons(A,c_List_Oappend(B,C,D),D) != C ),
inference(paramod,[status(thm)],[c_204,c_304]) ).
cnf(c_34663,plain,
( c_List_Olist_OCons(A,B,D) = c_List_Olist_ONil(D)
| c_List_Olist_OCons(A,c_List_Oappend(B,C,D),D) != C ),
inference(copy,[status(thm)],[c_34662]) ).
cnf(c_1097,plain,
c_List_Olist_OCons(A,c_List_Oappend(B,C,D),D) != C,
inference(resolve,[status(thm)],[c_212,c_34663]) ).
cnf(c_1733,plain,
( ~ hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,A,B),c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,A,B),C)) ),
inference(resolve,[status(thm)],[c_474,c_142]) ).
cnf(c_1840,plain,
hBOOL(hAPP(c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),E),B)),
inference(resolve,[status(thm)],[c_482,c_474]) ).
cnf(c_2664,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Oappend(C,D,E),E),E) != D,
inference(paramod,[status(thm)],[c_204,c_1097]) ).
cnf(c_2748,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,C,D),D) != C,
inference(paramod,[status(thm)],[c_157,c_2664]) ).
cnf(c_2749,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Olist_OCons(C,c_List_Oappend(D,E,F),F),F),F) != E,
inference(paramod,[status(thm)],[c_204,c_2664]) ).
cnf(c_2943,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Olist_OCons(C,D,E),E),E) != D,
inference(paramod,[status(thm)],[c_157,c_2749]) ).
cnf(c_27390,plain,
hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,c_Set_Oinsert(c_Public_Okeymode_OEncryption,A,B),C),D)),
inference(resolve,[status(thm)],[c_1733,c_1840]) ).
cnf(c_27406,plain,
( c_Public_Okeymode_OSignature = C
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,A,B),C)) ),
inference(resolve,[status(thm)],[c_27390,c_477]) ).
cnf(c_27426,plain,
( c_Public_Okeymode_OEncryption = A
| hBOOL(hAPP(B,A))
| c_Public_Okeymode_OSignature = A ),
inference(resolve,[status(thm)],[c_27406,c_477]) ).
cnf(c_27443,plain,
( c_Public_Okeymode_OEncryption = A
| c_Public_Okeymode_OSignature = A ),
inference(resolve,[status(thm)],[c_27426,c_116]) ).
cnf(c_34664,plain,
D != c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Olist_OCons(C,D,E),E),E),
inference(copy,[status(thm)],[c_2943]) ).
cnf(c_34665,plain,
c_Public_Okeymode_OEncryption = c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Olist_OCons(C,c_Public_Okeymode_OSignature,D),D),D),
inference(resolve,[status(thm)],[c_27443,c_34664]) ).
cnf(c_27454,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_List_Olist_OCons(C,c_Public_Okeymode_OSignature,D),D),D) = c_Public_Okeymode_OEncryption,
inference(copy,[status(thm)],[c_34665]) ).
cnf(c_34666,plain,
B != c_List_Olist_OCons(A,B,C),
inference(copy,[status(thm)],[c_550]) ).
cnf(c_34667,plain,
c_Public_Okeymode_OEncryption = c_List_Olist_OCons(A,c_Public_Okeymode_OSignature,B),
inference(resolve,[status(thm)],[c_27443,c_34666]) ).
cnf(c_27462,plain,
c_List_Olist_OCons(A,c_Public_Okeymode_OSignature,B) = c_Public_Okeymode_OEncryption,
inference(copy,[status(thm)],[c_34667]) ).
cnf(c_34668,plain,
c_List_Olist_OCons(A,c_List_Olist_OCons(B,c_Public_Okeymode_OEncryption,D),D) = c_Public_Okeymode_OEncryption,
inference(paramod,[status(thm)],[c_27462,c_27454]) ).
cnf(c_34661,plain,
$false,
inference(resolve,[status(thm)],[c_2748,c_34668]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV796-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.34 % Computer : n012.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 14:58:34 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 873534 was started by sandbox2 on n012,
% 0.09/0.35 % Sat Sep 26 14:58:34 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 130.96/17.96
% 130.96/17.96 % given #500 (I,wt=70): 734 -hBOOL(c_in(A,c_NS__Shared__Mirabelle_Ons__shared,tc_List_Olist(tc_Event_Oevent))) | hBOOL(c_in(B,c_Event_Obad,tc_Message_Oagent)) | hBOOL(c_in(hAPP(c_Message_Omsg_OKey,C),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)) | -hBOOL(c_in(c_Message_Omsg_OCrypt(hAPP(c_Public_OshrK,B),c_Message_Omsg_OMPair(D,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(B),c_Message_Omsg_OMPair(hAPP(c_Message_Omsg_OKey,C),E)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)) | -hBOOL(c_in(c_Message_Omsg_OCrypt(C,c_Message_Omsg_ONonce(F)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,A)),tc_Message_Omsg)) | hBOOL(c_in(c_Event_Oevent_OSays(B,B,v_sko__NS__Shared__Mirabelle__XIssues__def__1(B,B,c_Message_Omsg_OCrypt(C,c_Message_Omsg_ONonce(F)),A)),c_List_Oset(A,tc_Event_Oevent),tc_Event_Oevent)). [factor(712,b,c)].
% 130.96/17.96
% 130.96/17.96 % given #1000 (F,wt=21): 3644 c_List_Olist_OCons(A,c_List_Oappend(B,c_List_Olist_OCons(C,c_List_Oappend(D,c_List_Oappend(E,c_List_Olist_OCons(F,V6,V7),V7),V7),V7),V7),V7) != V6. [para(333(a,1),3081(a,1,2,2,2))].
% 130.96/17.96
% 130.96/17.96 % given #1500 (T,wt=9): 2674 hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(A,c_Event_Obad,tc_fun(B,tc_bool)),c_Message_Oagent_OSpy)). [resolve(2368,a,176,b)].
% 130.96/17.96
% 130.96/17.96 % given #2000 (F,wt=20): 11416 c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Lattices_Oupper__semilattice__class_Osup(C,c_Message_Oparts(c_Message_Osynth(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(152(a,1),11412(a,1,1,2))].
% 130.96/17.96
% 130.96/17.96 % given #2500 (T,wt=9): 10331 hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_NS__Shared__Mirabelle_Ons__shared)),c_Message_Omsg_OHash(c_Message_Omsg_OMPair(v_evs,v_evs)))). [resolve(10293,a,1176,b)].
% 130.96/17.96
% 130.96/17.96 % given #3000 (F,wt=19): 16729 c_Message_Oparts(c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oimage(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),B,tc_Message_Omsg),C,tc_fun(tc_Message_Omsg,tc_bool))) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(215(a,1),16722(a,1,1))].
% 130.96/17.96
% 130.96/17.96 % given #3500 (A,wt=20): 1162 c_lessequals(A,c_Message_Osynth(c_Set_Oinsert(B,C,tc_Message_Omsg)),tc_fun(tc_Message_Omsg,tc_bool)) | -c_lessequals(A,c_Set_Oinsert(B,c_Message_Osynth(C),tc_Message_Omsg),tc_fun(tc_Message_Omsg,tc_bool)). [resolve(315,b,170,a)].
% 130.96/17.96
% 130.96/17.96 % given #4000 (T,wt=9): 19290 hBOOL(hAPP(c_Message_Osynth(c_Set_Oinsert(A,c_Event_Obad,B)),c_Message_Omsg_OHash(c_Message_Oagent_OSpy))). [resolve(10395,a,668,b)].
% 130.96/17.96
% 130.96/17.96 % given #4500 (F,wt=26): 15462 c_Message_Oanalz(c_Set_Oinsert(A,c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Set_Oinsert(B,c_Lattices_Oupper__semilattice__class_Osup(C,c_Message_Oanalz(c_Message_Osynth(D)),tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)),E,tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(153(a,1),15403(a,1,1))].
% 130.96/17.96
% 130.96/17.96 % given #5000 (T,wt=10): 17603 hBOOL(hAPP(c_Message_Oanalz(c_Message_Osynth(c_Message_OinvKey)),c_Message_Omsg_OHash(hAPP(c_Message_OinvKey,c_Orderings_Otop__class_Otop(tc_bool))))). [resolve(17578,a,1176,b)].
% 130.96/17.96
% 130.96/17.96 % given #5500 (F,wt=24): 23021 c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Set_Oinsert(C,c_Set_Oinsert(D,c_Message_Oparts(c_Set_Oinsert(E,c_Message_Osynth(c_Event_Obad),tc_Message_Omsg)),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(4023(a,1),16161(a,1,1,2,2,2,2,1,2))].
% 130.96/17.96
% 130.96/17.96 % given #6000 (T,wt=10): 24133 hBOOL(c_in(A,c_Message_Oparts(c_Message_OkeysFor(c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)))),C)). [resolve(24124,a,667,b)].
% 130.96/17.96
% 130.96/17.96 % given #6500 (F,wt=28): 15111 c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Set_Oinsert(C,c_Lattices_Oupper__semilattice__class_Osup(D,c_Lattices_Oupper__semilattice__class_Osup(E,c_Message_Oparts(c_Message_Osynth(F)),tc_fun(tc_Message_Omsg,tc_bool)),tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg),tc_Message_Omsg),tc_Message_Omsg)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(195(a,1),11463(a,1,1,2,2,2))].
% 130.96/17.96
% 130.96/17.96 % given #7000 (T,wt=10): 26129 hBOOL(hAPP(c_Message_Oparts(c_Set_Oinsert(c_Message_Omsg_OMPair(A,B),C,D)),B)). [resolve(26124,a,1279,b)].
% 130.96/17.96
% 130.96/17.96 % given #7500 (F,wt=28): 19769 c_Lattices_Oupper__semilattice__class_Osup(c_Message_Oparts(c_Set_Oinsert(A,c_Set_Oinsert(B,c_Message_Oanalz(c_Set_Oinsert(C,c_Lattices_Oupper__semilattice__class_Osup(D,c_Message_Osynth(E),tc_fun(tc_Message_Omsg,tc_bool)),tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg)),F,tc_fun(tc_Message_Omsg,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool)). [para(152(a,1),19624(a,1,1,1,2,2,1))].
% 130.96/17.96
% 130.96/17.96 % SZS status Unsatisfiable for theBenchmark
% 130.96/17.96
% 130.96/17.96 % Proof 1 at 13.73 (+ 3.73) seconds.
% 130.96/17.96 % Length of proof is 27.
% 130.96/17.96 % Level of proof is 7.
% 130.96/17.96 % Maximum clause weight is 15.000.
% 130.96/17.96 % Given clauses 7573.
% 130.96/17.96
% 130.96/17.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------