%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV722-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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:13:57 PM UTC 2026
% Result : Unsatisfiable 58.08s 7.83s
% Output : Proof 58.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 65
% Syntax : Number of formulae : 288 ( 224 unt; 0 def)
% Number of atoms : 400 ( 184 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 462 ( 350 ~; 112 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 47 ( 47 usr; 15 con; 0-4 aty)
% Number of variables : 800 ( 272 sgn 384 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f472,axiom,
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_parts_OFst_0) ).
fof(f472_nnf,plain,
! [V_X,V_H,V_Y] :
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f472]) ).
fof(f472_sk,plain,
! [V_X,V_H,V_Y] :
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f472_nnf]) ).
cnf(c472,plain,
( ~ c_in(c_Message_Omsg_OMPair(X0,X2),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
cnf(t131,plain,
ifeq(c_in(c_Message_Omsg_OMPair(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X1,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(equality_encoding,[status(esa)],[c472]) ).
cnf(t406,plain,
ifeq(c_in(c_Message_Omsg_OMPair(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X1,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(orient,[status(thm)],[t131]) ).
cnf(f471,axiom,
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_parts_OSnd_0) ).
fof(f471_nnf,plain,
! [V_Y,V_H,V_X] :
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f471]) ).
fof(f471_sk,plain,
! [V_Y,V_H,V_X] :
( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_Y,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f471_nnf]) ).
cnf(c471,plain,
( ~ c_in(c_Message_Omsg_OMPair(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f471_sk]) ).
cnf(t132,plain,
ifeq(c_in(c_Message_Omsg_OMPair(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X2,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(equality_encoding,[status(esa)],[c471]) ).
cnf(t405,plain,
ifeq(c_in(c_Message_Omsg_OMPair(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X2,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(orient,[status(thm)],[t132]) ).
cnf(f481,axiom,
( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_parts_OBody_0) ).
fof(f481_nnf,plain,
! [V_X,V_H,V_K] :
( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f481]) ).
fof(f481_sk,plain,
! [V_X,V_H,V_K] :
( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(V_H),tc_Message_Omsg)
| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f481_nnf]) ).
cnf(c481,plain,
( ~ c_in(c_Message_Omsg_OCrypt(X2,X0),c_Message_Oparts(X1),tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f481_sk]) ).
cnf(t128,plain,
ifeq(c_in(c_Message_Omsg_OCrypt(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X2,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(equality_encoding,[status(esa)],[c481]) ).
cnf(t376,plain,
ifeq(c_in(c_Message_Omsg_OCrypt(X1,X2),c_Message_Oparts(X3),tc_Message_Omsg),true,c_in(X2,c_Message_Oparts(X3),tc_Message_Omsg),true) = true,
inference(orient,[status(thm)],[t128]) ).
cnf(f477,axiom,
( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Says__imp__parts__knows__Spy_0) ).
fof(f477_nnf,plain,
! [V_X,V_evs,V_A,V_B] :
( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ),
inference(nnf_transformation,[status(thm)],[f477]) ).
fof(f477_sk,plain,
! [V_X,V_evs,V_A,V_B] :
( ~ c_in(c_Event_Oevent_OSays(V_A,V_B,V_X),c_List_Oset(V_evs,tc_Event_Oevent),tc_Event_Oevent)
| c_in(V_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,V_evs)),tc_Message_Omsg) ),
inference(skolemisation,[status(esa)],[f477_nnf]) ).
cnf(c477,plain,
( ~ c_in(c_Event_Oevent_OSays(X2,X3,X0),c_List_Oset(X1,tc_Event_Oevent),tc_Event_Oevent)
| c_in(X0,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X1)),tc_Message_Omsg) ),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
cnf(t180,plain,
ifeq(c_in(c_Event_Oevent_OSays(X1,X2,X3),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent),true,c_in(X3,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg),true) = true,
inference(equality_encoding,[status(esa)],[c477]) ).
cnf(t415,plain,
ifeq(c_in(c_Event_Oevent_OSays(X1,X2,X3),c_List_Oset(X4,tc_Event_Oevent),tc_Event_Oevent),true,c_in(X3,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,X4)),tc_Message_Omsg),true) = true,
inference(orient,[status(thm)],[t180]) ).
cnf(f494,negated_conjecture,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f494_nnf,plain,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent),
inference(nnf_transformation,[status(thm)],[f494]) ).
cnf(c494,plain,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent),
inference(cnf_transformation,[status(esa)],[f494_nnf]) ).
cnf(t153,plain,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent) = true,
inference(equality_encoding,[status(esa)],[c494]) ).
cnf(t279,plain,
c_in(c_Event_Oevent_OSays(c_Message_Oagent_OServer,v_A,c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))))),c_List_Oset(v_evs,tc_Event_Oevent),tc_Event_Oevent) = true,
inference(orient,[status(thm)],[t153]) ).
cnf(t416,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t415,t279]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t247,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t40306,plain,
true = c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t416,t247]) ).
cnf(t37987,plain,
c_in(c_Message_Omsg_OCrypt(c_Public_OshrK(v_A),c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t40306]) ).
cnf(t37991,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t376,t37987]) ).
cnf(t40307,plain,
true = c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t37991,t247]) ).
cnf(t38012,plain,
c_in(c_Message_Omsg_OMPair(v_NA,c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X))),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t40307]) ).
cnf(t38017,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t405,t38012]) ).
cnf(t40318,plain,
true = c_in(c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t38017,t247]) ).
cnf(t38929,plain,
c_in(c_Message_Omsg_OMPair(v_B,c_Message_Omsg_OMPair(v_K,v_X)),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t40318]) ).
cnf(t38934,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OMPair(v_K,v_X),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t405,t38929]) ).
cnf(t40324,plain,
true = c_in(c_Message_Omsg_OMPair(v_K,v_X),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t38934,t247]) ).
cnf(t39325,plain,
c_in(c_Message_Omsg_OMPair(v_K,v_X),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = true,
inference(orient,[status(thm)],[t40324]) ).
cnf(t39329,plain,
true = ifeq(true,true,c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t406,t39325]) ).
cnf(t40325,plain,
true = c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t39329,t247]) ).
cnf(f495,negated_conjecture,
~ c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f495_nnf,plain,
~ c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f495]) ).
fof(f495_sk,plain,
~ c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f495_nnf]) ).
cnf(c495,plain,
~ c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f495_sk]) ).
cnf(t34,plain,
c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = false,
inference(equality_encoding,[status(esa)],[c495]) ).
cnf(t1218,plain,
c_in(v_K,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = false,
inference(orient,[status(thm)],[t34]) ).
cnf(t40326,plain,
true = false,
inference(step,[status(thm)],[t40325,t1218]) ).
cnf(t39348,plain,
false = true,
inference(orient,[status(thm)],[t40326]) ).
cnf(f1,axiom,
~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nonce__notin__initState_0) ).
fof(f1_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)],[f1]) ).
fof(f1_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)],[f1_nnf]) ).
cnf(c1,plain,
~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_OinitState(X1)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f2,axiom,
c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I36_J_0) ).
fof(f2_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)],[f2]) ).
fof(f2_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)],[f2_nnf]) ).
cnf(c2,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f3,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I19_J_0) ).
fof(f3_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)],[f3]) ).
fof(f3_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)],[f3_nnf]) ).
cnf(c3,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OAgent(X2),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(f4,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I18_J_0) ).
fof(f4_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)],[f4]) ).
fof(f4_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)],[f4_nnf]) ).
cnf(c4,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f5,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I37_J_0) ).
fof(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c5,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_ONonce(X2),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f6,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I35_J_0) ).
fof(f6_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)],[f6]) ).
fof(f6_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)],[f6_nnf]) ).
cnf(c6,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_ONonce(X2),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f7,axiom,
c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I34_J_0) ).
fof(f7_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)],[f7]) ).
fof(f7_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)],[f7_nnf]) ).
cnf(c7,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f8,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I16_J_0) ).
fof(f8_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)],[f8]) ).
fof(f8_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)],[f8_nnf]) ).
cnf(c8,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f9,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I17_J_0) ).
fof(f9_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)],[f9]) ).
fof(f9_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)],[f9_nnf]) ).
cnf(c9,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OAgent(X2),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f10,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I10_J_0) ).
fof(f10_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)],[f10]) ).
fof(f10_sk,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_ONonce(V_nat_H),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_ONonce(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f12,axiom,
c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I13_J_0) ).
fof(f12_nnf,plain,
! [V_nat_H,V_agent] : c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [V_nat_H,V_agent] : c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_OAgent(X1),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f13,axiom,
c_Message_Omsg_ONonce(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I11_J_0) ).
fof(f13_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)],[f13]) ).
fof(f13_sk,plain,
! [V_nat_H,V_agent] : c_Message_Omsg_ONonce(V_nat_H) != c_Message_Omsg_OAgent(V_agent),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OAgent(X1),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(f14,axiom,
c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OKey(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I30_J_0) ).
fof(f14_nnf,plain,
! [V_nat,V_nat_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OKey(V_nat_H),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V_nat,V_nat_H] : c_Message_Omsg_ONonce(V_nat) != c_Message_Omsg_OKey(V_nat_H),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
c_Message_Omsg_ONonce(X0) != c_Message_Omsg_OKey(X1),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,axiom,
c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_ONonce(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I31_J_0) ).
fof(f15_nnf,plain,
! [V_nat_H,V_nat] : c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_ONonce(V_nat),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [V_nat_H,V_nat] : c_Message_Omsg_OKey(V_nat_H) != c_Message_Omsg_ONonce(V_nat),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_ONonce(X1),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f16,axiom,
c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OKey(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I12_J_0) ).
fof(f16_nnf,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OKey(V_nat_H),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [V_agent,V_nat_H] : c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OKey(V_nat_H),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
c_Message_Omsg_OAgent(X0) != c_Message_Omsg_OKey(X1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f47,axiom,
c_Public_OpublicKey(V_c,V_A_H) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_publicKey__neq__privateKey_0) ).
fof(f47_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)],[f47]) ).
fof(f47_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)],[f47_nnf]) ).
cnf(c47,plain,
c_Public_OpublicKey(X0,X1) != c_Message_OinvKey(c_Public_OpublicKey(X2,X3)),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(f48,axiom,
c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)) != c_Public_OshrK(V_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_shrK__neq__priK_0) ).
fof(f48_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)],[f48]) ).
fof(f48_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)],[f48_nnf]) ).
cnf(c48,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(f52,axiom,
c_Public_OshrK(V_A) != c_Message_OinvKey(c_Public_OpublicKey(V_b,V_C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_priK__neq__shrK_0) ).
fof(f52_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)],[f52]) ).
fof(f52_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)],[f52_nnf]) ).
cnf(c52,plain,
c_Public_OshrK(X0) != c_Message_OinvKey(c_Public_OpublicKey(X1,X2)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(f62,axiom,
c_Message_OinvKey(c_Public_OpublicKey(V_b,V_A)) != c_Public_OpublicKey(V_c,V_A_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_privateKey__neq__publicKey_0) ).
fof(f62_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)],[f62]) ).
fof(f62_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)],[f62_nnf]) ).
cnf(c62,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OpublicKey(X2,X3),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(f75,axiom,
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f75_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f83,axiom,
c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pubK__neq__shrK_0) ).
fof(f83_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)],[f83]) ).
fof(f83_sk,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
c_Public_OshrK(X0) != c_Public_OpublicKey(X1,X2),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(f84,axiom,
c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_shrK__neq__pubK_0) ).
fof(f84_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)],[f84]) ).
fof(f84_sk,plain,
! [V_b,V_C,V_A] : c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
c_Public_OpublicKey(X0,X1) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f172,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f172_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)],[f172]) ).
fof(f172_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)],[f172_nnf]) ).
cnf(c172,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(f221,axiom,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Server__not__bad_0) ).
fof(f221_nnf,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c221,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f222,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f222_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)],[f222]) ).
fof(f222_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c222,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f223,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f223_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)],[f223]) ).
fof(f223_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f239,axiom,
~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f239_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)],[f239]) ).
fof(f239_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)],[f239_nnf]) ).
cnf(c239,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f241,axiom,
~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f241_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)],[f241]) ).
fof(f241_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)],[f241_nnf]) ).
cnf(c241,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f242,axiom,
~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f242_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)],[f242]) ).
fof(f242_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)],[f242_nnf]) ).
cnf(c242,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(f248,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/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f248_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)],[f248]) ).
fof(f248_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)],[f248_nnf]) ).
cnf(c248,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(f260,axiom,
c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I40_J_0) ).
fof(f260_nnf,plain,
! [V_nat,V_msg1_H,V_msg2_H] : c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
! [V_nat,V_msg1_H,V_msg2_H] : c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H),
inference(skolemisation,[status(esa)],[f260_nnf]) ).
cnf(c260,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
cnf(f261,axiom,
c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OKey(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I41_J_0) ).
fof(f261_nnf,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OKey(V_nat),
inference(nnf_transformation,[status(thm)],[f261]) ).
fof(f261_sk,plain,
! [V_msg1_H,V_msg2_H,V_nat] : c_Message_Omsg_OMPair(V_msg1_H,V_msg2_H) != c_Message_Omsg_OKey(V_nat),
inference(skolemisation,[status(esa)],[f261_nnf]) ).
cnf(c261,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OKey(X2),
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
cnf(f274,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OKey(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I43_J_0) ).
fof(f274_nnf,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OKey(V_nat),
inference(nnf_transformation,[status(thm)],[f274]) ).
fof(f274_sk,plain,
! [V_nat_H,V_msg_H,V_nat] : c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OKey(V_nat),
inference(skolemisation,[status(esa)],[f274_nnf]) ).
cnf(c274,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OKey(X2),
inference(cnf_transformation,[status(esa)],[f274_sk]) ).
cnf(f275,axiom,
c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I42_J_0) ).
fof(f275_nnf,plain,
! [V_nat,V_nat_H,V_msg_H] : c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(nnf_transformation,[status(thm)],[f275]) ).
fof(f275_sk,plain,
! [V_nat,V_nat_H,V_msg_H] : c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
inference(skolemisation,[status(esa)],[f275_nnf]) ).
cnf(c275,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f275_sk]) ).
cnf(f283,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I4_J_0) ).
fof(f283_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)],[f283]) ).
fof(f283_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)],[f283_nnf]) ).
cnf(c283,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f283_sk]) ).
cnf(f284,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I6_J_0) ).
fof(f284_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)],[f284]) ).
fof(f284_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)],[f284_nnf]) ).
cnf(c284,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_ONotes(X3,X4),
inference(cnf_transformation,[status(esa)],[f284_sk]) ).
cnf(f285,axiom,
c_Event_Oevent_OGets(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I5_J_0) ).
fof(f285_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)],[f285]) ).
fof(f285_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)],[f285_nnf]) ).
cnf(c285,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f285_sk]) ).
cnf(f286,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I7_J_0) ).
fof(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(f306,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f306_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)],[f306]) ).
fof(f306_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)],[f306_nnf]) ).
cnf(c306,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
cnf(f317,axiom,
c_Event_Oevent_OGets(V_agent,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I8_J_0) ).
fof(f317_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)],[f317]) ).
fof(f317_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)],[f317_nnf]) ).
cnf(c317,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_ONotes(X2,X3),
inference(cnf_transformation,[status(esa)],[f317_sk]) ).
cnf(f337,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f337_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)],[f337]) ).
fof(f337_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)],[f337_nnf]) ).
cnf(c337,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f349,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OGets(V_agent,V_msg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_event_Osimps_I9_J_0) ).
fof(f349_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)],[f349]) ).
fof(f349_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)],[f349_nnf]) ).
cnf(c349,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OGets(X2,X3),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
cnf(f402,axiom,
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__iff__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__first__prop__iff_2) ).
fof(f402_nnf,plain,
! [V_P,V_ys,V_xs,T_a,V_xc] :
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__iff__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(nnf_transformation,[status(thm)],[f402]) ).
fof(f402_sk,plain,
! [V_P,V_ys,V_xs,T_a,V_xc] :
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__iff__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(skolemisation,[status(esa)],[f402_nnf]) ).
cnf(c402,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__iff__1__1(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f402_sk]) ).
cnf(f411,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__first__prop_2) ).
fof(f411_nnf,plain,
! [V_P,V_ys,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_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(nnf_transformation,[status(thm)],[f411]) ).
fof(f411_sk,plain,
! [V_P,V_ys,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_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(skolemisation,[status(esa)],[f411_nnf]) ).
cnf(c411,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__first__prop__1__1(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f411_sk]) ).
cnf(f412,axiom,
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__iff__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__last__prop__iff_2) ).
fof(f412_nnf,plain,
! [V_P,V_ys,V_xs,T_a,V_xc] :
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__iff__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(nnf_transformation,[status(thm)],[f412]) ).
fof(f412_sk,plain,
! [V_P,V_ys,V_xs,T_a,V_xc] :
( ~ c_in(V_xc,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xc))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__iff__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(skolemisation,[status(esa)],[f412_nnf]) ).
cnf(c412,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__iff__1__3(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f414,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__first_1) ).
fof(f414_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f414]) ).
fof(f414_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
inference(skolemisation,[status(esa)],[f414_nnf]) ).
cnf(c414,plain,
( ~ c_in(X0,c_List_Oset(X1,X2),X2)
| ~ c_in(X0,c_List_Oset(c_List_Osko__List__Xsplit__list__first__1__1(X0,X1,X2),X2),X2) ),
inference(cnf_transformation,[status(esa)],[f414_sk]) ).
cnf(f415,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| ~ c_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__last__propE__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__last__propE_2) ).
fof(f415_nnf,plain,
! [V_P,V_xa,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_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__last__propE__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
inference(nnf_transformation,[status(thm)],[f415]) ).
fof(f415_sk,plain,
! [V_P,V_xa,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_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__last__propE__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
inference(skolemisation,[status(esa)],[f415_nnf]) ).
cnf(c415,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__last__propE__1__3(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f415_sk]) ).
cnf(f417,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__set__conv__decomp__first_1) ).
fof(f417_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f417]) ).
fof(f417_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__first__1__1(V_x,V_xs,T_a),T_a),T_a) ),
inference(skolemisation,[status(esa)],[f417_nnf]) ).
cnf(c417,plain,
( ~ c_in(X0,c_List_Oset(X1,X2),X2)
| ~ c_in(X0,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__first__1__1(X0,X1,X2),X2),X2) ),
inference(cnf_transformation,[status(esa)],[f417_sk]) ).
cnf(f418,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__set__conv__decomp__last_1) ).
fof(f418_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f418]) ).
fof(f418_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
inference(skolemisation,[status(esa)],[f418_nnf]) ).
cnf(c418,plain,
( ~ c_in(X0,c_List_Oset(X1,X2),X2)
| ~ c_in(X0,c_List_Oset(c_List_Osko__List__Xin__set__conv__decomp__last__1__2(X0,X1,X2),X2),X2) ),
inference(cnf_transformation,[status(esa)],[f418_sk]) ).
cnf(f423,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| ~ c_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__last__prop_2) ).
fof(f423_nnf,plain,
! [V_P,V_ys,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_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(nnf_transformation,[status(thm)],[f423]) ).
fof(f423_sk,plain,
! [V_P,V_ys,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_in(V_ys,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__1__3(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_ys)) ),
inference(skolemisation,[status(esa)],[f423_nnf]) ).
cnf(c423,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__last__prop__1__3(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f423_sk]) ).
cnf(f430,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| ~ c_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__first__propE__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__first__propE_2) ).
fof(f430_nnf,plain,
! [V_P,V_xa,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_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__first__propE__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_P,V_xa,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_in(V_xa,c_List_Oset(c_List_Osko__List__Xsplit__list__first__propE__1__1(V_P,V_xs,T_a),T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_xa)) ),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c430,plain,
( ~ c_in(X4,c_List_Oset(X2,X3),X3)
| ~ hBOOL(hAPP(X0,X4))
| ~ c_in(X1,c_List_Oset(c_List_Osko__List__Xsplit__list__first__propE__1__1(X0,X2,X3),X3),X3)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
cnf(f432,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_split__list__last_1) ).
fof(f432_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f432]) ).
fof(f432_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(c_List_Osko__List__Xsplit__list__last__1__2(V_x,V_xs,T_a),T_a),T_a) ),
inference(skolemisation,[status(esa)],[f432_nnf]) ).
cnf(c432,plain,
( ~ c_in(X0,c_List_Oset(X1,X2),X2)
| ~ c_in(X0,c_List_Oset(c_List_Osko__List__Xsplit__list__last__1__2(X0,X1,X2),X2),X2) ),
inference(cnf_transformation,[status(esa)],[f432_sk]) ).
cnf(f454,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/sandbox2/benchmark/theBenchmark.p',cls_parts__emptyE_0) ).
fof(f454_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)],[f454]) ).
fof(f454_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)],[f454_nnf]) ).
cnf(c454,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)],[f454_sk]) ).
cnf(f463,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/sandbox2/benchmark/theBenchmark.p',cls_Crypt__notin__initState_0) ).
fof(f463_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)],[f463]) ).
fof(f463_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)],[f463_nnf]) ).
cnf(c463,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(c_Event_OinitState(X2)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f463_sk]) ).
cnf(f482,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I4_J_0) ).
fof(f482_nnf,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f482]) ).
fof(f482_sk,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f482_nnf]) ).
cnf(c482,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f482_sk]) ).
cnf(f484,axiom,
c_Message_Omsg_OMPair(V_msg1,V_msg2) != c_Message_Omsg_OCrypt(V_nat_H,V_msg_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I48_J_0) ).
fof(f484_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)],[f484]) ).
fof(f484_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)],[f484_nnf]) ).
cnf(c484,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OCrypt(X2,X3),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
cnf(f491,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f491_nnf,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f491]) ).
fof(f491_sk,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f491_nnf]) ).
cnf(c491,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f491_sk]) ).
cnf(f492,axiom,
c_Message_Omsg_OCrypt(V_nat_H,V_msg_H) != c_Message_Omsg_OMPair(V_msg1,V_msg2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_msg_Osimps_I49_J_0) ).
fof(f492_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)],[f492]) ).
fof(f492_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)],[f492_nnf]) ).
cnf(c492,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OMPair(X2,X3),
inference(cnf_transformation,[status(esa)],[f492_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c12,c13,c14,c15,c16,c47,c48,c52,c62,c75,c83,c84,c172,c221,c222,c223,c239,c241,c242,c248,c260,c261,c274,c275,c283,c284,c285,c286,c306,c317,c337,c349,c402,c411,c412,c414,c415,c417,c418,c423,c430,c432,c454,c463,c482,c484,c491,c492,c495]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t39348]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV722-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 21:02:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 58.08/7.83 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.08/7.83 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------