%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV781-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:02 PM UTC 2026
% Result : Unsatisfiable 19.32s 2.82s
% Output : Proof 19.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 24
% Syntax : Number of formulae : 105 ( 93 unt; 0 def)
% Number of atoms : 121 ( 88 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 124 ( 108 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-3 aty)
% Number of variables : 260 ( 96 sgn 126 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f519,axiom,
c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_takeWhile_Osimps_I1_J_0) ).
fof(f519_nnf,plain,
! [V_P,T_a] : c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f519]) ).
fof(f519_sk,plain,
! [V_P,T_a] : c_List_OtakeWhile(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f519_nnf]) ).
cnf(c519,plain,
c_List_OtakeWhile(X0,c_List_Olist_ONil(X1),X1) = c_List_Olist_ONil(X1),
inference(cnf_transformation,[status(esa)],[f519_sk]) ).
cnf(t22,plain,
c_List_OtakeWhile(X1,c_List_Olist_ONil(X2),X2) = c_List_Olist_ONil(X2),
inference(equality_encoding,[status(esa)],[c519]) ).
cnf(t1130,plain,
c_List_OtakeWhile(X1,c_List_Olist_ONil(X2),X2) = c_List_Olist_ONil(X2),
inference(orient,[status(thm)],[t22]) ).
cnf(f515,axiom,
c_lessequals(V_A,V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subset__refl_0) ).
fof(f515_nnf,plain,
! [V_A,T_a] : c_lessequals(V_A,V_A,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f515]) ).
fof(f515_sk,plain,
! [V_A,T_a] : c_lessequals(V_A,V_A,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f515_nnf]) ).
cnf(c515,plain,
c_lessequals(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f515_sk]) ).
cnf(t23,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c515]) ).
cnf(t440,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(f18,axiom,
( ~ c_List_Odistinct(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)
| ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_distinct_Osimps_I2_J_0) ).
fof(f18_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)],[f18]) ).
fof(f18_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)],[f18_nnf]) ).
cnf(c18,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)],[f18_sk]) ).
cnf(f34,axiom,
( ~ c_in(V_x,c_List_Oset(V_xs,T_a),T_a)
| ~ hBOOL(hAPP(V_P,V_x))
| c_List_Ofilter(V_P,V_xs,T_a) != c_List_Olist_ONil(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_filter__empty__conv_0) ).
fof(f34_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)],[f34]) ).
fof(f34_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)],[f34_nnf]) ).
cnf(c34,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)],[f34_sk]) ).
cnf(f86,axiom,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Server__not__bad_0) ).
fof(f86_nnf,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c86,plain,
~ c_in(c_Message_Oagent_OServer,c_Event_Obad,tc_Message_Oagent),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(f158,axiom,
( ~ hBOOL(hAPP(V_P,V_y))
| c_List_OdropWhile(V_P,V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dropWhile__eq__Cons__conv_1) ).
fof(f158_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)],[f158]) ).
fof(f158_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)],[f158_nnf]) ).
cnf(c158,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(f238,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I7_J_0) ).
fof(f238_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)],[f238]) ).
fof(f238_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)],[f238_nnf]) ).
cnf(c238,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f257,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f257_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)],[f257]) ).
fof(f257_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)],[f257_nnf]) ).
cnf(c257,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
cnf(f326,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f326_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)],[f326]) ).
fof(f326_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f326_nnf]) ).
cnf(c326,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(f327,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f327_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)],[f327]) ).
fof(f327_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f327_nnf]) ).
cnf(c327,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f327_sk]) ).
cnf(f333,axiom,
c_Event_Oevent_OGets(V_agent_H,V_msg_H) != c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I5_J_0) ).
fof(f333_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)],[f333]) ).
fof(f333_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)],[f333_nnf]) ).
cnf(c333,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
cnf(f339,axiom,
c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I3_J_0) ).
fof(f339_nnf,plain,
! [V_nat_H] : c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f339]) ).
fof(f339_sk,plain,
! [V_nat_H] : c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f339_nnf]) ).
cnf(c339,plain,
c_Message_Oagent_OFriend(X0) != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f339_sk]) ).
cnf(f355,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I2_J_0) ).
fof(f355_nnf,plain,
! [V_nat_H] : c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
inference(nnf_transformation,[status(thm)],[f355]) ).
fof(f355_sk,plain,
! [V_nat_H] : c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
inference(skolemisation,[status(esa)],[f355_nnf]) ).
cnf(c355,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OFriend(X0),
inference(cnf_transformation,[status(esa)],[f355_sk]) ).
cnf(f359,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I6_J_0) ).
fof(f359_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)],[f359]) ).
fof(f359_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)],[f359_nnf]) ).
cnf(c359,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_ONotes(X3,X4),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(f363,axiom,
c_Event_Oevent_OSays(V_agent1,V_agent2,V_msg) != c_Event_Oevent_OGets(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I4_J_0) ).
fof(f363_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)],[f363]) ).
fof(f363_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)],[f363_nnf]) ).
cnf(c363,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f363_sk]) ).
cnf(f383,axiom,
c_Event_Oevent_OGets(V_agent,V_msg) != c_Event_Oevent_ONotes(V_agent_H,V_msg_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I8_J_0) ).
fof(f383_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)],[f383]) ).
fof(f383_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)],[f383_nnf]) ).
cnf(c383,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_ONotes(X2,X3),
inference(cnf_transformation,[status(esa)],[f383_sk]) ).
cnf(f402,axiom,
c_Event_Oevent_ONotes(V_agent_H,V_msg_H) != c_Event_Oevent_OGets(V_agent,V_msg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_event_Osimps_I9_J_0) ).
fof(f402_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)],[f402]) ).
fof(f402_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)],[f402_nnf]) ).
cnf(c402,plain,
c_Event_Oevent_ONotes(X0,X1) != c_Event_Oevent_OGets(X2,X3),
inference(cnf_transformation,[status(esa)],[f402_sk]) ).
cnf(f433,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f433_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)],[f433]) ).
fof(f433_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)],[f433_nnf]) ).
cnf(c433,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f433_sk]) ).
cnf(f434,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f434_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)],[f434]) ).
fof(f434_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)],[f434_nnf]) ).
cnf(c434,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f451,axiom,
c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I6_J_0) ).
fof(f451_nnf,plain,
! [V_nat] : c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f451]) ).
fof(f451_sk,plain,
! [V_nat] : c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f451_nnf]) ).
cnf(c451,plain,
c_Message_Oagent_OFriend(X0) != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f451_sk]) ).
cnf(f453,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I4_J_0) ).
fof(f453_nnf,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f453]) ).
fof(f453_sk,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f453_nnf]) ).
cnf(c453,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f453_sk]) ).
cnf(f455,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I7_J_0) ).
fof(f455_nnf,plain,
! [V_nat] : c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
inference(nnf_transformation,[status(thm)],[f455]) ).
fof(f455_sk,plain,
! [V_nat] : c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
inference(skolemisation,[status(esa)],[f455_nnf]) ).
cnf(c455,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(X0),
inference(cnf_transformation,[status(esa)],[f455_sk]) ).
cnf(f456,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f456_nnf,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f456]) ).
fof(f456_sk,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f456_nnf]) ).
cnf(c456,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(f526,negated_conjecture,
~ c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(v_P,c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f526_nnf,plain,
~ c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(v_P,c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)),
inference(nnf_transformation,[status(thm)],[f526]) ).
fof(f526_sk,plain,
~ c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(v_P,c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)),
inference(skolemisation,[status(esa)],[f526_nnf]) ).
cnf(c526,plain,
~ c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(v_P,c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)),
inference(cnf_transformation,[status(esa)],[f526_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c18,c34,c86,c158,c238,c257,c326,c327,c333,c339,c355,c359,c363,c383,c402,c433,c434,c451,c453,c455,c456,c526]) ).
cnf(g0_0,plain,
c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_OtakeWhile(v_P,c_List_Olist_ONil(tc_Event_Oevent),tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)) != false,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
c_lessequals(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),tc_fun(tc_Message_Omsg,tc_bool)) != false,
inference(rw,[status(thm)],[g0_0,t1130]) ).
cnf(g0_2,plain,
true != false,
inference(rw,[status(thm)],[g0_1,t440]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV781-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n017.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 20:59:31 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.32/2.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.32/2.82 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------