%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV721-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 : n007.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 212.15s 27.47s
% Output : Proof 212.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 45
% Syntax : Number of formulae : 206 ( 150 unt; 0 def)
% Number of atoms : 310 ( 118 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 370 ( 266 ~; 104 |; 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 : 43 ( 43 usr; 14 con; 0-4 aty)
% Number of variables : 614 ( 190 sgn 294 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f398,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(f398_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)],[f398]) ).
fof(f398_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)],[f398_nnf]) ).
cnf(c398,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)],[f398_sk]) ).
cnf(t121,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)],[c398]) ).
cnf(t345,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)],[t121]) ).
cnf(f407,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(f407_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)],[f407]) ).
fof(f407_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)],[f407_nnf]) ).
cnf(c407,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)],[f407_sk]) ).
cnf(t117,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)],[c407]) ).
cnf(t352,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)],[t117]) ).
cnf(f404,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(f404_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)],[f404]) ).
fof(f404_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)],[f404_nnf]) ).
cnf(c404,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)],[f404_sk]) ).
cnf(t174,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)],[c404]) ).
cnf(t364,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)],[t174]) ).
cnf(f417,negated_conjecture,
c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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(f417_nnf,plain,
c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[f417]) ).
cnf(c417,plain,
c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[f417_nnf]) ).
cnf(t137,plain,
c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[c417]) ).
cnf(t535,plain,
c_in(c_Event_Oevent_OSays(v_S,v_A,c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[t137]) ).
cnf(t551,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[t364,t535]) ).
cnf(t10,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t254,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t82858,plain,
true = c_in(c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[t551,t254]) ).
cnf(t78538,plain,
c_in(c_Message_Omsg_OCrypt(v_KA,c_Message_Omsg_OMPair(v_N,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)],[t82858]) ).
cnf(t78542,plain,
true = ifeq(true,true,c_in(c_Message_Omsg_OMPair(v_N,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)],[t352,t78538]) ).
cnf(t82859,plain,
true = c_in(c_Message_Omsg_OMPair(v_N,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)],[t78542,t254]) ).
cnf(t78566,plain,
c_in(c_Message_Omsg_OMPair(v_N,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)],[t82859]) ).
cnf(t78571,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)],[t345,t78566]) ).
cnf(t82883,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)],[t78571,t254]) ).
cnf(t80706,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)],[t82883]) ).
cnf(t80711,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)],[t345,t80706]) ).
cnf(t82895,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)],[t80711,t254]) ).
cnf(t81542,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)],[t82895]) ).
cnf(t81547,plain,
true = ifeq(true,true,c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),true),
inference(cp,[status(thm)],[t345,t81542]) ).
cnf(t82896,plain,
true = c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(step,[status(thm)],[t81547,t254]) ).
cnf(f418,negated_conjecture,
~ 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_conjecture_1) ).
fof(f418_nnf,plain,
~ c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f418]) ).
fof(f418_sk,plain,
~ c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f418_nnf]) ).
cnf(c418,plain,
~ c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f418_sk]) ).
cnf(t27,plain,
c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = false,
inference(equality_encoding,[status(esa)],[c418]) ).
cnf(t1426,plain,
c_in(v_X,c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs)),tc_Message_Omsg) = false,
inference(orient,[status(thm)],[t27]) ).
cnf(t82897,plain,
true = false,
inference(step,[status(thm)],[t82896,t1426]) ).
cnf(t81569,plain,
false = true,
inference(orient,[status(thm)],[t82897]) ).
cnf(f3,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(f3_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)],[f3]) ).
fof(f3_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)],[f3_nnf]) ).
cnf(c3,plain,
c_Public_OpublicKey(X0,X1) != c_Message_OinvKey(c_Public_OpublicKey(X2,X3)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(f4,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(f4_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)],[f4]) ).
fof(f4_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)],[f4_nnf]) ).
cnf(c4,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f5,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(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c5,plain,
c_Public_OshrK(X0) != c_Message_OinvKey(c_Public_OpublicKey(X1,X2)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f6,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(f6_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)],[f6]) ).
fof(f6_sk,plain,
! [V_A,V_b,V_C] : c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
c_Public_OshrK(X0) != c_Public_OpublicKey(X1,X2),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f8,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(f8_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)],[f8]) ).
fof(f8_sk,plain,
! [V_b,V_C,V_A] : c_Public_OpublicKey(V_b,V_C) != c_Public_OshrK(V_A),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
c_Public_OpublicKey(X0,X1) != c_Public_OshrK(X2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f11,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(f11_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)],[f11]) ).
fof(f11_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)],[f11_nnf]) ).
cnf(c11,plain,
c_Message_OinvKey(c_Public_OpublicKey(X0,X1)) != c_Public_OpublicKey(X2,X3),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f92,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(f92_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)],[f92]) ).
fof(f92_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)],[f92_nnf]) ).
cnf(c92,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(f152,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(f152_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)],[f152]) ).
fof(f152_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
cnf(f153,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(f153_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)],[f153]) ).
fof(f153_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f153_nnf]) ).
cnf(c153,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f153_sk]) ).
cnf(f169,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(f169_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)],[f169]) ).
fof(f169_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)],[f169_nnf]) ).
cnf(c169,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f169_sk]) ).
cnf(f171,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(f171_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)],[f171]) ).
fof(f171_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)],[f171_nnf]) ).
cnf(c171,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(f172,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(f172_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)],[f172]) ).
fof(f172_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)],[f172_nnf]) ).
cnf(c172,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(f178,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(f178_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)],[f178]) ).
fof(f178_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)],[f178_nnf]) ).
cnf(c178,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f190,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(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_OMPair(X1,X2),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f191,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(f191_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)],[f191]) ).
fof(f191_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)],[f191_nnf]) ).
cnf(c191,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OKey(X2),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f204,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(f204_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)],[f204]) ).
fof(f204_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)],[f204_nnf]) ).
cnf(c204,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OKey(X2),
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
cnf(f205,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(f205_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)],[f205]) ).
fof(f205_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)],[f205_nnf]) ).
cnf(c205,plain,
c_Message_Omsg_OKey(X0) != c_Message_Omsg_OCrypt(X1,X2),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f211,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(f211_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)],[f211]) ).
fof(f211_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)],[f211_nnf]) ).
cnf(c211,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f212,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(f212_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)],[f212]) ).
fof(f212_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)],[f212_nnf]) ).
cnf(c212,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_ONotes(X3,X4),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
cnf(f213,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(f213_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)],[f213]) ).
fof(f213_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)],[f213_nnf]) ).
cnf(c213,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(f214,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(f214_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)],[f214]) ).
fof(f214_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)],[f214_nnf]) ).
cnf(c214,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
cnf(f226,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(f226_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)],[f226]) ).
fof(f226_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)],[f226_nnf]) ).
cnf(c226,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f237,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(f237_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)],[f237]) ).
fof(f237_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)],[f237_nnf]) ).
cnf(c237,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_ONotes(X2,X3),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f257,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(f257_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)],[f257]) ).
fof(f257_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)],[f257_nnf]) ).
cnf(c257,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
cnf(f270,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(f270_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)],[f270]) ).
fof(f270_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)],[f270_nnf]) ).
cnf(c270,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OGets(X2,X3),
inference(cnf_transformation,[status(esa)],[f270_sk]) ).
cnf(f330,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(f330_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)],[f330]) ).
fof(f330_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)],[f330_nnf]) ).
cnf(c330,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)],[f330_sk]) ).
cnf(f339,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(f339_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)],[f339]) ).
fof(f339_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)],[f339_nnf]) ).
cnf(c339,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)],[f339_sk]) ).
cnf(f340,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(f340_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)],[f340]) ).
fof(f340_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)],[f340_nnf]) ).
cnf(c340,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)],[f340_sk]) ).
cnf(f342,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(f342_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)],[f342]) ).
fof(f342_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)],[f342_nnf]) ).
cnf(c342,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)],[f342_sk]) ).
cnf(f343,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(f343_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)],[f343]) ).
fof(f343_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)],[f343_nnf]) ).
cnf(c343,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)],[f343_sk]) ).
cnf(f345,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(f345_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)],[f345]) ).
fof(f345_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)],[f345_nnf]) ).
cnf(c345,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)],[f345_sk]) ).
cnf(f346,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(f346_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)],[f346]) ).
fof(f346_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)],[f346_nnf]) ).
cnf(c346,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)],[f346_sk]) ).
cnf(f351,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(f351_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)],[f351]) ).
fof(f351_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)],[f351_nnf]) ).
cnf(c351,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)],[f351_sk]) ).
cnf(f358,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(f358_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)],[f358]) ).
fof(f358_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)],[f358_nnf]) ).
cnf(c358,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)],[f358_sk]) ).
cnf(f360,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(f360_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)],[f360]) ).
fof(f360_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)],[f360_nnf]) ).
cnf(c360,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)],[f360_sk]) ).
cnf(f382,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(f382_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)],[f382]) ).
fof(f382_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)],[f382_nnf]) ).
cnf(c382,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)],[f382_sk]) ).
cnf(f391,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(f391_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)],[f391]) ).
fof(f391_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)],[f391_nnf]) ).
cnf(c391,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(c_Event_OinitState(X2)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f391_sk]) ).
cnf(f409,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(f409_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)],[f409]) ).
fof(f409_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)],[f409_nnf]) ).
cnf(c409,plain,
c_Message_Omsg_OMPair(X0,X1) != c_Message_Omsg_OCrypt(X2,X3),
inference(cnf_transformation,[status(esa)],[f409_sk]) ).
cnf(f416,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(f416_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)],[f416]) ).
fof(f416_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)],[f416_nnf]) ).
cnf(c416,plain,
c_Message_Omsg_OCrypt(X0,X1) != c_Message_Omsg_OMPair(X2,X3),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c3,c4,c5,c6,c8,c11,c92,c152,c153,c169,c171,c172,c178,c190,c191,c204,c205,c211,c212,c213,c214,c226,c237,c257,c270,c330,c339,c340,c342,c343,c345,c346,c351,c358,c360,c382,c391,c409,c416,c418]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t81569]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV721-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.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 20:57:37 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 212.15/27.47 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 212.15/27.47 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------