%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV790-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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 : Fri Sep 25 03:14:03 PM UTC 2026
% Result : Unsatisfiable 10.66s 1.91s
% Output : Proof 10.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 68
% Syntax : Number of formulae : 281 ( 257 unt; 0 def)
% Number of atoms : 309 ( 201 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 322 ( 294 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 49 ( 49 usr; 17 con; 0-5 aty)
% Number of variables : 716 ( 306 sgn 358 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f520,negated_conjecture,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f520_nnf,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
~ c_in(v_B,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
cnf(t10,plain,
c_in(v_B,c_Event_Obad,tc_Message_Oagent) = false,
inference(equality_encoding,[status(esa)],[c520]) ).
cnf(f436,axiom,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Spy__in__bad_0) ).
fof(f436_nnf,plain,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f436]) ).
cnf(c436,plain,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f436_nnf]) ).
cnf(t8,plain,
c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent) = true,
inference(equality_encoding,[status(esa)],[c436]) ).
cnf(f524,negated_conjecture,
v_B = c_Message_Oagent_OSpy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f524_nnf,plain,
v_B = c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f524]) ).
cnf(c524,plain,
v_B = c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f524_nnf]) ).
cnf(t0,plain,
v_B = c_Message_Oagent_OSpy,
inference(equality_encoding,[status(esa)],[c524]) ).
cnf(t256,plain,
c_Message_Oagent_OSpy = v_B,
inference(orient,[status(thm)],[t0]) ).
cnf(t269,plain,
c_in(v_B,c_Event_Obad,tc_Message_Oagent) = true,
inference(step,[status(thm)],[t8,t256]) ).
cnf(t264,plain,
c_in(v_B,c_Event_Obad,tc_Message_Oagent) = true,
inference(orient,[status(thm)],[t269]) ).
cnf(t271,plain,
true = false,
inference(step,[status(thm)],[t10,t264]) ).
cnf(t266,plain,
false = true,
inference(orient,[status(thm)],[t271]) ).
cnf(f7,axiom,
c_Public_OshrK(V_A) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_priK__neq__shrK_0) ).
fof(f7_nnf,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
c_Public_OshrK(X0) != c_Message_OinvKey(c_Public_OpublicKey(X1,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f11,axiom,
c_Message_Omsg_OAgent(V_A) != c_Message_OHPair(V_X,V_Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Agent__neq__HPair_0) ).
fof(f11_nnf,plain,
! [V_A,V_X,V_Y] : c_Message_Omsg_OAgent(V_A) != c_Message_OHPair(V_X,V_Y),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_A,V_X,V_Y] : c_Message_Omsg_OAgent(V_A) != c_Message_OHPair(V_X,V_Y),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
c_Message_Omsg_OAgent(X0) != c_Message_OHPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f24,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OGets(V_agent,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I9_J_0) ).
fof(f24_nnf,plain,
! [V_agent_H,V_msg_H,V_agent,V_msg] : c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OGets(V_agent,V_msg),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [V_agent_H,V_msg_H,V_agent,V_msg] : c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OGets(V_agent,V_msg),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OGets(X2,X3),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(f25,axiom,
c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pubK__neq__shrK_0) ).
fof(f25_nnf,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
c_Public_OshrK(X0) != c_Public_OpublicKey(X1,X2),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(f31,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f31_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f43,axiom,
c_Event_Oevent_OGets(V_agent,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I8_J_0) ).
fof(f43_nnf,plain,
! [V_agent,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OGets(V_agent,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [V_agent,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OGets(V_agent,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_ONotes(X2,X3),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(f52,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f52_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(f53,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I17_J_0) ).
fof(f53_nnf,plain,
! [V_msg1_H,V_msg2_H,V_agent] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OAgent(V_agent),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [V_msg1_H,V_msg2_H,V_agent] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OAgent(X2),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(f54,axiom,
c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_shrK__neq__pubK_0) ).
fof(f54_nnf,plain,
! [V_b,V_C,V_A] : c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [V_b,V_C,V_A] : c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
c_Public_OpublicKey(X0,X1) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(f60,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I16_J_0) ).
fof(f60_nnf,plain,
! [V_agent,V_msg1_H,V_msg2_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
! [V_agent,V_msg1_H,V_msg2_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c60,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
cnf(f65,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f65_nnf,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(f78,axiom,
c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)) != c_Public_OpublicKey(V_c,V_A_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_privateKey__neq__publicKey_0) ).
fof(f78_nnf,plain,
! [V_b,V_A,V_c,V_A_H] : c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)) != c_Public_OpublicKey(V_c,V_A_H),
inference(nnf_transformation,[status(thm)],[f78]) ).
fof(f78_sk,plain,
! [V_b,V_A,V_c,V_A_H] : c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)) != c_Public_OpublicKey(V_c,V_A_H),
inference(skolemisation,[status(esa)],[f78_nnf]) ).
cnf(c78,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OpublicKey(X2,X3),
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(f122,axiom,
c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)) != c_Public_OshrK(V_A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_shrK__neq__priK_0) ).
fof(f122_nnf,plain,
! [V_b,V_C,V_A] : c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)) != c_Public_OshrK(V_A),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [V_b,V_C,V_A] : c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)) != c_Public_OshrK(V_A),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f125,axiom,
c_Public_OpublicKey(V_c,V_A_H) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_publicKey__neq__privateKey_0) ).
fof(f125_nnf,plain,
! [V_c,V_A_H,V_b,V_A] : c_Public_OpublicKey(V_c,V_A_H) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [V_c,V_A_H,V_b,V_A] : c_Public_OpublicKey(V_c,V_A_H) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
c_Public_OpublicKey(X0,X1) != c_Message_OinvKey(c_Public_OpublicKey(X2,X3)),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(f159,axiom,
~ c_in(V_X,c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_parts__emptyE_0) ).
fof(f159_nnf,plain,
! [V_X] : ~ c_in(V_X,c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f159]) ).
fof(f159_sk,plain,
! [V_X] : ~ c_in(V_X,c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f159_nnf]) ).
cnf(c159,plain,
~ c_in(X0,c_Message_Oparts(c_Orderings_Obot__class_Obot(tc_fun(tc_Message_Omsg,tc_bool))),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f159_sk]) ).
cnf(f212,axiom,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Server__not__bad_0) ).
fof(f212_nnf,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f212]) ).
fof(f212_sk,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(skolemisation,[status(esa)],[f212_nnf]) ).
cnf(c212,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
cnf(f218,axiom,
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_distinct_Osimps_I2_J_0) ).
fof(f218_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c218,plain,
( ~ c_List_Odistinct(c_List_Olist_OCons(X0,X1,X2),X2)
| ~ c_in(X0,c_List_Oset(X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
cnf(f222,axiom,
~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f222_nnf,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c222,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f224,axiom,
~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f224_nnf,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f224]) ).
fof(f224_sk,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f224_nnf]) ).
cnf(c224,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(f225,axiom,
~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f225_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f225]) ).
fof(f225_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f225_nnf]) ).
cnf(c225,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f225_sk]) ).
cnf(f230,axiom,
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f230_nnf,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c230,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f242,axiom,
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f242_nnf,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(nnf_transformation,[status(thm)],[f242]) ).
fof(f242_sk,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(skolemisation,[status(esa)],[f242_nnf]) ).
cnf(c242,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(f272,axiom,
c_Message_Omsg_OCrypt(V_K,V_X_H) != c_Message_OHPair(V_X,V_Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__neq__HPair_0) ).
fof(f272_nnf,plain,
! [V_K,V_X_H,V_X,V_Y] : c_Message_Omsg_OCrypt(V_K,V_X_H) != c_Message_OHPair(V_X,V_Y),
inference(nnf_transformation,[status(thm)],[f272]) ).
fof(f272_sk,plain,
! [V_K,V_X_H,V_X,V_Y] : c_Message_Omsg_OCrypt(V_K,V_X_H) != c_Message_OHPair(V_X,V_Y),
inference(skolemisation,[status(esa)],[f272_nnf]) ).
cnf(c272,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_OHPair(X2,X3),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
cnf(f273,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I18_J_0) ).
fof(f273_nnf,plain,
! [V_agent,V_nat_H,V_msg_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [V_agent,V_nat_H,V_msg_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f274,axiom,
c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I48_J_0) ).
fof(f274_nnf,plain,
! [V_msg1,V_msg2,V_nat_H,V_msg_H] : c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [V_msg1,V_msg2,V_nat_H,V_msg_H] : c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c274,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OCrypt(X2,X3),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f275,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I19_J_0) ).
fof(f275_nnf,plain,
! [V_nat_H,V_msg_H,V_agent] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OAgent(V_agent),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [V_nat_H,V_msg_H,V_agent] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c275,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OAgent(X2),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
cnf(f276,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OMPair(V_msg1,V_msg2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I49_J_0) ).
fof(f276_nnf,plain,
! [V_nat_H,V_msg_H,V_msg1,V_msg2] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OMPair(V_msg1,V_msg2),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [V_nat_H,V_msg_H,V_msg1,V_msg2] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OMPair(V_msg1,V_msg2),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c276,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OMPair(X2,X3),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(f278,axiom,
c_Message_Omsg_OAgent(V_agent) != hAPP(c_Message_Omsg_OKey,V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I12_J_0) ).
fof(f278_nnf,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != hAPP(c_Message_Omsg_OKey,V_nat_H),
inference(nnf_transformation,[status(thm)],[f278]) ).
fof(f278_sk,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != hAPP(c_Message_Omsg_OKey,V_nat_H),
inference(skolemisation,[status(esa)],[f278_nnf]) ).
cnf(c278,plain,
c_Message_Omsg_OAgent(X0) != hAPP(c_Message_Omsg_OKey,X1),
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
cnf(f279,axiom,
hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I13_J_0) ).
fof(f279_nnf,plain,
! [V_nat_H,V_agent] : hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(nnf_transformation,[status(thm)],[f279]) ).
fof(f279_sk,plain,
! [V_nat_H,V_agent] : hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f279_nnf]) ).
cnf(c279,plain,
hAPP(c_Message_Omsg_OKey,X0) != c_Message_Omsg_OAgent(X1),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
cnf(f280,axiom,
hAPP(c_Message_Omsg_OKey,V_K) != c_Message_OHPair(V_X,V_Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Key__neq__HPair_0) ).
fof(f280_nnf,plain,
! [V_K,V_X,V_Y] : hAPP(c_Message_Omsg_OKey,V_K) != c_Message_OHPair(V_X,V_Y),
inference(nnf_transformation,[status(thm)],[f280]) ).
fof(f280_sk,plain,
! [V_K,V_X,V_Y] : hAPP(c_Message_Omsg_OKey,V_K) != c_Message_OHPair(V_X,V_Y),
inference(skolemisation,[status(esa)],[f280_nnf]) ).
cnf(c280,plain,
hAPP(c_Message_Omsg_OKey,X0) != c_Message_OHPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f280_sk]) ).
cnf(f281,axiom,
hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I40_J_0) ).
fof(f281_nnf,plain,
! [V_nat,V_msg1_H,V_msg2_H] : hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(nnf_transformation,[status(thm)],[f281]) ).
fof(f281_sk,plain,
! [V_nat,V_msg1_H,V_msg2_H] : hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(skolemisation,[status(esa)],[f281_nnf]) ).
cnf(c281,plain,
hAPP(c_Message_Omsg_OKey,X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f281_sk]) ).
cnf(f282,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != hAPP(c_Message_Omsg_OKey,V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I41_J_0) ).
fof(f282_nnf,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != hAPP(c_Message_Omsg_OKey,V_nat),
inference(nnf_transformation,[status(thm)],[f282]) ).
fof(f282_sk,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != hAPP(c_Message_Omsg_OKey,V_nat),
inference(skolemisation,[status(esa)],[f282_nnf]) ).
cnf(c282,plain,
c_Message_Omsg_OMPair(X0,X1) != hAPP(c_Message_Omsg_OKey,X2),
inference(cnf_transformation,[status(esa)],[f282_sk]) ).
cnf(f293,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I4_J_0) ).
fof(f293_nnf,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f293_nnf]) ).
cnf(c293,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f294,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f294_nnf,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f294]) ).
fof(f294_sk,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f294_nnf]) ).
cnf(c294,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f294_sk]) ).
cnf(f295,axiom,
c_Message_Omsg_ONonce(V_N) != c_Message_OHPair(V_X,V_Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nonce__neq__HPair_0) ).
fof(f295_nnf,plain,
! [V_N,V_X,V_Y] : c_Message_Omsg_ONonce(V_N) != c_Message_OHPair(V_X,V_Y),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
! [V_N,V_X,V_Y] : c_Message_Omsg_ONonce(V_N) != c_Message_OHPair(V_X,V_Y),
inference(skolemisation,[status(esa)],[f295_nnf]) ).
cnf(c295,plain,
c_Message_Omsg_ONonce(X0) != c_Message_OHPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
cnf(f296,axiom,
c_Message_Omsg_ONonce(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I11_J_0) ).
fof(f296_nnf,plain,
! [V_nat_H,V_agent] : c_Message_Omsg_ONonce(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
! [V_nat_H,V_agent] : c_Message_Omsg_ONonce(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c296,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OAgent(X1),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
cnf(f297,axiom,
c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I34_J_0) ).
fof(f297_nnf,plain,
! [V_nat,V_msg1_H,V_msg2_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(nnf_transformation,[status(thm)],[f297]) ).
fof(f297_sk,plain,
! [V_nat,V_msg1_H,V_msg2_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(skolemisation,[status(esa)],[f297_nnf]) ).
cnf(c297,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f297_sk]) ).
cnf(f298,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I10_J_0) ).
fof(f298_nnf,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c298,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_ONonce(X1),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f299,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I35_J_0) ).
fof(f299_nnf,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_ONonce(V_nat),
inference(nnf_transformation,[status(thm)],[f299]) ).
fof(f299_sk,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_ONonce(V_nat),
inference(skolemisation,[status(esa)],[f299_nnf]) ).
cnf(c299,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_ONonce(X2),
inference(cnf_transformation,[status(esa)],[f299_sk]) ).
cnf(f300,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I4_J_0) ).
fof(f300_nnf,plain,
! [V_agent1,V_agent2,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f300]) ).
fof(f300_sk,plain,
! [V_agent1,V_agent2,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
inference(skolemisation,[status(esa)],[f300_nnf]) ).
cnf(c300,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f300_sk]) ).
cnf(f301,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I6_J_0) ).
fof(f301_nnf,plain,
! [V_agent1,V_agent2,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f301]) ).
fof(f301_sk,plain,
! [V_agent1,V_agent2,V_msg,V_agent_H,V_msg_H] : c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
inference(skolemisation,[status(esa)],[f301_nnf]) ).
cnf(c301,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_ONotes(X3,X4),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
cnf(f302,axiom,
c_Event_Oevent_OGets(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I5_J_0) ).
fof(f302_nnf,plain,
! [V_agent_H,V_msg_H,V_agent1,V_agent2,V_msg] : c_Event_Oevent_OGets(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
inference(nnf_transformation,[status(thm)],[f302]) ).
fof(f302_sk,plain,
! [V_agent_H,V_msg_H,V_agent1,V_agent2,V_msg] : c_Event_Oevent_OGets(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
inference(skolemisation,[status(esa)],[f302_nnf]) ).
cnf(c302,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
cnf(f303,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I7_J_0) ).
fof(f303_nnf,plain,
! [V_agent_H,V_msg_H,V_agent1,V_agent2,V_msg] : c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
! [V_agent_H,V_msg_H,V_agent1,V_agent2,V_msg] : c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
inference(skolemisation,[status(esa)],[f303_nnf]) ).
cnf(c303,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
cnf(f321,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_filter__empty__conv_0) ).
fof(f321_nnf,plain,
! [V_P,V_xs,T_a,V_x] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [V_P,V_xs,T_a,V_x] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c321,plain,
( ~ c_in(X3,c_List_Oset(X1,X2),X2)
| ~ hBOOL(hAPP(X0,X3))
| c_List_Ofilter(X0,X1,X2) != c_List_Olist_ONil(X2) ),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
cnf(f335,axiom,
~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__notin__initState_0) ).
fof(f335_nnf,plain,
! [V_K,V_X,V_B] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f335]) ).
fof(f335_sk,plain,
! [V_K,V_X,V_B] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f335_nnf]) ).
cnf(c335,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(c_Event_OinitState(X2)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f335_sk]) ).
cnf(f337,axiom,
~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__notin__image__Key_0) ).
fof(f337_nnf,plain,
! [V_K,V_X,V_A] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [V_K,V_X,V_A] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Set_Oimage(c_Message_Omsg_OKey,X2,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f341,axiom,
~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nonce__notin__initState_0) ).
fof(f341_nnf,plain,
! [V_N,V_B] : ~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f341]) ).
fof(f341_sk,plain,
! [V_N,V_B] : ~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f341_nnf]) ).
cnf(c341,plain,
~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_OinitState(X1)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f341_sk]) ).
cnf(f348,axiom,
~ c_in(c_Message_Omsg_ONonce(V_x),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nonce__Key__image__eq_0) ).
fof(f348_nnf,plain,
! [V_x,V_A] : ~ c_in(c_Message_Omsg_ONonce(V_x),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f348]) ).
fof(f348_sk,plain,
! [V_x,V_A] : ~ c_in(c_Message_Omsg_ONonce(V_x),c_Set_Oimage(c_Message_Omsg_OKey,V_A,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f348_nnf]) ).
cnf(c348,plain,
~ c_in(c_Message_Omsg_ONonce(X0),c_Set_Oimage(c_Message_Omsg_OKey,X1,tc_nat,tc_Message_Omsg),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
cnf(f355,axiom,
~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Crypt__notin__used__empty_0) ).
fof(f355_nnf,plain,
! [V_K,V_X] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f355]) ).
fof(f355_sk,plain,
! [V_K,V_X] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f355_nnf]) ).
cnf(c355,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f355_sk]) ).
cnf(f356,axiom,
~ c_in(c_Message_Omsg_ONonce(V_N),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nonce__notin__used__empty_0) ).
fof(f356_nnf,plain,
! [V_N] : ~ c_in(c_Message_Omsg_ONonce(V_N),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f356]) ).
fof(f356_sk,plain,
! [V_N] : ~ c_in(c_Message_Omsg_ONonce(V_N),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f356_nnf]) ).
cnf(c356,plain,
~ c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f356_sk]) ).
cnf(f391,axiom,
( ~ c_NS__Shared__Mirabelle_OIssues(V_A,V_B,V_X,V_evs)
| ~ c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(V_A,V_B,v_sko__NS__Shared__Mirabelle__XIssues__def__1(V_A,V_B,V_X,V_evs)),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(V_evs,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Issues__def_2) ).
fof(f391_nnf,plain,
! [V_X,V_A,V_B,V_evs] :
( ~ c_NS__Shared__Mirabelle_OIssues(V_A,V_B,V_X,V_evs)
| ~ c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(V_A,V_B,v_sko__NS__Shared__Mirabelle__XIssues__def__1(V_A,V_B,V_X,V_evs)),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(V_evs,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f391]) ).
fof(f391_sk,plain,
! [V_X,V_A,V_B,V_evs] :
( ~ c_NS__Shared__Mirabelle_OIssues(V_A,V_B,V_X,V_evs)
| ~ c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(V_A,V_B,v_sko__NS__Shared__Mirabelle__XIssues__def__1(V_A,V_B,V_X,V_evs)),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(V_evs,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f391_nnf]) ).
cnf(c391,plain,
( ~ c_NS__Shared__Mirabelle_OIssues(X1,X2,X0,X3)
| ~ c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(X1,X2,v_sko__NS__Shared__Mirabelle__XIssues__def__1(X1,X2,X0,X3)),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(X3,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f391_sk]) ).
cnf(f419,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I37_J_0) ).
fof(f419_nnf,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_ONonce(V_nat),
inference(nnf_transformation,[status(thm)],[f419]) ).
fof(f419_sk,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_ONonce(V_nat),
inference(skolemisation,[status(esa)],[f419_nnf]) ).
cnf(c419,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_ONonce(X2),
inference(cnf_transformation,[status(esa)],[f419_sk]) ).
cnf(f420,axiom,
hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I31_J_0) ).
fof(f420_nnf,plain,
! [V_nat_H,V_nat] : hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_ONonce(V_nat),
inference(nnf_transformation,[status(thm)],[f420]) ).
fof(f420_sk,plain,
! [V_nat_H,V_nat] : hAPP(c_Message_Omsg_OKey,V_nat_H) != c_Message_Omsg_ONonce(V_nat),
inference(skolemisation,[status(esa)],[f420_nnf]) ).
cnf(c420,plain,
hAPP(c_Message_Omsg_OKey,X0) != c_Message_Omsg_ONonce(X1),
inference(cnf_transformation,[status(esa)],[f420_sk]) ).
cnf(f438,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f438_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f438]) ).
fof(f438_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f438_nnf]) ).
cnf(c438,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f438_sk]) ).
cnf(f439,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != hAPP(c_Message_Omsg_OKey,V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I43_J_0) ).
fof(f439_nnf,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != hAPP(c_Message_Omsg_OKey,V_nat),
inference(nnf_transformation,[status(thm)],[f439]) ).
fof(f439_sk,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != hAPP(c_Message_Omsg_OKey,V_nat),
inference(skolemisation,[status(esa)],[f439_nnf]) ).
cnf(c439,plain,
c_Message_Omsg_OCrypt(X0,X1) != hAPP(c_Message_Omsg_OKey,X2),
inference(cnf_transformation,[status(esa)],[f439_sk]) ).
cnf(f442,axiom,
c_Message_Omsg_ONonce(V_nat) != hAPP(c_Message_Omsg_OKey,V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I30_J_0) ).
fof(f442_nnf,plain,
! [V_nat,V_nat_H] : c_Message_Omsg_ONonce(V_nat) != hAPP(c_Message_Omsg_OKey,V_nat_H),
inference(nnf_transformation,[status(thm)],[f442]) ).
fof(f442_sk,plain,
! [V_nat,V_nat_H] : c_Message_Omsg_ONonce(V_nat) != hAPP(c_Message_Omsg_OKey,V_nat_H),
inference(skolemisation,[status(esa)],[f442_nnf]) ).
cnf(c442,plain,
c_Message_Omsg_ONonce(X0) != hAPP(c_Message_Omsg_OKey,X1),
inference(cnf_transformation,[status(esa)],[f442_sk]) ).
cnf(f478,axiom,
c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I36_J_0) ).
fof(f478_nnf,plain,
! [V_nat,V_nat_H,V_msg_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f478]) ).
fof(f478_sk,plain,
! [V_nat,V_nat_H,V_msg_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c478,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
cnf(f490,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f490_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f490]) ).
fof(f490_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f490_nnf]) ).
cnf(c490,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f490_sk]) ).
cnf(f491,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f491_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f491]) ).
fof(f491_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f491_nnf]) ).
cnf(c491,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f491_sk]) ).
cnf(f501,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f501_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f501]) ).
fof(f501_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f501_nnf]) ).
cnf(c501,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f501_sk]) ).
cnf(f502,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f502_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f502]) ).
fof(f502_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f502_nnf]) ).
cnf(c502,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f502_sk]) ).
cnf(f512,axiom,
hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_msg_Osimps_I42_J_0) ).
fof(f512_nnf,plain,
! [V_nat,V_nat_H,V_msg_H] : hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f512]) ).
fof(f512_sk,plain,
! [V_nat,V_nat_H,V_msg_H] : hAPP(c_Message_Omsg_OKey,V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(skolemisation,[status(esa)],[f512_nnf]) ).
cnf(c512,plain,
hAPP(c_Message_Omsg_OKey,X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
cnf(f519,negated_conjecture,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f519_nnf,plain,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f519]) ).
fof(f519_sk,plain,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(skolemisation,[status(esa)],[f519_nnf]) ).
cnf(c519,plain,
~ c_in(v_A,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f519_sk]) ).
cnf(f523,negated_conjecture,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f523_nnf,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f523]) ).
fof(f523_sk,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f523_nnf]) ).
cnf(c523,plain,
~ c_in(hAPP(c_Message_Omsg_OKey,v_K),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evsf)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f523_sk]) ).
cnf(f528,negated_conjecture,
( ~ c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(v_evsf,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_9) ).
fof(f528_nnf,plain,
( ~ c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(v_evsf,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f528]) ).
fof(f528_sk,plain,
( ~ c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(v_evsf,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f528_nnf]) ).
cnf(c528,plain,
( ~ c_in(c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),c_List_Oset(v_evsf,tc_Event_Oevent),tc_Event_Oevent)
| ~ c_in(c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(c_COMBB(c_Not,c_COMBC(c_fequal(tc_Event_Oevent),c_Event_Oevent_OSays(v_B,v_A,c_Message_Omsg_OCrypt(v_K,c_Message_Omsg_ONonce(v_Nb))),tc_Event_Oevent,tc_Event_Oevent,tc_bool),tc_bool,tc_bool,tc_Event_Oevent),c_List_Orev(v_evsf,tc_Event_Oevent),tc_Event_Oevent))),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f528_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7,c11,c24,c25,c31,c43,c52,c53,c54,c60,c65,c78,c122,c125,c159,c212,c218,c222,c224,c225,c230,c242,c272,c273,c274,c275,c276,c278,c279,c280,c281,c282,c293,c294,c295,c296,c297,c298,c299,c300,c301,c302,c303,c321,c335,c337,c341,c348,c355,c356,c391,c419,c420,c438,c439,c442,c478,c490,c491,c501,c502,c512,c519,c520,c523,c528]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t266]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV790-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.53 % Computer : n020.cluster.edu
% 0.08/0.53 % Model : x86_64 x86_64
% 0.08/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.53 % Memory : 8046.5625MB
% 0.08/0.53 % OS : Linux 6.8.0-71-generic
% 0.08/0.53 % CPULimit : 300
% 0.08/0.53 % WCLimit : 300
% 0.08/0.53 % DateTime : Thu Sep 24 21:06:04 UTC 2026
% 0.08/0.53 % CPUTime :
% 0.08/0.53 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 10.66/1.91 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.66/1.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------