%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV772-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:14:01 PM UTC 2026
% Result : Unsatisfiable 23.39s 3.43s
% Output : Proof 23.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 33
% Syntax : Number of formulae : 137 ( 73 unt; 0 def)
% Number of atoms : 245 ( 68 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 344 ( 236 ~; 108 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 9 con; 0-5 aty)
% Number of variables : 430 ( 104 sgn 208 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f400,axiom,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(V_A,V_B,V_X),V_evs,tc_Event_Oevent)) = c_Set_Oinsert(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_knows__Spy__Says_0) ).
fof(f400_nnf,plain,
! [V_A,V_B,V_X,V_evs] : c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(V_A,V_B,V_X),V_evs,tc_Event_Oevent)) = c_Set_Oinsert(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
! [V_A,V_B,V_X,V_evs] : c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(V_A,V_B,V_X),V_evs,tc_Event_Oevent)) = c_Set_Oinsert(V_X,c_Event_Oknows(c_Message_Oagent_OSpy,V_evs),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f400_nnf]) ).
cnf(c400,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(X0,X1,X2),X3,tc_Event_Oevent)) = c_Set_Oinsert(X2,c_Event_Oknows(c_Message_Oagent_OSpy,X3),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
cnf(t99,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(X1,X2,X3),X4,tc_Event_Oevent)) = c_Set_Oinsert(X3,c_Event_Oknows(c_Message_Oagent_OSpy,X4),tc_Message_Omsg),
inference(equality_encoding,[status(esa)],[c400]) ).
cnf(t863,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(X1,X2,X3),X4,tc_Event_Oevent)) = c_Set_Oinsert(X3,c_Event_Oknows(c_Message_Oagent_OSpy,X4),tc_Message_Omsg),
inference(orient,[status(thm)],[t99]) ).
cnf(t14,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t193,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(f7,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(f7_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)],[f7]) ).
fof(f7_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)],[f7_nnf]) ).
cnf(c7,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Message_Oparts(c_Event_OinitState(X2)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f40,axiom,
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f40_nnf,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [V_P,V_xs,T_a,V_y,V_ys] :
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(f67,axiom,
~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Crypt__notin__used__empty_0) ).
fof(f67_nnf,plain,
! [V_K,V_X] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [V_K,V_X] : ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
~ c_in(c_Message_Omsg_OCrypt(X0,X1),c_Event_Oused(c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(f72,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f72_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f72]) ).
fof(f72_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f72_nnf]) ).
cnf(c72,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(f73,axiom,
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f73_nnf,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c73,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_fun(X3,X0))
| ~ c_lessequals(X1,X2,tc_fun(X3,X0))
| ~ class_HOL_Oord(X0) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(f75,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f75_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f77,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f77_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(f79,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f79_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c79,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(f93,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f93_nnf,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(f95,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f95_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(f96,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f96_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(f97,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f97_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c97,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(f136,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f136_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f136_nnf]) ).
cnf(c136,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
cnf(f137,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f137_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c137,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
cnf(f138,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f138_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f138]) ).
fof(f138_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f138_nnf]) ).
cnf(c138,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f138_sk]) ).
cnf(f139,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f139_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f139]) ).
fof(f139_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f139_nnf]) ).
cnf(c139,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
cnf(f190,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(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f191,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(f191_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)],[f191]) ).
fof(f191_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)],[f191_nnf]) ).
cnf(c191,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_ONotes(X3,X4),
inference(cnf_transformation,[status(esa)],[f191_sk]) ).
cnf(f192,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(f192_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)],[f192]) ).
fof(f192_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)],[f192_nnf]) ).
cnf(c192,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
cnf(f193,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(f193_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)],[f193]) ).
fof(f193_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)],[f193_nnf]) ).
cnf(c193,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
cnf(f204,axiom,
( ~ c_List_Odistinct(c_List_Olinorder__class_Oinsort__key(V_f,V_x,V_xs,T_a,T_b),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ class_Orderings_Olinorder(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_distinct__insort_0) ).
fof(f204_nnf,plain,
! [T_b,V_x,V_xs,T_a,V_f] :
( ~ c_List_Odistinct(c_List_Olinorder__class_Oinsort__key(V_f,V_x,V_xs,T_a,T_b),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ class_Orderings_Olinorder(T_b) ),
inference(nnf_transformation,[status(thm)],[f204]) ).
fof(f204_sk,plain,
! [T_b,V_x,V_xs,T_a,V_f] :
( ~ c_List_Odistinct(c_List_Olinorder__class_Oinsort__key(V_f,V_x,V_xs,T_a,T_b),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ class_Orderings_Olinorder(T_b) ),
inference(skolemisation,[status(esa)],[f204_nnf]) ).
cnf(c204,plain,
( ~ c_List_Odistinct(c_List_Olinorder__class_Oinsort__key(X4,X1,X2,X3,X0),X3)
| ~ c_in(X1,c_List_Oset(X2,X3),X3)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
cnf(f220,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_filter__empty__conv_0) ).
fof(f220_nnf,plain,
! [V_P,V_xs,T_a,V_x] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [V_P,V_xs,T_a,V_x] :
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
( ~ c_in(X3,c_List_Oset(X1,X2),X2)
| ~ hBOOL(hAPP(X0,X3))
| c_List_Ofilter(X0,X1,X2) != c_List_Olist_ONil(X2) ),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(f227,axiom,
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_distinct_Osimps_I2_J_0) ).
fof(f227_nnf,plain,
! [V_x,V_xs,T_a] :
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f227]) ).
fof(f227_sk,plain,
! [V_x,V_xs,T_a] :
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
inference(skolemisation,[status(esa)],[f227_nnf]) ).
cnf(c227,plain,
( ~ c_List_Odistinct(c_List_Olist_OCons(X0,X1,X2),X2)
| ~ c_in(X0,c_List_Oset(X1,X2),X2) ),
inference(cnf_transformation,[status(esa)],[f227_sk]) ).
cnf(f301,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(f301_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)],[f301]) ).
fof(f301_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)],[f301_nnf]) ).
cnf(c301,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_ONotes(X2,X3),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
cnf(f315,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(f315_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)],[f315]) ).
fof(f315_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)],[f315_nnf]) ).
cnf(c315,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OGets(X2,X3),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
cnf(f411,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f411_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f411]) ).
fof(f411_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f411_nnf]) ).
cnf(c411,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f411_sk]) ).
cnf(f431,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f431_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f431]) ).
fof(f431_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f431_nnf]) ).
cnf(c431,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f431_sk]) ).
cnf(f432,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f432_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f432]) ).
fof(f432_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f432_nnf]) ).
cnf(c432,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f432_sk]) ).
cnf(f433,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(f433_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)],[f433]) ).
fof(f433_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f433_nnf]) ).
cnf(c433,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f433_sk]) ).
cnf(f434,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(f434_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)],[f434]) ).
fof(f434_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c434,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f437,negated_conjecture,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Oappend(c_List_Olist_ONil(tc_Event_Oevent),c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,v_X),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)) != c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f437_nnf,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Oappend(c_List_Olist_ONil(tc_Event_Oevent),c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,v_X),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)) != c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(nnf_transformation,[status(thm)],[f437]) ).
fof(f437_sk,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Oappend(c_List_Olist_ONil(tc_Event_Oevent),c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,v_X),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)) != c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(skolemisation,[status(esa)],[f437_nnf]) ).
cnf(c437,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Oappend(c_List_Olist_ONil(tc_Event_Oevent),c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,v_X),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent),tc_Event_Oevent)) != c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),
inference(cnf_transformation,[status(esa)],[f437_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7,c40,c67,c72,c73,c75,c77,c79,c93,c95,c96,c97,c136,c137,c138,c139,c190,c191,c192,c193,c204,c220,c227,c301,c315,c411,c431,c432,c433,c434,c437]) ).
cnf(g0_0,plain,
true != ifeq(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_OCons(c_Event_Oevent_OSays(v_A,v_B,v_X),c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),c_Set_Oinsert(v_X,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_Message_Omsg),false,true),
inference(rw,[status(thm)],[g0_0,t863]) ).
cnf(g0_2,plain,
true != false,
inference(rw,[status(thm)],[g0_1,t193]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV772-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 21:01:53 UTC 2026
% 0.14/0.37 % CPUTime :
% 0.14/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.39/3.43 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.39/3.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------