%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV283-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:50:25 PM UTC 2026
% Result : Unsatisfiable 133.60s 17.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV283-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:36:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 133.60/17.35 % Refutation found
% 133.60/17.35 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 133.60/17.35 % SZS output start CNFRefutation for theBenchmark
% 133.60/17.35 fof(f48,axiom,(
% 133.60/17.35 (![V_A,V_xs,T_a]: (( ~ c_in(c_Main_Oin__listsI__1(V_A,V_xs,T_a),V_A,T_a)| c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f59,axiom,(
% 133.60/17.35 (![V_x,V_l,T_a,V_A]: (( ~ c_in(c_List_Olist_OCons(V_x,V_l,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a))| c_in(V_x,V_A,T_a) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f61,axiom,(
% 133.60/17.35 (![V_A,T_a]: (c_in(c_List_Olist_ONil,c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f68,axiom,(
% 133.60/17.35 (![T_a,V_x]: (( ~ class_Orderings_Oorder(T_a)| c_lessequals(V_x,V_x,T_a) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f70,axiom,(
% 133.60/17.35 (![V_a,V_b,T_a,T_b,V_r]: (( ~ c_in(c_Pair(V_a,V_b,T_a,T_b),V_r,tc_prod(T_a,T_b))| c_in(V_a,c_Relation_ODomain(V_r,T_a,T_b),T_a) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f75,axiom,(
% 133.60/17.35 (![V_b,V_r,T_b,T_a]: (( ~ c_in(V_b,c_Relation_ORange(V_r,T_b,T_a),T_a)| c_in(c_Pair(c_Main_ORangeE__1(V_b,V_r,T_a,T_b),V_b,T_b,T_a),V_r,tc_prod(T_b,T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f76,axiom,(
% 133.60/17.35 (![V_a,V_b,T_a,T_b,V_r]: (( ~ c_in(c_Pair(V_a,V_b,T_a,T_b),V_r,tc_prod(T_a,T_b))| c_in(V_b,c_Relation_ORange(V_r,T_a,T_b),T_b) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f86,axiom,(
% 133.60/17.35 (![V_l,V_u]: (c_in(c_SetInterval_OatLeastAtMost(V_l,V_u,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f94,axiom,(
% 133.60/17.35 (![V_l,V_u]: (c_in(c_SetInterval_OgreaterThanLessThan(V_l,V_u,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f95,axiom,(
% 133.60/17.35 (![V_k]: (c_in(c_SetInterval_OlessThan(V_k,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f96,axiom,(
% 133.60/17.35 (![V_A,V_C,T_a]: (( c_in(V_A,c_Inter(V_C,T_a),T_a)| c_in(c_Main_OInterI__1(V_A,V_C,T_a),V_C,tc_set(T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f98,axiom,(
% 133.60/17.35 (![V_x,T_a]: (c_in(V_x,c_UNIV,T_a) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f101,axiom,(
% 133.60/17.35 (![V_A,T_a]: (c_lessequals(c_emptyset,V_A,tc_set(T_a)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f102,axiom,(
% 133.60/17.35 (![V_A,V_B,T_a]: (( ~ c_less(V_A,V_B,tc_set(T_a))| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f109,axiom,(
% 133.60/17.35 (![V_A,V_B,T_a]: (( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a)| c_lessequals(V_A,V_B,tc_set(T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f110,axiom,(
% 133.60/17.35 (![V_A,V_B,T_a]: (( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a)| c_lessequals(V_A,V_B,tc_set(T_a)) ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f111,axiom,(
% 133.60/17.35 (![V_B,V_A,T_a]: (( ~ c_lessequals(V_B,V_A,tc_set(T_a))| ~ c_lessequals(V_A,V_B,tc_set(T_a))| V_A = V_B ) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f112,axiom,(
% 133.60/17.35 (![V_A,T_a]: (c_lessequals(V_A,V_A,tc_set(T_a)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f120,axiom,(
% 133.60/17.35 (![V_a,T_a,V_r]: (c_in(c_Pair(V_a,V_a,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) ))),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f154,axiom,(
% 133.60/17.35 class_Orderings_Oorder(tc_IntDef_Oint) ),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f174,axiom,(
% 133.60/17.35 class_Orderings_Oord(tc_IntDef_Oint) ),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f210,axiom,(
% 133.60/17.35 class_Orderings_Oord(tc_nat) ),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.35 fof(f221,axiom,(
% 133.60/17.35 class_Orderings_Oorder(tc_nat) ),
% 133.60/17.35 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f243,axiom,(
% 133.60/17.36 class_Orderings_Olinorder(tc_nat) ),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f248,axiom,(
% 133.60/17.36 (![T_1]: (class_Orderings_Oord(tc_set(T_1)) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f249,axiom,(
% 133.60/17.36 (![T_1]: (class_Orderings_Oorder(tc_set(T_1)) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f454,axiom,(
% 133.60/17.36 (![T]: (( ~ class_Orderings_Oorder(T)| class_Orderings_Oord(T) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1161,axiom,(
% 133.60/17.36 (![V_x,T_a]: (c_in(V_x,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(V_x,T_a),T_a),T_a) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1164,axiom,(
% 133.60/17.36 (![V_a_H,T_a]: (c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1238,axiom,(
% 133.60/17.36 (![V_a_H,V_list_H,T_a]: (c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1261,axiom,(
% 133.60/17.36 (![V_m]: (c_Suc(V_m) != c_0 ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1279,axiom,(
% 133.60/17.36 (![V_n]: (~ c_less(V_n,c_0,tc_nat) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1285,axiom,(
% 133.60/17.36 (![V_a,T_a]: (c_in(c_Pair(V_a,V_a,T_a,T_a),c_Relation_OId,tc_prod(T_a,T_a)) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1293,axiom,(
% 133.60/17.36 (![T_a,V_k,V_i]: (( ~ class_Orderings_Oord(T_a)| ~ c_lessequals(V_k,V_i,T_a)| c_in(V_i,c_SetInterval_OatLeast(V_k,T_a),T_a) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1298,axiom,(
% 133.60/17.36 (![T_a,V_i,V_k]: (( ~ class_Orderings_Oord(T_a)| ~ c_lessequals(V_i,V_k,T_a)| c_in(V_i,c_SetInterval_OatMost(V_k,T_a),T_a) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1325,axiom,(
% 133.60/17.36 c_UNIV != c_emptyset ),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1333,axiom,(
% 133.60/17.36 (![V_a,T_a]: (~ c_in(V_a,c_emptyset,T_a) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1334,axiom,(
% 133.60/17.36 (![V_a,V_B,T_a,V_b]: (( ~ c_in(V_a,V_B,T_a)| c_in(V_a,c_insert(V_b,V_B,T_a),T_a) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1335,axiom,(
% 133.60/17.36 (![V_x,V_B,T_a]: (c_in(V_x,c_insert(V_x,V_B,T_a),T_a) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1336,axiom,(
% 133.60/17.36 (![V_a,V_b,V_A,T_a]: (( ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a)| c_in(V_a,V_A,T_a)| V_a = V_b ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1359,axiom,(
% 133.60/17.36 c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent) ),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1382,axiom,(
% 133.60/17.36 (![V_N,V_X,V_Y]: (c_Message_Omsg_ONonce(V_N) != c_Message_OHPair(V_X,V_Y) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1384,axiom,(
% 133.60/17.36 (![V_K,V_X,V_Y]: (c_Message_Omsg_OKey(V_K) != c_Message_OHPair(V_X,V_Y) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1401,axiom,(
% 133.60/17.36 (![V_X,V_Y,V_H]: (( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg)| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1412,axiom,(
% 133.60/17.36 (![V_nat]: (c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1418,axiom,(
% 133.60/17.36 (![V_agent,V_agent_H]: (( c_Message_Omsg_OAgent(V_agent) != c_Message_Omsg_OAgent(V_agent_H)| V_agent = V_agent_H ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1419,axiom,(
% 133.60/17.36 (![V_nat,V_nat_H]: (( c_Message_Omsg_ONumber(V_nat) != c_Message_Omsg_ONumber(V_nat_H)| V_nat = V_nat_H ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1421,axiom,(
% 133.60/17.36 (![V_nat,V_nat_H]: (( c_Message_Omsg_OKey(V_nat) != c_Message_Omsg_OKey(V_nat_H)| V_nat = V_nat_H ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1427,axiom,(
% 133.60/17.36 (![V_X,V_H]: (( ~ c_in(V_X,V_H,tc_Message_Omsg)| c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1435,axiom,(
% 133.60/17.36 (![V_n,V_H]: (c_in(c_Message_Omsg_ONumber(V_n),c_Message_Osynth(V_H),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1438,axiom,(
% 133.60/17.36 (![V_U,V_msg]: (( ~ c_in(c_Message_Omsg_ONonce(V_U),c_Message_Oparts(c_insert(V_msg,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)| ~ c_lessequals(v_sko__upX(V_msg),V_U,tc_nat) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1439,axiom,(
% 133.60/17.36 (![V_m,V_k,V_n]: (( ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat)| c_lessequals(V_k,V_n,tc_nat) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1440,axiom,(
% 133.60/17.36 (![V_m,V_k,V_n]: (( ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat)| c_lessequals(V_m,V_n,tc_nat) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1443,axiom,(
% 133.60/17.36 (![V_N,V_B]: (~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(c_Event_OinitState(V_B)),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1455,axiom,(
% 133.60/17.36 (![V_A,V_b,V_C]: (c_Public_OshrK(V_A) != c_Public_OpublicKey(V_b,V_C) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1459,axiom,(
% 133.60/17.36 (![V_b,V_A,V_evs]: (c_in(c_Message_Omsg_OKey(c_Public_OpublicKey(V_b,V_A)),c_Event_Oused(V_evs),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1461,axiom,(
% 133.60/17.36 (![V_X]: (c_in(c_Public_OshrK(V_X),c_Message_OsymKeys,tc_nat) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1462,axiom,(
% 133.60/17.36 (![V_A]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Event_OinitState(V_A),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1463,axiom,(
% 133.60/17.36 (![V_A,V_evs]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Event_Oknows(V_A,V_evs),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1464,axiom,(
% 133.60/17.36 (![V_A,V_evs]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(V_A)),c_Event_Oused(V_evs),tc_Message_Omsg) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1469,negated_conjecture,(
% 133.60/17.36 (![V_U]: (( ~ c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(v_list),tc_Message_Omsg)| ~ c_lessequals(v_x,V_U,tc_nat) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1473,negated_conjecture,(
% 133.60/17.36 (![V_W,V_U]: (( c_lessequals(V_W,v_xd(V_W),tc_nat)| c_lessequals(V_U,v_xd(V_U),tc_nat) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1478,negated_conjecture,(
% 133.60/17.36 (![V_X,V_U]: (( c_in(c_Message_Omsg_ONonce(v_xd(V_X)),c_Event_Oused(v_list),tc_Message_Omsg)| c_in(c_Message_Omsg_ONonce(v_xd(V_X)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)| c_in(c_Message_Omsg_ONonce(v_xd(V_U)),c_Event_Oused(v_list),tc_Message_Omsg)| c_in(c_Message_Omsg_ONonce(v_xd(V_U)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg) ) ))),
% 133.60/17.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 133.60/17.36 fof(f1545,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_in(c_Main_Oin__listsI__1(X0,X1,X2),X0,X2)|c_in(X1,c_List_Olists(X0,X2),tc_List_Olist(X2)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f48])).
% 133.60/17.36 fof(f1559,plain,(
% 133.60/17.36 ![V_x,T_a,V_A]: ((![V_l]: ~c_in(c_List_Olist_OCons(V_x,V_l,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a)))|c_in(V_x,V_A,T_a))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f59])).
% 133.60/17.36 fof(f1560,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (~c_in(c_List_Olist_OCons(X0,X1,X2),c_List_Olists(X3,X2),tc_List_Olist(X2))|c_in(X0,X3,X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1559])).
% 133.60/17.36 fof(f1562,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_List_Olist_ONil,c_List_Olists(X0,X1),tc_List_Olist(X1)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f61])).
% 133.60/17.36 fof(f1569,plain,(
% 133.60/17.36 ![T_a]: (~class_Orderings_Oorder(T_a)|(![V_x]: c_lessequals(V_x,V_x,T_a)))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f68])).
% 133.60/17.36 fof(f1570,plain,(
% 133.60/17.36 ![X0,X1]: (~class_Orderings_Oorder(X0)|c_lessequals(X1,X1,X0))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1569])).
% 133.60/17.36 fof(f1572,plain,(
% 133.60/17.36 ![V_a,T_a,T_b,V_r]: ((![V_b]: ~c_in(c_Pair(V_a,V_b,T_a,T_b),V_r,tc_prod(T_a,T_b)))|c_in(V_a,c_Relation_ODomain(V_r,T_a,T_b),T_a))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f70])).
% 133.60/17.36 fof(f1573,plain,(
% 133.60/17.36 ![X0,X1,X2,X3,X4]: (~c_in(c_Pair(X0,X1,X2,X3),X4,tc_prod(X2,X3))|c_in(X0,c_Relation_ODomain(X4,X2,X3),X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1572])).
% 133.60/17.36 fof(f1579,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (~c_in(X0,c_Relation_ORange(X1,X2,X3),X3)|c_in(c_Pair(c_Main_ORangeE__1(X0,X1,X3,X2),X0,X2,X3),X1,tc_prod(X2,X3)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f75])).
% 133.60/17.36 fof(f1580,plain,(
% 133.60/17.36 ![V_b,T_a,T_b,V_r]: ((![V_a]: ~c_in(c_Pair(V_a,V_b,T_a,T_b),V_r,tc_prod(T_a,T_b)))|c_in(V_b,c_Relation_ORange(V_r,T_a,T_b),T_b))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f76])).
% 133.60/17.36 fof(f1581,plain,(
% 133.60/17.36 ![X0,X1,X2,X3,X4]: (~c_in(c_Pair(X0,X1,X2,X3),X4,tc_prod(X2,X3))|c_in(X1,c_Relation_ORange(X4,X2,X3),X3))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1580])).
% 133.60/17.36 fof(f1592,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_SetInterval_OatLeastAtMost(X0,X1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f86])).
% 133.60/17.36 fof(f1600,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f94])).
% 133.60/17.36 fof(f1601,plain,(
% 133.60/17.36 ![X0]: (c_in(c_SetInterval_OlessThan(X0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f95])).
% 133.60/17.36 fof(f1602,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_Inter(X1,X2),X2)|c_in(c_Main_OInterI__1(X0,X1,X2),X1,tc_set(X2)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f96])).
% 133.60/17.36 fof(f1604,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(X0,c_UNIV,X1))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f98])).
% 133.60/17.36 fof(f1607,plain,(
% 133.60/17.36 ![X0,X1]: (c_lessequals(c_emptyset,X0,tc_set(X1)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f101])).
% 133.60/17.36 fof(f1608,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_less(X0,X1,tc_set(X2))|~c_lessequals(X1,X0,tc_set(X2)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f102])).
% 133.60/17.36 fof(f1619,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)|c_lessequals(X0,X1,tc_set(X2)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f109])).
% 133.60/17.36 fof(f1620,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)|c_lessequals(X0,X1,tc_set(X2)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f110])).
% 133.60/17.36 fof(f1621,plain,(
% 133.60/17.36 ![V_B,V_A]: ((![T_a]: (~c_lessequals(V_B,V_A,tc_set(T_a))|~c_lessequals(V_A,V_B,tc_set(T_a))))|V_A=V_B)),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f111])).
% 133.60/17.36 fof(f1622,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_lessequals(X0,X1,tc_set(X2))|~c_lessequals(X1,X0,tc_set(X2))|X1=X0)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1621])).
% 133.60/17.36 fof(f1623,plain,(
% 133.60/17.36 ![X0,X1]: (c_lessequals(X0,X0,tc_set(X1)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f112])).
% 133.60/17.36 fof(f1637,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(c_Pair(X0,X0,X1,X1),c_Transitive__Closure_Ortrancl(X2,X1),tc_prod(X1,X1)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f120])).
% 133.60/17.36 fof(f1671,plain,(
% 133.60/17.36 class_Orderings_Oorder(tc_IntDef_Oint)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f154])).
% 133.60/17.36 fof(f1691,plain,(
% 133.60/17.36 class_Orderings_Oord(tc_IntDef_Oint)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f174])).
% 133.60/17.36 fof(f1728,plain,(
% 133.60/17.36 class_Orderings_Oord(tc_nat)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f210])).
% 133.60/17.36 fof(f1739,plain,(
% 133.60/17.36 class_Orderings_Oorder(tc_nat)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f221])).
% 133.60/17.36 fof(f1761,plain,(
% 133.60/17.36 class_Orderings_Olinorder(tc_nat)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f243])).
% 133.60/17.36 fof(f1767,plain,(
% 133.60/17.36 ![X0]: (class_Orderings_Oord(tc_set(X0)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f248])).
% 133.60/17.36 fof(f1768,plain,(
% 133.60/17.36 ![X0]: (class_Orderings_Oorder(tc_set(X0)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f249])).
% 133.60/17.36 fof(f1974,plain,(
% 133.60/17.36 ![X0]: (~class_Orderings_Oorder(X0)|class_Orderings_Oord(X0))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f454])).
% 133.60/17.36 fof(f2681,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(X0,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(X0,X1),X1),X1))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1161])).
% 133.60/17.36 fof(f2686,plain,(
% 133.60/17.36 ![X0,X1]: (~c_Datatype_Ooption_ONone=c_Datatype_Ooption_OSome(X0,X1))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1164])).
% 133.60/17.36 fof(f2790,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_List_Olist_ONil=c_List_Olist_OCons(X0,X1,X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1238])).
% 133.60/17.36 fof(f2822,plain,(
% 133.60/17.36 ![X0]: (~c_Suc(X0)=c_0)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1261])).
% 133.60/17.36 fof(f2845,plain,(
% 133.60/17.36 ![X0]: (~c_less(X0,c_0,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1279])).
% 133.60/17.36 fof(f2854,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_Pair(X0,X0,X1,X1),c_Relation_OId,tc_prod(X1,X1)))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1285])).
% 133.60/17.36 fof(f2864,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~class_Orderings_Oord(X0)|~c_lessequals(X1,X2,X0)|c_in(X2,c_SetInterval_OatLeast(X1,X0),X0))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1293])).
% 133.60/17.36 fof(f2870,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~class_Orderings_Oord(X0)|~c_lessequals(X1,X2,X0)|c_in(X1,c_SetInterval_OatMost(X2,X0),X0))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1298])).
% 133.60/17.36 fof(f2905,plain,(
% 133.60/17.36 ~c_UNIV=c_emptyset),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1325])).
% 133.60/17.36 fof(f2919,plain,(
% 133.60/17.36 ![X0,X1]: (~c_in(X0,c_emptyset,X1))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1333])).
% 133.60/17.36 fof(f2920,plain,(
% 133.60/17.36 ![V_a,V_B,T_a]: (~c_in(V_a,V_B,T_a)|(![V_b]: c_in(V_a,c_insert(V_b,V_B,T_a),T_a)))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1334])).
% 133.60/17.36 fof(f2921,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (~c_in(X0,X1,X2)|c_in(X0,c_insert(X3,X1,X2),X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f2920])).
% 133.60/17.36 fof(f2922,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_insert(X0,X1,X2),X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1335])).
% 133.60/17.36 fof(f2923,plain,(
% 133.60/17.36 ![V_a,V_b]: ((![V_A,T_a]: (~c_in(V_a,c_insert(V_b,V_A,T_a),T_a)|c_in(V_a,V_A,T_a)))|V_a=V_b)),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1336])).
% 133.60/17.36 fof(f2924,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (~c_in(X0,c_insert(X1,X2,X3),X3)|c_in(X0,X2,X3)|X0=X1)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f2923])).
% 133.60/17.36 fof(f2955,plain,(
% 133.60/17.36 c_in(c_Message_Oagent_OSpy,c_Event_Obad,tc_Message_Oagent)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1359])).
% 133.60/17.36 fof(f2990,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_Message_Omsg_ONonce(X0)=c_Message_OHPair(X1,X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1382])).
% 133.60/17.36 fof(f2992,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_Message_Omsg_OKey(X0)=c_Message_OHPair(X1,X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1384])).
% 133.60/17.36 fof(f3014,plain,(
% 133.60/17.36 ![V_X,V_H]: ((![V_Y]: ~c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg))|c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1401])).
% 133.60/17.36 fof(f3015,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg)|c_in(X0,c_Message_Oparts(X2),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f3014])).
% 133.60/17.36 fof(f3028,plain,(
% 133.60/17.36 ![X0]: (~c_Message_Oagent_OFriend(X0)=c_Message_Oagent_OSpy)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1412])).
% 133.60/17.36 fof(f3035,plain,(
% 133.60/17.36 ![X0,X1]: (~c_Message_Omsg_OAgent(X0)=c_Message_Omsg_OAgent(X1)|X0=X1)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1418])).
% 133.60/17.36 fof(f3036,plain,(
% 133.60/17.36 ![X0,X1]: (~c_Message_Omsg_ONumber(X0)=c_Message_Omsg_ONumber(X1)|X0=X1)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1419])).
% 133.60/17.36 fof(f3038,plain,(
% 133.60/17.36 ![X0,X1]: (~c_Message_Omsg_OKey(X0)=c_Message_Omsg_OKey(X1)|X0=X1)),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1421])).
% 133.60/17.36 fof(f3048,plain,(
% 133.60/17.36 ![X0,X1]: (~c_in(X0,X1,tc_Message_Omsg)|c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1427])).
% 133.60/17.36 fof(f3056,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_Message_Omsg_ONumber(X0),c_Message_Osynth(X1),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1435])).
% 133.60/17.36 fof(f3060,plain,(
% 133.60/17.36 ![X0,X1]: (~c_in(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_insert(X1,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)|~c_lessequals(v_sko__upX(X1),X0,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1438])).
% 133.60/17.36 fof(f3061,plain,(
% 133.60/17.36 ![V_k,V_n]: ((![V_m]: ~c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat))|c_lessequals(V_k,V_n,tc_nat))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1439])).
% 133.60/17.36 fof(f3062,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_lessequals(c_plus(X0,X1,tc_nat),X2,tc_nat)|c_lessequals(X1,X2,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f3061])).
% 133.60/17.36 fof(f3063,plain,(
% 133.60/17.36 ![V_m,V_n]: ((![V_k]: ~c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat))|c_lessequals(V_m,V_n,tc_nat))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1440])).
% 133.60/17.36 fof(f3064,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_lessequals(c_plus(X0,X1,tc_nat),X2,tc_nat)|c_lessequals(X0,X2,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f3063])).
% 133.60/17.36 fof(f3069,plain,(
% 133.60/17.36 ![X0,X1]: (~c_in(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_Event_OinitState(X1)),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1443])).
% 133.60/17.36 fof(f3083,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_Public_OshrK(X0)=c_Public_OpublicKey(X1,X2))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1455])).
% 133.60/17.36 fof(f3089,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(c_Message_Omsg_OKey(c_Public_OpublicKey(X0,X1)),c_Event_Oused(X2),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1459])).
% 133.60/17.36 fof(f3091,plain,(
% 133.60/17.36 ![X0]: (c_in(c_Public_OshrK(X0),c_Message_OsymKeys,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1461])).
% 133.60/17.36 fof(f3092,plain,(
% 133.60/17.36 ![X0]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_OinitState(X0),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1462])).
% 133.60/17.36 fof(f3093,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_Oknows(X0,X1),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1463])).
% 133.60/17.36 fof(f3094,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_Oused(X1),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1464])).
% 133.60/17.36 fof(f3099,plain,(
% 133.60/17.36 ![X0]: (~c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_list),tc_Message_Omsg)|~c_lessequals(v_x,X0,tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f1469])).
% 133.60/17.36 fof(f3105,plain,(
% 133.60/17.36 (![V_W]: c_lessequals(V_W,v_xd(V_W),tc_nat))|(![V_U]: c_lessequals(V_U,v_xd(V_U),tc_nat))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1473])).
% 133.60/17.36 fof(f3106,plain,(
% 133.60/17.36 ![X0,X1]: (c_lessequals(X0,v_xd(X0),tc_nat)|c_lessequals(X1,v_xd(X1),tc_nat))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f3105])).
% 133.60/17.36 fof(f3114,plain,(
% 133.60/17.36 ![V_U]: (((![V_X]: (c_in(c_Message_Omsg_ONonce(v_xd(V_X)),c_Event_Oused(v_list),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(V_X)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)))|c_in(c_Message_Omsg_ONonce(v_xd(V_U)),c_Event_Oused(v_list),tc_Message_Omsg))|c_in(c_Message_Omsg_ONonce(v_xd(V_U)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg))),
% 133.60/17.36 inference(miniscoping,[status(thm)],[f1478])).
% 133.60/17.36 fof(f3115,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Event_Oused(v_list),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(X1)),c_Event_Oused(v_list),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(X1)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg))),
% 133.60/17.36 inference(cnf_transformation,[status(thm)],[f3114])).
% 133.60/17.36 fof(f3123,definition,(
% 133.60/17.36 ![X0]: (sQ2_spl <=> (c_lessequals(X0,v_xd(X0),tc_nat)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f3124,plain,(
% 133.60/17.36 ![X0]: (c_lessequals(X0,v_xd(X0),tc_nat)|~sQ2_spl)),
% 133.60/17.36 inference(component_clause,[status(thm)],[f3123])).
% 133.60/17.36 fof(f3128,plain,(
% 133.60/17.36 sQ2_spl),
% 133.60/17.36 inference(split_clause,[status(thm)],[f3106,f3123])).
% 133.60/17.36 fof(f3129,definition,(
% 133.60/17.36 ![X0]: (sQ3_spl <=> (c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Event_Oused(v_list),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f3130,plain,(
% 133.60/17.36 ![X0]: (c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Event_Oused(v_list),tc_Message_Omsg)|c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)|~sQ3_spl)),
% 133.60/17.36 inference(component_clause,[status(thm)],[f3129])).
% 133.60/17.36 fof(f3136,plain,(
% 133.60/17.36 sQ3_spl),
% 133.60/17.36 inference(split_clause,[status(thm)],[f3115,f3129])).
% 133.60/17.36 fof(f3146,definition,(
% 133.60/17.36 sQ4_spl <=> (v_a=v_a)),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f3148,plain,(
% 133.60/17.36 ~v_a=v_a|sQ4_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f3146])).
% 133.60/17.36 fof(f3165,plain,(
% 133.60/17.36 $false|sQ4_spl),
% 133.60/17.36 inference(trivial_equality_resolution,[status(thm)],[f3148])).
% 133.60/17.36 fof(f3166,plain,(
% 133.60/17.36 sQ4_spl),
% 133.60/17.36 inference(contradiction_clause,[status(thm)],[f3165])).
% 133.60/17.36 fof(f3240,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)|~c_in(c_Message_Omsg_OMPair(X0,X2),X1,tc_Message_Omsg))),
% 133.60/17.36 inference(resolution,[status(thm)],[f3015,f3048])).
% 133.60/17.36 fof(f4168,plain,(
% 133.60/17.36 ![X0]: (c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1604,f3240])).
% 133.60/17.36 fof(f4207,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (c_in(X0,c_List_Olists(c_insert(X1,X2,X3),X3),tc_List_Olist(X3))|~c_in(c_Main_Oin__listsI__1(c_insert(X1,X2,X3),X0,X3),X2,X3))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1545,f2921])).
% 133.60/17.36 fof(f4271,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_List_Olists(c_insert(X1,c_UNIV,X2),X2),tc_List_Olist(X2)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f4207,f1604])).
% 133.60/17.36 fof(f4646,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_insert(X1,c_UNIV,X2),X2))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1560,f4271])).
% 133.60/17.36 fof(f4987,definition,(
% 133.60/17.36 ![X0]: (sQ8_spl <=> (~class_Orderings_Oorder(tc_set(X0))))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f4988,plain,(
% 133.60/17.36 ![X0]: (~class_Orderings_Oorder(tc_set(X0))|~sQ8_spl)),
% 133.60/17.36 inference(component_clause,[status(thm)],[f4987])).
% 133.60/17.36 fof(f4994,plain,(
% 133.60/17.36 $false|~sQ8_spl),
% 133.60/17.36 inference(forward_subsumption_resolution,[status(thm)],[f4988,f1768])).
% 133.60/17.36 fof(f4995,plain,(
% 133.60/17.36 ~sQ8_spl),
% 133.60/17.36 inference(contradiction_clause,[status(thm)],[f4994])).
% 133.60/17.36 fof(f5550,plain,(
% 133.60/17.36 ![X0,X1,X2,X3,X4]: (c_in(X0,c_Relation_ORange(c_insert(c_Pair(X1,X0,X2,X3),X4,tc_prod(X2,X3)),X2,X3),X3))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1581,f2922])).
% 133.60/17.36 fof(f5708,plain,(
% 133.60/17.36 ![X0,X1,X2,X3,X4]: (c_in(c_Pair(c_Main_ORangeE__1(X0,c_insert(c_Pair(X1,X0,X2,X3),X4,tc_prod(X2,X3)),X3,X2),X0,X2,X3),c_insert(c_Pair(X1,X0,X2,X3),X4,tc_prod(X2,X3)),tc_prod(X2,X3)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f5550,f1579])).
% 133.60/17.36 fof(f6852,plain,(
% 133.60/17.36 ![X0,X1]: (c_in(X0,c_Inter(c_emptyset,X1),X1))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1602,f2919])).
% 133.60/17.36 fof(f7429,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2))|c_in(c_Main_OsubsetI__1(c_insert(X0,X1,X2),X3,X2),X1,X2)|c_Main_OsubsetI__1(c_insert(X0,X1,X2),X3,X2)=X0)),
% 133.60/17.36 inference(resolution,[status(thm)],[f1619,f2924])).
% 133.60/17.36 fof(f7436,plain,(
% 133.60/17.36 ![X0,X1]: (c_lessequals(X0,c_Inter(c_emptyset,X1),tc_set(X1)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1620,f6852])).
% 133.60/17.36 fof(f7455,plain,(
% 133.60/17.36 ![X0]: (c_lessequals(X0,c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1620,f4168])).
% 133.60/17.36 fof(f7488,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_lessequals(X0,c_insert(X1,c_UNIV,X2),tc_set(X2)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1620,f4646])).
% 133.60/17.36 fof(f7490,plain,(
% 133.60/17.36 ![X0,X1,X2,X3]: (c_lessequals(X0,c_insert(X1,X2,X3),tc_set(X3))|~c_in(c_Main_OsubsetI__1(X0,c_insert(X1,X2,X3),X3),X2,X3))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1620,f2921])).
% 133.60/17.36 fof(f7525,plain,(
% 133.60/17.36 ![X0,X1]: (~c_lessequals(c_Inter(c_emptyset,X0),X1,tc_set(X0))|X1=c_Inter(c_emptyset,X0))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7436,f1622])).
% 133.60/17.36 fof(f7529,plain,(
% 133.60/17.36 ![X0]: (~c_lessequals(c_Message_Oparts(c_UNIV),X0,tc_set(tc_Message_Omsg))|X0=c_Message_Oparts(c_UNIV))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7455,f1622])).
% 133.60/17.36 fof(f7594,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))|c_Main_OsubsetI__1(c_insert(X0,X1,X2),X1,X2)=X0|c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7429,f1620])).
% 133.60/17.36 fof(f7637,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))|c_Main_OsubsetI__1(c_insert(X0,X1,X2),X1,X2)=X0)),
% 133.60/17.36 inference(duplicate_literals_removal,[status(thm)],[f7594])).
% 133.60/17.36 fof(f7708,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2))|c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7490,f1619])).
% 133.60/17.36 fof(f7768,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)))),
% 133.60/17.36 inference(duplicate_literals_removal,[status(thm)],[f7708])).
% 133.60/17.36 fof(f7798,plain,(
% 133.60/17.36 ![X0,X1,X2]: (~c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))|X1=c_insert(X0,X1,X2))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7768,f1622])).
% 133.60/17.36 fof(f7804,definition,(
% 133.60/17.36 sQ10_spl <=> (c_less(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f7805,plain,(
% 133.60/17.36 c_less(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg))|~sQ10_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f7804])).
% 133.60/17.36 fof(f7818,plain,(
% 133.60/17.36 ~c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg))|~sQ10_spl),
% 133.60/17.36 inference(resolution,[status(thm)],[f7805,f1608])).
% 133.60/17.36 fof(f7819,plain,(
% 133.60/17.36 $false|~sQ10_spl),
% 133.60/17.36 inference(forward_subsumption_resolution,[status(thm)],[f7818,f1607])).
% 133.60/17.36 fof(f7820,plain,(
% 133.60/17.36 ~sQ10_spl),
% 133.60/17.36 inference(contradiction_clause,[status(thm)],[f7819])).
% 133.60/17.36 fof(f7834,definition,(
% 133.60/17.36 sQ12_spl <=> (c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f7836,plain,(
% 133.60/17.36 ~c_lessequals(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg))|sQ12_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f7834])).
% 133.60/17.36 fof(f8090,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_Relation_ORange(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1637,f1581])).
% 133.60/17.36 fof(f8094,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_in(X0,c_Relation_ODomain(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2))),
% 133.60/17.36 inference(resolution,[status(thm)],[f1637,f1573])).
% 133.60/17.36 fof(f8144,definition,(
% 133.60/17.36 sQ13_spl <=> (c_lessequals(c_Inter(c_emptyset,tc_Message_Omsg),c_Inter(c_emptyset,tc_Message_Omsg),tc_set(tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f8146,plain,(
% 133.60/17.36 ~c_lessequals(c_Inter(c_emptyset,tc_Message_Omsg),c_Inter(c_emptyset,tc_Message_Omsg),tc_set(tc_Message_Omsg))|sQ13_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f8144])).
% 133.60/17.36 fof(f8174,plain,(
% 133.60/17.36 c_Inter(c_emptyset,tc_Message_Omsg)=c_Message_Oparts(c_UNIV)),
% 133.60/17.36 inference(resolution,[status(thm)],[f7529,f7436])).
% 133.60/17.36 fof(f8186,definition,(
% 133.60/17.36 sQ17_spl <=> (class_Orderings_Oorder(tc_set(tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f8188,plain,(
% 133.60/17.36 ~class_Orderings_Oorder(tc_set(tc_Message_Omsg))|sQ17_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f8186])).
% 133.60/17.36 fof(f8725,plain,(
% 133.60/17.36 ![X0,X1]: (c_insert(X0,c_UNIV,X1)=c_Inter(c_emptyset,X1))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7525,f7488])).
% 133.60/17.36 fof(f9370,definition,(
% 133.60/17.36 sQ20_spl <=> (c_less(c_Message_Oparts(c_UNIV),c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f9371,plain,(
% 133.60/17.36 c_less(c_Message_Oparts(c_UNIV),c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg))|~sQ20_spl),
% 133.60/17.36 inference(component_clause,[status(thm)],[f9370])).
% 133.60/17.36 fof(f9379,plain,(
% 133.60/17.36 ~c_lessequals(c_Message_Oparts(c_UNIV),c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg))|~sQ20_spl),
% 133.60/17.36 inference(resolution,[status(thm)],[f9371,f1608])).
% 133.60/17.36 fof(f9380,plain,(
% 133.60/17.36 $false|~sQ20_spl),
% 133.60/17.36 inference(forward_subsumption_resolution,[status(thm)],[f9379,f7455])).
% 133.60/17.36 fof(f9381,plain,(
% 133.60/17.36 ~sQ20_spl),
% 133.60/17.36 inference(contradiction_clause,[status(thm)],[f9380])).
% 133.60/17.36 fof(f11464,plain,(
% 133.60/17.36 ![X0,X1,X2]: (c_Main_OsubsetI__1(c_insert(X0,X1,X2),X1,X2)=X0|X1=c_insert(X0,X1,X2))),
% 133.60/17.36 inference(resolution,[status(thm)],[f7637,f7798])).
% 133.60/17.36 fof(f11487,definition,(
% 133.60/17.36 ![X0]: (sQ24_spl <=> (~c_in(X0,c_UNIV,tc_Message_Omsg)))),
% 133.60/17.36 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 133.60/17.36 fof(f11488,plain,(
% 133.60/17.36 ![X0]: (~c_in(X0,c_UNIV,tc_Message_Omsg)|~sQ24_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f11487])).
% 133.60/17.38 fof(f11491,definition,(
% 133.60/17.38 ![X0]: (sQ25_spl <=> (~c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f11492,plain,(
% 133.60/17.38 ![X0]: (~c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg)|~sQ25_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f11491])).
% 133.60/17.38 fof(f11506,plain,(
% 133.60/17.38 ![X0,X1,X2]: (~c_in(X0,X1,X2)|c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))|X1=c_insert(X0,X1,X2))),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f11464,f1620])).
% 133.60/17.38 fof(f11511,plain,(
% 133.60/17.38 ![X0,X1,X2]: (~c_in(X0,X1,X2)|X1=c_insert(X0,X1,X2))),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f11506,f7798])).
% 133.60/17.38 fof(f11570,plain,(
% 133.60/17.38 ![X0]: (c_Finite__Set_OFinites=c_insert(c_SetInterval_OlessThan(X0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.38 inference(resolution,[status(thm)],[f11511,f1601])).
% 133.60/17.38 fof(f11571,plain,(
% 133.60/17.38 ![X0,X1]: (c_Finite__Set_OFinites=c_insert(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)))),
% 133.60/17.38 inference(resolution,[status(thm)],[f11511,f1600])).
% 133.60/17.38 fof(f11579,plain,(
% 133.60/17.38 ![X0,X1]: (c_Finite__Set_OFinites=c_insert(c_SetInterval_OatLeastAtMost(X0,X1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.38 inference(resolution,[status(thm)],[f11511,f1592])).
% 133.60/17.38 fof(f11689,plain,(
% 133.60/17.38 ![X0,X1]: (c_UNIV=c_insert(X0,c_UNIV,X1))),
% 133.60/17.38 inference(resolution,[status(thm)],[f11511,f1604])).
% 133.60/17.38 fof(f11723,plain,(
% 133.60/17.38 ![X0]: (c_UNIV=c_Inter(c_emptyset,X0))),
% 133.60/17.38 inference(backward_demodulation,[status(thm)],[f11689,f8725])).
% 133.60/17.38 fof(f11910,plain,(
% 133.60/17.38 c_UNIV=c_Message_Oparts(c_UNIV)),
% 133.60/17.38 inference(backward_demodulation,[status(thm)],[f11723,f8174])).
% 133.60/17.38 fof(f11915,plain,(
% 133.60/17.38 ![X0,X1]: (c_lessequals(X0,c_UNIV,tc_set(X1)))),
% 133.60/17.38 inference(backward_demodulation,[status(thm)],[f11723,f7436])).
% 133.60/17.38 fof(f11944,definition,(
% 133.60/17.38 sQ27_spl <=> (c_lessequals(c_UNIV,c_UNIV,tc_set(tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f11946,plain,(
% 133.60/17.38 ~c_lessequals(c_UNIV,c_UNIV,tc_set(tc_Message_Omsg))|sQ27_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f11944])).
% 133.60/17.38 fof(f13017,definition,(
% 133.60/17.38 sQ66_spl <=> (c_less(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_nat))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f13018,plain,(
% 133.60/17.38 c_less(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_nat)))|~sQ66_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f13017])).
% 133.60/17.38 fof(f13174,plain,(
% 133.60/17.38 ~c_lessequals(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_nat)))|~sQ66_spl),
% 133.60/17.38 inference(resolution,[status(thm)],[f13018,f1608])).
% 133.60/17.38 fof(f13175,plain,(
% 133.60/17.38 $false|~sQ66_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f13174,f1623])).
% 133.60/17.38 fof(f13176,plain,(
% 133.60/17.38 ~sQ66_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f13175])).
% 133.60/17.38 fof(f13307,definition,(
% 133.60/17.38 ![X0]: (sQ70_spl <=> (~c_in(c_SetInterval_OlessThan(X0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f13308,plain,(
% 133.60/17.38 ![X0]: (~c_in(c_SetInterval_OlessThan(X0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat))|~sQ70_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f13307])).
% 133.60/17.38 fof(f13462,definition,(
% 133.60/17.38 sQ75_spl <=> (c_less(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_IntDef_Oint))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f13463,plain,(
% 133.60/17.38 c_less(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_IntDef_Oint)))|~sQ75_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f13462])).
% 133.60/17.38 fof(f13556,plain,(
% 133.60/17.38 ~c_lessequals(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_set(tc_IntDef_Oint)))|~sQ75_spl),
% 133.60/17.38 inference(resolution,[status(thm)],[f13463,f1608])).
% 133.60/17.38 fof(f13557,plain,(
% 133.60/17.38 $false|~sQ75_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f13556,f1623])).
% 133.60/17.38 fof(f13558,plain,(
% 133.60/17.38 ~sQ75_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f13557])).
% 133.60/17.38 fof(f14556,definition,(
% 133.60/17.38 sQ95_spl <=> (c_emptyset=c_Finite__Set_OFinites)),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f14557,plain,(
% 133.60/17.38 c_emptyset=c_Finite__Set_OFinites|~sQ95_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f14556])).
% 133.60/17.38 fof(f14571,definition,(
% 133.60/17.38 sQ99_spl <=> (c_emptyset=c_Event_Oused(v_list))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f14572,plain,(
% 133.60/17.38 c_emptyset=c_Event_Oused(v_list)|~sQ99_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f14571])).
% 133.60/17.38 fof(f14828,plain,(
% 133.60/17.38 ![X0,X1]: (c_in(c_Message_Omsg_OKey(c_Public_OpublicKey(X0,X1)),c_emptyset,tc_Message_Omsg)|~sQ99_spl)),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f14572,f3089])).
% 133.60/17.38 fof(f14845,plain,(
% 133.60/17.38 $false|~sQ99_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f14828,f2919])).
% 133.60/17.38 fof(f14846,plain,(
% 133.60/17.38 ~sQ99_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f14845])).
% 133.60/17.38 fof(f14867,definition,(
% 133.60/17.38 sQ156_spl <=> (c_lessequals(c_emptyset,c_Event_Oused(v_list),tc_set(tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f14869,plain,(
% 133.60/17.38 ~c_lessequals(c_emptyset,c_Event_Oused(v_list),tc_set(tc_Message_Omsg))|sQ156_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f14867])).
% 133.60/17.38 fof(f15219,definition,(
% 133.60/17.38 sQ165_spl <=> (c_lessequals(c_Relation_OId,c_Relation_OId,tc_set(tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f15221,plain,(
% 133.60/17.38 ~c_lessequals(c_Relation_OId,c_Relation_OId,tc_set(tc_Message_Omsg))|sQ165_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f15219])).
% 133.60/17.38 fof(f15356,definition,(
% 133.60/17.38 sQ173_spl <=> (c_lessequals(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f15358,plain,(
% 133.60/17.38 ~c_lessequals(c_Finite__Set_OFinites,c_Finite__Set_OFinites,tc_set(tc_Message_Omsg))|sQ173_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f15356])).
% 133.60/17.38 fof(f16268,plain,(
% 133.60/17.38 ![X0]: (c_in(c_SetInterval_OlessThan(X0,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f11570,f2922])).
% 133.60/17.38 fof(f16338,plain,(
% 133.60/17.38 $false|sQ173_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f15358,f1623])).
% 133.60/17.38 fof(f16339,plain,(
% 133.60/17.38 sQ173_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16338])).
% 133.60/17.38 fof(f16340,plain,(
% 133.60/17.38 $false|sQ165_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f15221,f1623])).
% 133.60/17.38 fof(f16341,plain,(
% 133.60/17.38 sQ165_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16340])).
% 133.60/17.38 fof(f16342,plain,(
% 133.60/17.38 $false|sQ156_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f14869,f1607])).
% 133.60/17.38 fof(f16343,plain,(
% 133.60/17.38 sQ156_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16342])).
% 133.60/17.38 fof(f16353,plain,(
% 133.60/17.38 $false|~sQ70_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f13308,f16268])).
% 133.60/17.38 fof(f16354,plain,(
% 133.60/17.38 ~sQ70_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16353])).
% 133.60/17.38 fof(f16357,plain,(
% 133.60/17.38 $false|sQ27_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f11946,f11915])).
% 133.60/17.38 fof(f16358,plain,(
% 133.60/17.38 sQ27_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16357])).
% 133.60/17.38 fof(f16360,plain,(
% 133.60/17.38 ![X0]: (~c_in(X0,c_UNIV,tc_Message_Omsg)|~sQ25_spl)),
% 133.60/17.38 inference(forward_demodulation,[status(thm)],[f11910,f11492])).
% 133.60/17.38 fof(f16361,plain,(
% 133.60/17.38 $false|~sQ25_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16360,f1604])).
% 133.60/17.38 fof(f16362,plain,(
% 133.60/17.38 ~sQ25_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16361])).
% 133.60/17.38 fof(f16363,plain,(
% 133.60/17.38 $false|~sQ24_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f11488,f1604])).
% 133.60/17.38 fof(f16364,plain,(
% 133.60/17.38 ~sQ24_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16363])).
% 133.60/17.38 fof(f16368,plain,(
% 133.60/17.38 $false|sQ17_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f8188,f1768])).
% 133.60/17.38 fof(f16369,plain,(
% 133.60/17.38 sQ17_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16368])).
% 133.60/17.38 fof(f16374,plain,(
% 133.60/17.38 ~c_lessequals(c_UNIV,c_Inter(c_emptyset,tc_Message_Omsg),tc_set(tc_Message_Omsg))|sQ13_spl),
% 133.60/17.38 inference(forward_demodulation,[status(thm)],[f11723,f8146])).
% 133.60/17.38 fof(f16375,plain,(
% 133.60/17.38 ~c_lessequals(c_UNIV,c_UNIV,tc_set(tc_Message_Omsg))|sQ13_spl),
% 133.60/17.38 inference(forward_demodulation,[status(thm)],[f11723,f16374])).
% 133.60/17.38 fof(f16376,plain,(
% 133.60/17.38 $false|sQ13_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16375,f11915])).
% 133.60/17.38 fof(f16377,plain,(
% 133.60/17.38 sQ13_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16376])).
% 133.60/17.38 fof(f16378,plain,(
% 133.60/17.38 $false|sQ12_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f7836,f1607])).
% 133.60/17.38 fof(f16379,plain,(
% 133.60/17.38 sQ12_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16378])).
% 133.60/17.38 fof(f16394,definition,(
% 133.60/17.38 ![X0,X1]: (sQ184_spl <=> (c_in(X0,c_emptyset,X1)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16395,plain,(
% 133.60/17.38 ![X0,X1]: (c_in(X0,c_emptyset,X1)|~sQ184_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16394])).
% 133.60/17.38 fof(f16398,plain,(
% 133.60/17.38 $false|~sQ184_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16395,f2919])).
% 133.60/17.38 fof(f16399,plain,(
% 133.60/17.38 ~sQ184_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16398])).
% 133.60/17.38 fof(f16668,definition,(
% 133.60/17.38 sQ185_spl <=> (c_emptyset=c_insert(v_xc,c_emptyset,tc_Message_Omsg))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16669,plain,(
% 133.60/17.38 c_emptyset=c_insert(v_xc,c_emptyset,tc_Message_Omsg)|~sQ185_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16668])).
% 133.60/17.38 fof(f16696,plain,(
% 133.60/17.38 c_in(v_xc,c_emptyset,tc_Message_Omsg)|~sQ185_spl),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f16669,f2922])).
% 133.60/17.38 fof(f16721,plain,(
% 133.60/17.38 $false|~sQ185_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16696,f2919])).
% 133.60/17.38 fof(f16722,plain,(
% 133.60/17.38 ~sQ185_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16721])).
% 133.60/17.38 fof(f16775,definition,(
% 133.60/17.38 sQ189_spl <=> (c_emptyset=c_insert(c_Message_Omsg_ONonce(v_xd(v_x)),c_emptyset,tc_Message_Omsg))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16776,plain,(
% 133.60/17.38 c_emptyset=c_insert(c_Message_Omsg_ONonce(v_xd(v_x)),c_emptyset,tc_Message_Omsg)|~sQ189_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16775])).
% 133.60/17.38 fof(f16779,definition,(
% 133.60/17.38 sQ190_spl <=> (c_in(c_Message_Omsg_ONonce(v_xd(v_x)),c_emptyset,tc_Message_Omsg))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16780,plain,(
% 133.60/17.38 c_in(c_Message_Omsg_ONonce(v_xd(v_x)),c_emptyset,tc_Message_Omsg)|~sQ190_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16779])).
% 133.60/17.38 fof(f16798,definition,(
% 133.60/17.38 ![X0]: (sQ192_spl <=> (c_in(c_emptyset,c_emptyset,tc_set(X0))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16799,plain,(
% 133.60/17.38 ![X0]: (c_in(c_emptyset,c_emptyset,tc_set(X0))|~sQ192_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16798])).
% 133.60/17.38 fof(f16802,plain,(
% 133.60/17.38 $false|~sQ192_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16799,f2919])).
% 133.60/17.38 fof(f16803,plain,(
% 133.60/17.38 ~sQ192_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f16802])).
% 133.60/17.38 fof(f16825,definition,(
% 133.60/17.38 ![X0]: (sQ193_spl <=> (X0=c_emptyset))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f16826,plain,(
% 133.60/17.38 ![X0]: (X0=c_emptyset|~sQ193_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f16825])).
% 133.60/17.38 fof(f16842,plain,(
% 133.60/17.38 $false|~sQ193_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f2905,f16826])).
% 133.60/17.38 fof(f17063,plain,(
% 133.60/17.38 c_in(c_Message_Omsg_ONonce(v_xd(v_x)),c_emptyset,tc_Message_Omsg)|~sQ189_spl),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f16776,f2922])).
% 133.60/17.38 fof(f17072,definition,(
% 133.60/17.38 ![X0]: (sQ194_spl <=> (X0=c_Message_Omsg_ONonce(v_xd(v_x))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f17073,plain,(
% 133.60/17.38 ![X0]: (X0=c_Message_Omsg_ONonce(v_xd(v_x))|~sQ194_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f17072])).
% 133.60/17.38 fof(f17095,plain,(
% 133.60/17.38 $false|~sQ189_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f17063,f2919])).
% 133.60/17.38 fof(f17096,plain,(
% 133.60/17.38 ~sQ189_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f17095])).
% 133.60/17.38 fof(f17099,plain,(
% 133.60/17.38 $false|~sQ194_spl),
% 133.60/17.38 inference(resolution,[status(thm)],[f17073,f2990])).
% 133.60/17.38 fof(f17107,plain,(
% 133.60/17.38 ~sQ194_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f17099])).
% 133.60/17.38 fof(f17376,definition,(
% 133.60/17.38 ![X0,X1]: (sQ198_spl <=> (c_in(c_List_Oset(X0,X1),c_emptyset,tc_set(X1))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f17377,plain,(
% 133.60/17.38 ![X0,X1]: (c_in(c_List_Oset(X0,X1),c_emptyset,tc_set(X1))|~sQ198_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f17376])).
% 133.60/17.38 fof(f17381,plain,(
% 133.60/17.38 $false|~sQ198_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f17377,f2919])).
% 133.60/17.38 fof(f17382,plain,(
% 133.60/17.38 ~sQ198_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f17381])).
% 133.60/17.38 fof(f17522,definition,(
% 133.60/17.38 sQ200_spl <=> (c_lessequals(c_emptyset,c_insert(v_xc,c_emptyset,tc_Message_Omsg),tc_set(tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f17524,plain,(
% 133.60/17.38 ~c_lessequals(c_emptyset,c_insert(v_xc,c_emptyset,tc_Message_Omsg),tc_set(tc_Message_Omsg))|sQ200_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f17522])).
% 133.60/17.38 fof(f17614,plain,(
% 133.60/17.38 $false|sQ200_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f17524,f1607])).
% 133.60/17.38 fof(f17615,plain,(
% 133.60/17.38 sQ200_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f17614])).
% 133.60/17.38 fof(f17616,plain,(
% 133.60/17.38 $false|~sQ190_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f16780,f2919])).
% 133.60/17.38 fof(f17617,plain,(
% 133.60/17.38 ~sQ190_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f17616])).
% 133.60/17.38 fof(f17719,plain,(
% 133.60/17.38 ![X0,X1]: (c_in(c_SetInterval_OatLeastAtMost(X0,X1,tc_nat),c_Finite__Set_OFinites,tc_set(tc_nat)))),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f11579,f2922])).
% 133.60/17.38 fof(f18093,plain,(
% 133.60/17.38 ![X0,X1]: (c_in(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_IntDef_Oint),c_Finite__Set_OFinites,tc_set(tc_IntDef_Oint)))),
% 133.60/17.38 inference(paramodulation,[status(thm)],[f11571,f2922])).
% 133.60/17.38 fof(f18438,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Finite__Set_OFinites,X1)|~sQ95_spl)),
% 133.60/17.38 inference(backward_demodulation,[status(thm)],[f14557,f2919])).
% 133.60/17.38 fof(f18532,plain,(
% 133.60/17.38 $false|~sQ95_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f18093,f18438])).
% 133.60/17.38 fof(f18553,plain,(
% 133.60/17.38 ~sQ95_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f18532])).
% 133.60/17.38 fof(f19877,definition,(
% 133.60/17.38 sQ236_spl <=> (c_emptyset=c_insert(c_Message_Oagent_OSpy,c_emptyset,tc_Message_Oagent))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f19878,plain,(
% 133.60/17.38 c_emptyset=c_insert(c_Message_Oagent_OSpy,c_emptyset,tc_Message_Oagent)|~sQ236_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f19877])).
% 133.60/17.38 fof(f20022,definition,(
% 133.60/17.38 ![X0]: (sQ243_spl <=> (~X0=X0))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20023,plain,(
% 133.60/17.38 ![X0]: (~X0=X0|~sQ243_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20022])).
% 133.60/17.38 fof(f20026,plain,(
% 133.60/17.38 $false|~sQ243_spl),
% 133.60/17.38 inference(trivial_equality_resolution,[status(thm)],[f20023])).
% 133.60/17.38 fof(f20027,plain,(
% 133.60/17.38 ~sQ243_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20026])).
% 133.60/17.38 fof(f20402,definition,(
% 133.60/17.38 ![X0]: (sQ253_spl <=> (~c_in(X0,c_Event_Oused(v_list),tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20403,plain,(
% 133.60/17.38 ![X0]: (~c_in(X0,c_Event_Oused(v_list),tc_Message_Omsg)|~sQ253_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20402])).
% 133.60/17.38 fof(f20418,plain,(
% 133.60/17.38 $false|~sQ253_spl),
% 133.60/17.38 inference(resolution,[status(thm)],[f20403,f3089])).
% 133.60/17.38 fof(f20424,plain,(
% 133.60/17.38 ~sQ253_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20418])).
% 133.60/17.38 fof(f20435,definition,(
% 133.60/17.38 ![X0,X1]: (sQ256_spl <=> (~c_in(X0,c_UNIV,X1)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20436,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_UNIV,X1)|~sQ256_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20435])).
% 133.60/17.38 fof(f20440,plain,(
% 133.60/17.38 $false|~sQ256_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f20436,f1604])).
% 133.60/17.38 fof(f20441,plain,(
% 133.60/17.38 ~sQ256_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20440])).
% 133.60/17.38 fof(f20446,definition,(
% 133.60/17.38 ![X0]: (sQ257_spl <=> (~c_in(X0,c_Event_Obad,tc_Message_Oagent)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20447,plain,(
% 133.60/17.38 ![X0]: (~c_in(X0,c_Event_Obad,tc_Message_Oagent)|~sQ257_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20446])).
% 133.60/17.38 fof(f20452,plain,(
% 133.60/17.38 $false|~sQ257_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f2955,f20447])).
% 133.60/17.38 fof(f20458,plain,(
% 133.60/17.38 ~sQ257_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20452])).
% 133.60/17.38 fof(f20463,definition,(
% 133.60/17.38 ![X0]: (sQ258_spl <=> (~c_in(X0,c_Message_OsymKeys,tc_nat)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20464,plain,(
% 133.60/17.38 ![X0]: (~c_in(X0,c_Message_OsymKeys,tc_nat)|~sQ258_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20463])).
% 133.60/17.38 fof(f20469,plain,(
% 133.60/17.38 $false|~sQ258_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f3091,f20464])).
% 133.60/17.38 fof(f20475,plain,(
% 133.60/17.38 ~sQ258_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20469])).
% 133.60/17.38 fof(f20570,definition,(
% 133.60/17.38 ![X0]: (sQ264_spl <=> (~c_in(c_Public_OshrK(X0),c_Message_OsymKeys,tc_nat)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20571,plain,(
% 133.60/17.38 ![X0]: (~c_in(c_Public_OshrK(X0),c_Message_OsymKeys,tc_nat)|~sQ264_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20570])).
% 133.60/17.38 fof(f20580,plain,(
% 133.60/17.38 $false|~sQ264_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f20571,f3091])).
% 133.60/17.38 fof(f20581,plain,(
% 133.60/17.38 ~sQ264_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20580])).
% 133.60/17.38 fof(f20586,definition,(
% 133.60/17.38 ![X0,X1]: (sQ266_spl <=> (~c_in(X0,c_Event_Oused(X1),tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20587,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Event_Oused(X1),tc_Message_Omsg)|~sQ266_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20586])).
% 133.60/17.38 fof(f20593,plain,(
% 133.60/17.38 $false|~sQ266_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f3089,f20587])).
% 133.60/17.38 fof(f20599,plain,(
% 133.60/17.38 ~sQ266_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20593])).
% 133.60/17.38 fof(f20604,definition,(
% 133.60/17.38 ![X0,X1]: (sQ267_spl <=> (~c_in(X0,c_Finite__Set_OFinites,tc_set(X1))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20605,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Finite__Set_OFinites,tc_set(X1))|~sQ267_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20604])).
% 133.60/17.38 fof(f20611,plain,(
% 133.60/17.38 $false|~sQ267_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f17719,f20605])).
% 133.60/17.38 fof(f20638,plain,(
% 133.60/17.38 ~sQ267_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f20611])).
% 133.60/17.38 fof(f20649,definition,(
% 133.60/17.38 sQ269_spl <=> (class_Orderings_Oorder(tc_nat))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20651,plain,(
% 133.60/17.38 ~class_Orderings_Oorder(tc_nat)|sQ269_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20649])).
% 133.60/17.38 fof(f20817,definition,(
% 133.60/17.38 sQ271_spl <=> (c_less(c_0,c_0,tc_nat))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f20818,plain,(
% 133.60/17.38 c_less(c_0,c_0,tc_nat)|~sQ271_spl),
% 133.60/17.38 inference(component_clause,[status(thm)],[f20817])).
% 133.60/17.38 fof(f21115,definition,(
% 133.60/17.38 ![X0,X1]: (sQ277_spl <=> (~c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f21116,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Message_Osynth(X1),tc_Message_Omsg)|~sQ277_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f21115])).
% 133.60/17.38 fof(f21121,plain,(
% 133.60/17.38 $false|~sQ277_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f3056,f21116])).
% 133.60/17.38 fof(f21127,plain,(
% 133.60/17.38 ~sQ277_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f21121])).
% 133.60/17.38 fof(f21178,plain,(
% 133.60/17.38 $false|sQ269_spl),
% 133.60/17.38 inference(forward_subsumption_resolution,[status(thm)],[f20651,f1739])).
% 133.60/17.38 fof(f21179,plain,(
% 133.60/17.38 sQ269_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f21178])).
% 133.60/17.38 fof(f21223,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(c_Message_Omsg_ONonce(X0),c_Event_OinitState(X1),tc_Message_Omsg))),
% 133.60/17.38 inference(resolution,[status(thm)],[f3069,f3048])).
% 133.60/17.38 fof(f21302,definition,(
% 133.60/17.38 ![X0,X1]: (sQ283_spl <=> (~c_in(X0,c_Event_OinitState(X1),tc_Message_Omsg)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f21303,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Event_OinitState(X1),tc_Message_Omsg)|~sQ283_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f21302])).
% 133.60/17.38 fof(f21308,plain,(
% 133.60/17.38 $false|~sQ283_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f3092,f21303])).
% 133.60/17.38 fof(f21313,plain,(
% 133.60/17.38 ~sQ283_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f21308])).
% 133.60/17.38 fof(f21347,definition,(
% 133.60/17.38 ![X0,X1,X2,X3]: (sQ285_spl <=> (~c_in(X0,c_insert(X1,X2,X3),X3)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f21348,plain,(
% 133.60/17.38 ![X0,X1,X2,X3]: (~c_in(X0,c_insert(X1,X2,X3),X3)|~sQ285_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f21347])).
% 133.60/17.38 fof(f21354,plain,(
% 133.60/17.38 $false|~sQ285_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f5708,f21348])).
% 133.60/17.38 fof(f21396,plain,(
% 133.60/17.38 ~sQ285_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f21354])).
% 133.60/17.38 fof(f21506,definition,(
% 133.60/17.38 ![X0]: (sQ286_spl <=> (~class_Orderings_Olinorder(X0)))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f21507,plain,(
% 133.60/17.38 ![X0]: (~class_Orderings_Olinorder(X0)|~sQ286_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f21506])).
% 133.60/17.38 fof(f21520,plain,(
% 133.60/17.38 $false|~sQ286_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f1761,f21507])).
% 133.60/17.38 fof(f21523,plain,(
% 133.60/17.38 ~sQ286_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f21520])).
% 133.60/17.38 fof(f22180,definition,(
% 133.60/17.38 ![X0,X1]: (sQ296_spl <=> (~c_in(X0,c_Relation_OId,tc_prod(X1,X1))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f22181,plain,(
% 133.60/17.38 ![X0,X1]: (~c_in(X0,c_Relation_OId,tc_prod(X1,X1))|~sQ296_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f22180])).
% 133.60/17.38 fof(f22186,plain,(
% 133.60/17.38 $false|~sQ296_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f2854,f22181])).
% 133.60/17.38 fof(f22194,plain,(
% 133.60/17.38 ~sQ296_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f22186])).
% 133.60/17.38 fof(f22207,definition,(
% 133.60/17.38 ![X0,X1,X2]: (sQ298_spl <=> (~c_in(X0,c_List_Olists(X1,X2),tc_List_Olist(X2))))),
% 133.60/17.38 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 133.60/17.38 fof(f22208,plain,(
% 133.60/17.38 ![X0,X1,X2]: (~c_in(X0,c_List_Olists(X1,X2),tc_List_Olist(X2))|~sQ298_spl)),
% 133.60/17.38 inference(component_clause,[status(thm)],[f22207])).
% 133.60/17.38 fof(f22249,plain,(
% 133.60/17.38 $false|~sQ298_spl),
% 133.60/17.38 inference(backward_subsumption_resolution,[status(thm)],[f1562,f22208])).
% 133.60/17.38 fof(f22260,plain,(
% 133.60/17.38 ~sQ298_spl),
% 133.60/17.38 inference(contradiction_clause,[status(thm)],[f22249])).
% 133.60/17.38 fof(f22305,plain,(
% 133.60/17.38 ![X0,X1]: (~class_Orderings_Oord(X0)|c_in(X1,c_SetInterval_OatLeast(X1,X0),X0)|~class_Orderings_Oorder(X0))),
% 133.60/17.40 inference(resolution,[status(thm)],[f2864,f1570])).
% 133.60/17.40 fof(f22306,definition,(
% 133.60/17.40 sQ299_spl <=> (class_Orderings_Oord(tc_nat))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f22308,plain,(
% 133.60/17.40 ~class_Orderings_Oord(tc_nat)|sQ299_spl),
% 133.60/17.40 inference(component_clause,[status(thm)],[f22306])).
% 133.60/17.40 fof(f22324,definition,(
% 133.60/17.40 sQ303_spl <=> (class_Orderings_Oord(tc_IntDef_Oint))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f22326,plain,(
% 133.60/17.40 ~class_Orderings_Oord(tc_IntDef_Oint)|sQ303_spl),
% 133.60/17.40 inference(component_clause,[status(thm)],[f22324])).
% 133.60/17.40 fof(f22333,definition,(
% 133.60/17.40 sQ305_spl <=> (class_Orderings_Oord(tc_set(tc_Message_Omsg)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f22335,plain,(
% 133.60/17.40 ~class_Orderings_Oord(tc_set(tc_Message_Omsg))|sQ305_spl),
% 133.60/17.40 inference(component_clause,[status(thm)],[f22333])).
% 133.60/17.40 fof(f22352,plain,(
% 133.60/17.40 ![X0,X1]: (c_in(X0,c_SetInterval_OatLeast(X0,X1),X1)|~class_Orderings_Oorder(X1))),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22305,f1974])).
% 133.60/17.40 fof(f22353,plain,(
% 133.60/17.40 $false|sQ299_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22308,f1728])).
% 133.60/17.40 fof(f22354,plain,(
% 133.60/17.40 sQ299_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f22353])).
% 133.60/17.40 fof(f22355,plain,(
% 133.60/17.40 $false|sQ305_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22335,f1767])).
% 133.60/17.40 fof(f22356,plain,(
% 133.60/17.40 sQ305_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f22355])).
% 133.60/17.40 fof(f22357,plain,(
% 133.60/17.40 $false|sQ303_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22326,f1691])).
% 133.60/17.40 fof(f22358,plain,(
% 133.60/17.40 sQ303_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f22357])).
% 133.60/17.40 fof(f22532,plain,(
% 133.60/17.40 ![X0]: (c_in(X0,c_SetInterval_OatLeast(X0,tc_IntDef_Oint),tc_IntDef_Oint))),
% 133.60/17.40 inference(resolution,[status(thm)],[f22352,f1671])).
% 133.60/17.40 fof(f22687,plain,(
% 133.60/17.40 ![X0,X1]: (~class_Orderings_Oord(tc_set(X0))|c_in(c_emptyset,c_SetInterval_OatMost(X1,tc_set(X0)),tc_set(X0)))),
% 133.60/17.40 inference(resolution,[status(thm)],[f2870,f1607])).
% 133.60/17.40 fof(f22709,plain,(
% 133.60/17.40 ![X0,X1]: (c_in(c_emptyset,c_SetInterval_OatMost(X0,tc_set(X1)),tc_set(X1)))),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22687,f1767])).
% 133.60/17.40 fof(f22831,definition,(
% 133.60/17.40 sQ328_spl <=> (class_Orderings_Oorder(tc_IntDef_Oint))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f22833,plain,(
% 133.60/17.40 ~class_Orderings_Oorder(tc_IntDef_Oint)|sQ328_spl),
% 133.60/17.40 inference(component_clause,[status(thm)],[f22831])).
% 133.60/17.40 fof(f22843,plain,(
% 133.60/17.40 $false|sQ328_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f22833,f1671])).
% 133.60/17.40 fof(f22844,plain,(
% 133.60/17.40 sQ328_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f22843])).
% 133.60/17.40 fof(f23177,definition,(
% 133.60/17.40 ![X0,X1]: (sQ369_spl <=> (~c_in(X0,c_SetInterval_OatLeast(X1,tc_IntDef_Oint),tc_IntDef_Oint)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f23178,plain,(
% 133.60/17.40 ![X0,X1]: (~c_in(X0,c_SetInterval_OatLeast(X1,tc_IntDef_Oint),tc_IntDef_Oint)|~sQ369_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f23177])).
% 133.60/17.40 fof(f23183,plain,(
% 133.60/17.40 $false|~sQ369_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f22532,f23178])).
% 133.60/17.40 fof(f23189,plain,(
% 133.60/17.40 ~sQ369_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f23183])).
% 133.60/17.40 fof(f23455,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ384_spl <=> (~c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f23456,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))|~sQ384_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f23455])).
% 133.60/17.40 fof(f23462,plain,(
% 133.60/17.40 $false|~sQ384_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f1637,f23456])).
% 133.60/17.40 fof(f23471,plain,(
% 133.60/17.40 ~sQ384_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f23462])).
% 133.60/17.40 fof(f23485,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ386_spl <=> (~c_in(X0,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(X1,X2),X2),X2)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ386_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f23486,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(X1,X2),X2),X2)|~sQ386_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f23485])).
% 133.60/17.40 fof(f23491,plain,(
% 133.60/17.40 $false|~sQ386_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2681,f23486])).
% 133.60/17.40 fof(f23503,plain,(
% 133.60/17.40 ~sQ386_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f23491])).
% 133.60/17.40 fof(f24824,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ426_spl <=> (~c_in(X0,c_Event_Oknows(X1,X2),tc_Message_Omsg)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f24825,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Event_Oknows(X1,X2),tc_Message_Omsg)|~sQ426_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f24824])).
% 133.60/17.40 fof(f24830,plain,(
% 133.60/17.40 $false|~sQ426_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f3093,f24825])).
% 133.60/17.40 fof(f24837,plain,(
% 133.60/17.40 ~sQ426_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f24830])).
% 133.60/17.40 fof(f24856,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ429_spl <=> (~c_in(X0,c_Datatype_Oo2s(X1,X2),X2)|X1=c_Datatype_Ooption_ONone))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f24857,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Datatype_Oo2s(X1,X2),X2)|X1=c_Datatype_Ooption_ONone|~sQ429_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f24856])).
% 133.60/17.40 fof(f24872,plain,(
% 133.60/17.40 ![X0,X1]: (c_Datatype_Ooption_OSome(X0,X1)=c_Datatype_Ooption_ONone|~sQ429_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f24857,f2681])).
% 133.60/17.40 fof(f24873,definition,(
% 133.60/17.40 ![X0]: (sQ430_spl <=> (X0=c_Datatype_Ooption_ONone))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f24874,plain,(
% 133.60/17.40 ![X0]: (X0=c_Datatype_Ooption_ONone|~sQ430_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f24873])).
% 133.60/17.40 fof(f24884,plain,(
% 133.60/17.40 $false|~sQ429_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f24872,f2686])).
% 133.60/17.40 fof(f24885,plain,(
% 133.60/17.40 ~sQ429_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f24884])).
% 133.60/17.40 fof(f24886,plain,(
% 133.60/17.40 $false|~sQ430_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2686,f24874])).
% 133.60/17.40 fof(f24890,plain,(
% 133.60/17.40 ~sQ430_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f24886])).
% 133.60/17.40 fof(f25080,definition,(
% 133.60/17.40 sQ439_spl <=> (class_Orderings_Oord(tc_set(tc_nat)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f25082,plain,(
% 133.60/17.40 ~class_Orderings_Oord(tc_set(tc_nat))|sQ439_spl),
% 133.60/17.40 inference(component_clause,[status(thm)],[f25080])).
% 133.60/17.40 fof(f25091,plain,(
% 133.60/17.40 $false|sQ439_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f25082,f1767])).
% 133.60/17.40 fof(f25092,plain,(
% 133.60/17.40 sQ439_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f25091])).
% 133.60/17.40 fof(f25249,definition,(
% 133.60/17.40 ![X2]: (sQ457_spl <=> (X2=c_UNIV))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f25250,plain,(
% 133.60/17.40 ![X0]: (X0=c_UNIV|~sQ457_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f25249])).
% 133.60/17.40 fof(f25380,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ461_spl <=> (~c_in(X0,c_Relation_ORange(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f25381,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Relation_ORange(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2)|~sQ461_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f25380])).
% 133.60/17.40 fof(f25385,plain,(
% 133.60/17.40 $false|~sQ461_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f25381,f8090])).
% 133.60/17.40 fof(f25386,plain,(
% 133.60/17.40 ~sQ461_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f25385])).
% 133.60/17.40 fof(f25431,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ463_spl <=> (~c_in(X0,c_Relation_ODomain(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f25432,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_Relation_ODomain(c_Transitive__Closure_Ortrancl(X1,X2),X2,X2),X2)|~sQ463_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f25431])).
% 133.60/17.40 fof(f25436,plain,(
% 133.60/17.40 $false|~sQ463_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f25432,f8094])).
% 133.60/17.40 fof(f25437,plain,(
% 133.60/17.40 ~sQ463_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f25436])).
% 133.60/17.40 fof(f25922,definition,(
% 133.60/17.40 ![X0]: (sQ469_spl <=> (X0=c_0))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f25923,plain,(
% 133.60/17.40 ![X0]: (X0=c_0|~sQ469_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f25922])).
% 133.60/17.40 fof(f25930,plain,(
% 133.60/17.40 $false|~sQ469_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2822,f25923])).
% 133.60/17.40 fof(f25954,plain,(
% 133.60/17.40 ~sQ469_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f25930])).
% 133.60/17.40 fof(f26347,definition,(
% 133.60/17.40 ![X0,X1,X2]: (sQ485_spl <=> (~c_in(X0,c_SetInterval_OatMost(X1,tc_set(X2)),tc_set(X2))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ485_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f26348,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_in(X0,c_SetInterval_OatMost(X1,tc_set(X2)),tc_set(X2))|~sQ485_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f26347])).
% 133.60/17.40 fof(f26353,plain,(
% 133.60/17.40 $false|~sQ485_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f22709,f26348])).
% 133.60/17.40 fof(f26367,plain,(
% 133.60/17.40 ~sQ485_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f26353])).
% 133.60/17.40 fof(f26533,plain,(
% 133.60/17.40 ~sQ193_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f16842])).
% 133.60/17.40 fof(f26742,plain,(
% 133.60/17.40 $false|~sQ457_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2905,f25250])).
% 133.60/17.40 fof(f26769,plain,(
% 133.60/17.40 ~sQ457_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f26742])).
% 133.60/17.40 fof(f27214,plain,(
% 133.60/17.40 ![X0,X1]: (c_lessequals(X0,v_xd(c_plus(X1,X0,tc_nat)),tc_nat)|~sQ2_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f3062,f3124])).
% 133.60/17.40 fof(f27223,plain,(
% 133.60/17.40 ![X0,X1]: (~c_in(c_Message_Omsg_ONonce(v_xd(c_plus(X0,v_sko__upX(X1),tc_nat))),c_Message_Oparts(c_insert(X1,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)|~sQ2_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f27214,f3060])).
% 133.60/17.40 fof(f27613,plain,(
% 133.60/17.40 ![X0,X1]: (c_lessequals(X0,v_xd(c_plus(X0,X1,tc_nat)),tc_nat)|~sQ2_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f3064,f3124])).
% 133.60/17.40 fof(f27628,plain,(
% 133.60/17.40 ![X0,X1,X2]: (c_lessequals(X0,v_xd(c_plus(c_plus(X1,X0,tc_nat),X2,tc_nat)),tc_nat)|~sQ2_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f27613,f3062])).
% 133.60/17.40 fof(f28331,plain,(
% 133.60/17.40 ![X0]: (c_in(c_Message_Omsg_ONonce(v_xd(c_plus(X0,v_sko__upX(v_xc),tc_nat))),c_Event_Oused(v_list),tc_Message_Omsg)|~sQ2_spl|~sQ3_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f27223,f3130])).
% 133.60/17.40 fof(f29487,plain,(
% 133.60/17.40 $false|~sQ271_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f20818,f2845])).
% 133.60/17.40 fof(f29488,plain,(
% 133.60/17.40 ~sQ271_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f29487])).
% 133.60/17.40 fof(f30259,plain,(
% 133.60/17.40 c_in(c_Message_Oagent_OSpy,c_emptyset,tc_Message_Oagent)|~sQ236_spl),
% 133.60/17.40 inference(paramodulation,[status(thm)],[f19878,f2922])).
% 133.60/17.40 fof(f30276,definition,(
% 133.60/17.40 ![X0]: (sQ639_spl <=> (X0=c_Message_Oagent_OSpy))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30277,plain,(
% 133.60/17.40 ![X0]: (X0=c_Message_Oagent_OSpy|~sQ639_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30276])).
% 133.60/17.40 fof(f30295,plain,(
% 133.60/17.40 $false|~sQ236_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f30259,f2919])).
% 133.60/17.40 fof(f30296,plain,(
% 133.60/17.40 ~sQ236_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30295])).
% 133.60/17.40 fof(f30394,plain,(
% 133.60/17.40 $false|~sQ639_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f3028,f30277])).
% 133.60/17.40 fof(f30407,plain,(
% 133.60/17.40 ~sQ639_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30394])).
% 133.60/17.40 fof(f30451,definition,(
% 133.60/17.40 ![X0]: (sQ653_spl <=> (c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_emptyset,tc_Message_Omsg)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ653_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30452,plain,(
% 133.60/17.40 ![X0]: (c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_emptyset,tc_Message_Omsg)|~sQ653_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30451])).
% 133.60/17.40 fof(f30464,plain,(
% 133.60/17.40 $false|~sQ653_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f30452,f2919])).
% 133.60/17.40 fof(f30465,plain,(
% 133.60/17.40 ~sQ653_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30464])).
% 133.60/17.40 fof(f30613,definition,(
% 133.60/17.40 ![X1]: (sQ657_spl <=> (c_Message_Omsg_ONonce(v_xd(v_xd(v_x)))=c_Message_Omsg_OKey(c_Public_OshrK(X1))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30614,plain,(
% 133.60/17.40 ![X0]: (c_Message_Omsg_ONonce(v_xd(v_xd(v_x)))=c_Message_Omsg_OKey(c_Public_OshrK(X0))|~sQ657_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30613])).
% 133.60/17.40 fof(f30621,definition,(
% 133.60/17.40 ![X1,X2]: (sQ659_spl <=> (c_Message_Omsg_ONumber(X1)=c_Message_Omsg_OKey(c_Public_OshrK(X2))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30622,plain,(
% 133.60/17.40 ![X0,X1]: (c_Message_Omsg_ONumber(X0)=c_Message_Omsg_OKey(c_Public_OshrK(X1))|~sQ659_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30621])).
% 133.60/17.40 fof(f30625,definition,(
% 133.60/17.40 ![X1,X2]: (sQ660_spl <=> (c_Message_Omsg_OAgent(X1)=c_Message_Omsg_OKey(c_Public_OshrK(X2))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ660_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30626,plain,(
% 133.60/17.40 ![X0,X1]: (c_Message_Omsg_OAgent(X0)=c_Message_Omsg_OKey(c_Public_OshrK(X1))|~sQ660_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30625])).
% 133.60/17.40 fof(f30642,definition,(
% 133.60/17.40 ![X1,X2,X3]: (sQ664_spl <=> (c_Message_Omsg_OKey(c_Public_OpublicKey(X1,X2))=c_Message_Omsg_OKey(c_Public_OshrK(X3))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30643,plain,(
% 133.60/17.40 ![X0,X1,X2]: (c_Message_Omsg_OKey(c_Public_OpublicKey(X0,X1))=c_Message_Omsg_OKey(c_Public_OshrK(X2))|~sQ664_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30642])).
% 133.60/17.40 fof(f30659,definition,(
% 133.60/17.40 ![X0,X1]: (sQ668_spl <=> (X0=c_Message_Omsg_OKey(c_Public_OshrK(X1))))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f30660,plain,(
% 133.60/17.40 ![X0,X1]: (X0=c_Message_Omsg_OKey(c_Public_OshrK(X1))|~sQ668_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f30659])).
% 133.60/17.40 fof(f30694,plain,(
% 133.60/17.40 $false|~sQ668_spl),
% 133.60/17.40 inference(resolution,[status(thm)],[f30660,f2992])).
% 133.60/17.40 fof(f30707,plain,(
% 133.60/17.40 ~sQ668_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30694])).
% 133.60/17.40 fof(f30727,plain,(
% 133.60/17.40 ![X0,X1,X2]: (~c_Message_Omsg_OAgent(X0)=c_Message_Omsg_OKey(c_Public_OshrK(X1))|X0=X2|~sQ660_spl)),
% 133.60/17.40 inference(paramodulation,[status(thm)],[f30626,f3035])).
% 133.60/17.40 fof(f30734,plain,(
% 133.60/17.40 ![X0,X1]: (X0=X1|~sQ660_spl)),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f30727,f30626])).
% 133.60/17.40 fof(f30741,plain,(
% 133.60/17.40 $false|~sQ660_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2905,f30734])).
% 133.60/17.40 fof(f30784,plain,(
% 133.60/17.40 ~sQ660_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30741])).
% 133.60/17.40 fof(f30897,plain,(
% 133.60/17.40 ![X0,X1]: (c_Message_Omsg_ONumber(X0)=c_Message_Omsg_ONumber(X1)|~sQ659_spl)),
% 133.60/17.40 inference(paramodulation,[status(thm)],[f30622,f30622])).
% 133.60/17.40 fof(f30993,plain,(
% 133.60/17.40 $false|~sQ659_spl),
% 133.60/17.40 inference(backward_subsumption_resolution,[status(thm)],[f2790,f31018])).
% 133.60/17.40 fof(f31018,plain,(
% 133.60/17.40 ![X0,X1]: (X0=X1|~sQ659_spl)),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f3036,f30897])).
% 133.60/17.40 fof(f31019,plain,(
% 133.60/17.40 ~sQ659_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f30993])).
% 133.60/17.40 fof(f31453,definition,(
% 133.60/17.40 ![X0]: (sQ676_spl <=> (~c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_Oused(v_list),tc_Message_Omsg)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f31454,plain,(
% 133.60/17.40 ![X0]: (~c_in(c_Message_Omsg_OKey(c_Public_OshrK(X0)),c_Event_Oused(v_list),tc_Message_Omsg)|~sQ676_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f31453])).
% 133.60/17.40 fof(f31525,plain,(
% 133.60/17.40 ![X0]: (c_in(c_Message_Omsg_ONonce(v_xd(v_xd(v_x))),c_Event_OinitState(X0),tc_Message_Omsg)|~sQ657_spl)),
% 133.60/17.40 inference(paramodulation,[status(thm)],[f30614,f3092])).
% 133.60/17.40 fof(f31538,plain,(
% 133.60/17.40 $false|~sQ657_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f31525,f21223])).
% 133.60/17.40 fof(f31539,plain,(
% 133.60/17.40 ~sQ657_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f31538])).
% 133.60/17.40 fof(f31542,plain,(
% 133.60/17.40 $false|~sQ676_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f31454,f3094])).
% 133.60/17.40 fof(f31543,plain,(
% 133.60/17.40 ~sQ676_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f31542])).
% 133.60/17.40 fof(f31638,definition,(
% 133.60/17.40 ![X0]: (sQ684_spl <=> (~c_in(X0,c_UNIV,tc_nat)))),
% 133.60/17.40 introduced(definition,[new_symbols(definition,[sQ684_spl])],[split_symbol_definition])).
% 133.60/17.40 fof(f31639,plain,(
% 133.60/17.40 ![X0]: (~c_in(X0,c_UNIV,tc_nat)|~sQ684_spl)),
% 133.60/17.40 inference(component_clause,[status(thm)],[f31638])).
% 133.60/17.40 fof(f31643,plain,(
% 133.60/17.40 $false|~sQ684_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f31639,f1604])).
% 133.60/17.40 fof(f31644,plain,(
% 133.60/17.40 ~sQ684_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f31643])).
% 133.60/17.40 fof(f31738,plain,(
% 133.60/17.40 ![X0,X1,X2]: (c_Public_OpublicKey(X0,X1)=c_Public_OshrK(X2)|~sQ664_spl)),
% 133.60/17.40 inference(resolution,[status(thm)],[f30643,f3038])).
% 133.60/17.40 fof(f31758,plain,(
% 133.60/17.40 $false|~sQ664_spl),
% 133.60/17.40 inference(forward_subsumption_resolution,[status(thm)],[f31738,f3083])).
% 133.60/17.40 fof(f31759,plain,(
% 133.60/17.40 ~sQ664_spl),
% 133.60/17.40 inference(contradiction_clause,[status(thm)],[f31758])).
% 133.60/17.40 fof(f32820,definition,(
% 133.60/17.40 ![X0,X1]: (sQ704_spl <=> (~c_in(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)))),
% 133.60/17.49 introduced(definition,[new_symbols(definition,[sQ704_spl])],[split_symbol_definition])).
% 133.60/17.49 fof(f32821,plain,(
% 133.60/17.49 ![X0,X1]: (~c_in(X0,c_Event_Oknows(c_Message_Oagent_OSpy,X1),tc_Message_Omsg)|~sQ704_spl)),
% 133.60/17.49 inference(component_clause,[status(thm)],[f32820])).
% 133.60/17.49 fof(f32840,plain,(
% 133.60/17.49 $false|~sQ704_spl),
% 133.60/17.49 inference(resolution,[status(thm)],[f32821,f3093])).
% 133.60/17.49 fof(f32846,plain,(
% 133.60/17.49 ~sQ704_spl),
% 133.60/17.49 inference(contradiction_clause,[status(thm)],[f32840])).
% 133.60/17.49 fof(f33454,plain,(
% 133.60/17.49 ![X0]: (~c_lessequals(v_x,v_xd(c_plus(X0,v_sko__upX(v_xc),tc_nat)),tc_nat)|~sQ2_spl|~sQ3_spl)),
% 133.60/17.49 inference(resolution,[status(thm)],[f28331,f3099])).
% 133.60/17.49 fof(f34331,plain,(
% 133.60/17.49 $false|~sQ3_spl|~sQ2_spl),
% 133.60/17.49 inference(resolution,[status(thm)],[f33454,f27628])).
% 133.60/17.49 fof(f34339,plain,(
% 133.60/17.49 ~sQ3_spl|~sQ2_spl),
% 133.60/17.49 inference(contradiction_clause,[status(thm)],[f34331])).
% 133.60/17.49 fof(f34340,plain,(
% 133.60/17.49 $false),
% 133.60/17.49 inference(sat_refutation,[status(thm)],[f3128,f3136,f3166,f4995,f7820,f9381,f13176,f13558,f14846,f16339,f16341,f16343,f16354,f16358,f16362,f16364,f16369,f16377,f16379,f16399,f16722,f16803,f17096,f17107,f17382,f17615,f17617,f18553,f20027,f20424,f20441,f20458,f20475,f20581,f20599,f20638,f21127,f21179,f21313,f21396,f21523,f22194,f22260,f22354,f22356,f22358,f22844,f23189,f23471,f23503,f24837,f24885,f24890,f25092,f25386,f25437,f25954,f26367,f26533,f26769,f29488,f30296,f30407,f30465,f30707,f30784,f31019,f31539,f31543,f31644,f31759,f32846,f34339])).
% 133.60/17.49 % SZS output end CNFRefutation for theBenchmark.p
% 4.34/17.57 % Elapsed time: 17.198143 seconds
% 4.34/17.57 % CPU time: 134.946514 seconds
% 4.34/17.57 % Total memory used: 1.515 GB
% 4.34/17.57 % Net memory used: 1.467 GB
%------------------------------------------------------------------------------