%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV779-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 : n012.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 4.91s 1.10s
% Output : Proof 4.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 22
% Syntax : Number of formulae : 96 ( 92 unt; 0 def)
% Number of atoms : 100 ( 83 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 82 ( 78 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-3 aty)
% Number of variables : 176 ( 60 sgn 86 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f428,negated_conjecture,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)) != c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f428_nnf,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)) != c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent))),
inference(nnf_transformation,[status(thm)],[f428]) ).
fof(f428_sk,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)) != c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent))),
inference(skolemisation,[status(esa)],[f428_nnf]) ).
cnf(c428,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)) != c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent))),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
cnf(t46,plain,
eq(c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent)))) = false,
inference(equality_encoding,[status(esa)],[c428]) ).
cnf(t70,axiom,
sF0 = c_List_Olist_ONil(tc_Event_Oevent),
introduced(definition) ).
cnf(t77,plain,
c_List_Olist_ONil(tc_Event_Oevent) = sF0,
inference(orient,[status(thm)],[t70]) ).
cnf(t483,plain,
eq(c_Event_Oknows(c_Message_Oagent_OSpy,sF0),c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent)))) = false,
inference(step,[status(thm)],[t46,t77]) ).
cnf(t71,axiom,
sF1 = c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent)),
introduced(definition) ).
cnf(t430,plain,
sF1 = c_Event_Oknows(c_Message_Oagent_OSpy,sF0),
inference(step,[status(thm)],[t71,t77]) ).
cnf(t82,plain,
c_Event_Oknows(c_Message_Oagent_OSpy,sF0) = sF1,
inference(orient,[status(thm)],[t430]) ).
cnf(t484,plain,
eq(sF1,c_Event_Oknows(c_Message_Oagent_OSpy,hAPP(c_List_Orev(tc_Event_Oevent),c_List_Olist_ONil(tc_Event_Oevent)))) = false,
inference(step,[status(thm)],[t483,t82]) ).
cnf(f420,axiom,
c_List_Olist_ONil(T_a) = hAPP(c_List_Orev(T_a),c_List_Olist_ONil(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nil__is__rev__conv_1) ).
fof(f420_nnf,plain,
! [T_a] : c_List_Olist_ONil(T_a) = hAPP(c_List_Orev(T_a),c_List_Olist_ONil(T_a)),
inference(nnf_transformation,[status(thm)],[f420]) ).
fof(f420_sk,plain,
! [T_a] : c_List_Olist_ONil(T_a) = hAPP(c_List_Orev(T_a),c_List_Olist_ONil(T_a)),
inference(skolemisation,[status(esa)],[f420_nnf]) ).
cnf(c420,plain,
c_List_Olist_ONil(X0) = hAPP(c_List_Orev(X0),c_List_Olist_ONil(X0)),
inference(cnf_transformation,[status(esa)],[f420_sk]) ).
cnf(t12,plain,
hAPP(c_List_Orev(X1),c_List_Olist_ONil(X1)) = c_List_Olist_ONil(X1),
inference(equality_encoding,[status(esa)],[c420]) ).
cnf(t90,plain,
hAPP(c_List_Orev(X1),c_List_Olist_ONil(X1)) = c_List_Olist_ONil(X1),
inference(orient,[status(thm)],[t12]) ).
cnf(t485,plain,
eq(sF1,c_Event_Oknows(c_Message_Oagent_OSpy,c_List_Olist_ONil(tc_Event_Oevent))) = false,
inference(step,[status(thm)],[t484,t90]) ).
cnf(t486,plain,
eq(sF1,c_Event_Oknows(c_Message_Oagent_OSpy,sF0)) = false,
inference(step,[status(thm)],[t485,t77]) ).
cnf(t487,plain,
eq(sF1,sF1) = false,
inference(step,[status(thm)],[t486,t82]) ).
cnf(t1,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t80,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t488,plain,
true = false,
inference(step,[status(thm)],[t487,t80]) ).
cnf(t404,plain,
false = true,
inference(orient,[status(thm)],[t488]) ).
cnf(f1,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(f1_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)],[f1]) ).
fof(f1_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)],[f1_nnf]) ).
cnf(c1,plain,
c_Event_Oevent_OGets(X0,X1) != c_Event_Oevent_OSays(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f2,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(f2_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)],[f2]) ).
fof(f2_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)],[f2_nnf]) ).
cnf(c2,plain,
c_Event_Oevent_OSays(X0,X1,X2) != c_Event_Oevent_OGets(X3,X4),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f97,axiom,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_impossible__Cons_0) ).
fof(f97_nnf,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c97,plain,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)),c_Nat_Osize__class_Osize(X1,tc_List_Olist(X2)),tc_nat),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(f155,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I2_J_0) ).
fof(f155_nnf,plain,
! [V_nat_H] : c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
inference(nnf_transformation,[status(thm)],[f155]) ).
fof(f155_sk,plain,
! [V_nat_H] : c_Message_Oagent_OServer != c_Message_Oagent_OFriend(V_nat_H),
inference(skolemisation,[status(esa)],[f155_nnf]) ).
cnf(c155,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OFriend(X0),
inference(cnf_transformation,[status(esa)],[f155_sk]) ).
cnf(f178,axiom,
c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I3_J_0) ).
fof(f178_nnf,plain,
! [V_nat_H] : c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [V_nat_H] : c_Message_Oagent_OFriend(V_nat_H) != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c178,plain,
c_Message_Oagent_OFriend(X0) != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f194,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(f194_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)],[f194]) ).
fof(f194_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f195,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(f195_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)],[f195]) ).
fof(f195_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(f223,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(f223_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)],[f223]) ).
fof(f223_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)],[f223_nnf]) ).
cnf(c223,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f248,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(f248_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)],[f248]) ).
fof(f248_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)],[f248_nnf]) ).
cnf(c248,plain,
( ~ hBOOL(hAPP(X0,X3))
| c_List_OdropWhile(X0,X1,X2) != c_List_Olist_OCons(X3,X4,X2) ),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(f291,axiom,
~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Onull_Osimps_I2_J_0) ).
fof(f291_nnf,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f291]) ).
fof(f291_sk,plain,
! [V_x,V_xs,T_a] : ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),
inference(skolemisation,[status(esa)],[f291_nnf]) ).
cnf(c291,plain,
~ c_List_Onull(c_List_Olist_OCons(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
cnf(f350,axiom,
~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list__ex_Osimps_I1_J_0) ).
fof(f350_nnf,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f350]) ).
fof(f350_sk,plain,
! [V_P,T_a] : ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f350_nnf]) ).
cnf(c350,plain,
~ c_List_Olist__ex(X0,c_List_Olist_ONil(X1),X1),
inference(cnf_transformation,[status(esa)],[f350_sk]) ).
cnf(f369,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(f369_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)],[f369]) ).
fof(f369_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)],[f369_nnf]) ).
cnf(c369,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(f370,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(f370_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)],[f370]) ).
fof(f370_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)],[f370_nnf]) ).
cnf(c370,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f370_sk]) ).
cnf(f390,axiom,
c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I6_J_0) ).
fof(f390_nnf,plain,
! [V_nat] : c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f390]) ).
fof(f390_sk,plain,
! [V_nat] : c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f390_nnf]) ).
cnf(c390,plain,
c_Message_Oagent_OFriend(X0) != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f390_sk]) ).
cnf(f392,axiom,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I4_J_0) ).
fof(f392_nnf,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(nnf_transformation,[status(thm)],[f392]) ).
fof(f392_sk,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(skolemisation,[status(esa)],[f392_nnf]) ).
cnf(c392,plain,
c_Message_Oagent_OServer != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(esa)],[f392_sk]) ).
cnf(f394,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I7_J_0) ).
fof(f394_nnf,plain,
! [V_nat] : c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
inference(nnf_transformation,[status(thm)],[f394]) ).
fof(f394_sk,plain,
! [V_nat] : c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(V_nat),
inference(skolemisation,[status(esa)],[f394_nnf]) ).
cnf(c394,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OFriend(X0),
inference(cnf_transformation,[status(esa)],[f394_sk]) ).
cnf(f395,axiom,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_agent_Osimps_I5_J_0) ).
fof(f395_nnf,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(nnf_transformation,[status(thm)],[f395]) ).
fof(f395_sk,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(skolemisation,[status(esa)],[f395_nnf]) ).
cnf(c395,plain,
c_Message_Oagent_OSpy != c_Message_Oagent_OServer,
inference(cnf_transformation,[status(esa)],[f395_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c2,c97,c155,c178,c194,c195,c223,c248,c291,c350,c369,c370,c390,c392,c394,c395,c428]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t404]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV779-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Thu Sep 24 21:04:09 UTC 2026
% 0.05/0.31 % CPUTime :
% 0.05/0.31 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.91/1.10 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.91/1.10 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------