%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV283-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:47:10 PM UTC 2026
% Result : Unsatisfiable 49.00s 6.72s
% Output : CNFRefutation 49.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 49
% Syntax : Number of formulae : 199 ( 67 unt; 15 def)
% Number of atoms : 363 ( 68 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 318 ( 154 ~; 149 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 16 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 11 con; 0-3 aty)
% Number of variables : 350 ( 350 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f48,axiom,
! [V_A,V_xs,T_a] :
( c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| ~ c_in(c_Main_Oin__listsI__1(V_A,V_xs,T_a),V_A,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [V_x,V_l,T_a,V_A] :
( c_in(V_x,V_A,T_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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [V_A,V_C,T_a] :
( c_in(c_Main_OInterI__1(V_A,V_C,T_a),V_C,tc_set(T_a))
| c_in(V_A,c_Inter(V_C,T_a),T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [V_x,T_a] : c_in(V_x,c_UNIV,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [V_A,T_a] : c_lessequals(c_emptyset,V_A,tc_set(T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [V_A,V_B,T_a] :
( V_A = V_B
| c_less(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,axiom,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f221,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,axiom,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1215,axiom,
! [T_a] : c_List_Olist_ONil = c_List_Orev(c_List_Olist_ONil,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1227,axiom,
! [V_ys,T_a] : c_append(c_List_Olist_ONil,V_ys,T_a) = V_ys,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1228,axiom,
! [V_xs,V_ys,T_a] :
( V_ys = c_List_Olist_ONil
| c_append(V_xs,V_ys,T_a) != V_xs ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1238,axiom,
! [V_a_H,V_list_H,T_a] : c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1242,axiom,
! [V_xs,T_a,V_y,V_ys] :
( V_xs = c_append(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a)
| c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1243,axiom,
! [V_ys,T_a,V_y] : c_List_Orev(c_append(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a),T_a) = c_List_Olist_OCons(V_y,V_ys,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1279,axiom,
! [V_n] : ~ c_less(V_n,c_0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1333,axiom,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1334,axiom,
! [V_a,V_B,T_a,V_b] :
( c_in(V_a,c_insert(V_b,V_B,T_a),T_a)
| ~ c_in(V_a,V_B,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1336,axiom,
! [V_a,V_b,V_A,T_a] :
( V_a = V_b
| c_in(V_a,V_A,T_a)
| ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1382,axiom,
! [V_N,V_X,V_Y] : c_Message_Omsg_ONonce(V_N) != c_Message_OHPair(V_X,V_Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1401,axiom,
! [V_X,V_Y,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1412,axiom,
! [V_nat] : c_Message_Oagent_OFriend(V_nat) != c_Message_Oagent_OSpy,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1427,axiom,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(V_X,V_H,tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1429,axiom,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ~ c_in(V_X,c_Message_Oparts(c_Message_Oparts(V_H)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1438,axiom,
! [V_U,V_msg] :
( ~ c_lessequals(v_sko__upX(V_msg),V_U,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(V_U),c_Message_Oparts(c_insert(V_msg,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1439,axiom,
! [V_m,V_k,V_n] :
( c_lessequals(V_k,V_n,tc_nat)
| ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1440,axiom,
! [V_m,V_k,V_n] :
( c_lessequals(V_m,V_n,tc_nat)
| ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1469,negated_conjecture,
! [V_U] :
( ~ c_lessequals(v_x,V_U,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(v_list),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1473,negated_conjecture,
! [V_W,V_U] :
( c_lessequals(V_U,v_xd(V_U),tc_nat)
| c_lessequals(V_W,v_xd(V_W),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1478,negated_conjecture,
! [V_X,V_U] :
( 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)
| 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_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_X)),c_Event_Oused(v_list),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1545,plain,
! [X0,X1,X2] :
( c_in(X1,c_List_Olists(X0,X2),tc_List_Olist(X2))
| ~ c_in(c_Main_Oin__listsI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f1559,plain,
! [V_x,T_a,V_A] :
( c_in(V_x,V_A,T_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)) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f1560,plain,
! [X0,X1,X2,X3] :
( c_in(X0,X3,X2)
| ~ c_in(c_List_Olist_OCons(X0,X1,X2),c_List_Olists(X3,X2),tc_List_Olist(X2)) ),
inference(cnf_transformation,[status(thm)],[f1559]) ).
fof(f1602,plain,
! [X0,X1,X2] :
( c_in(c_Main_OInterI__1(X0,X1,X2),X1,tc_set(X2))
| c_in(X0,c_Inter(X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f1604,plain,
! [X0,X1] : c_in(X0,c_UNIV,X1),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f1607,plain,
! [X0,X1] : c_lessequals(c_emptyset,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f1608,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f1610,plain,
! [V_A,V_B] :
( V_A = V_B
| ! [T_a] :
( c_less(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_A,V_B,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f1611,plain,
! [X0,X1,X2] :
( X0 = X1
| c_less(X0,X1,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1610]) ).
fof(f1619,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f1620,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f1621,plain,
! [V_B,V_A] :
( V_A = V_B
| ! [T_a] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f111]) ).
fof(f1622,plain,
! [X0,X1,X2] :
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1621]) ).
fof(f1739,plain,
class_Orderings_Oorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f1761,plain,
class_Orderings_Olinorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f1768,plain,
! [X0] : class_Orderings_Oorder(tc_set(X0)),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f2754,plain,
! [X0] : c_List_Olist_ONil = c_List_Orev(c_List_Olist_ONil,X0),
inference(cnf_transformation,[status(thm)],[f1215]) ).
fof(f2774,plain,
! [X0,X1] : c_append(c_List_Olist_ONil,X0,X1) = X0,
inference(cnf_transformation,[status(thm)],[f1227]) ).
fof(f2775,plain,
! [V_ys] :
( V_ys = c_List_Olist_ONil
| ! [V_xs,T_a] : c_append(V_xs,V_ys,T_a) != V_xs ),
inference(miniscoping,[status(thm)],[f1228]) ).
fof(f2776,plain,
! [X0,X1,X2] :
( X1 = c_List_Olist_ONil
| c_append(X0,X1,X2) != X0 ),
inference(cnf_transformation,[status(thm)],[f2775]) ).
fof(f2790,plain,
! [X0,X1,X2] : c_List_Olist_ONil != c_List_Olist_OCons(X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f1238]) ).
fof(f2796,plain,
! [X0,X1,X2,X3] :
( X0 = c_append(c_List_Orev(X3,X1),c_List_Olist_OCons(X2,c_List_Olist_ONil,X1),X1)
| c_List_Orev(X0,X1) != c_List_Olist_OCons(X2,X3,X1) ),
inference(cnf_transformation,[status(thm)],[f1242]) ).
fof(f2797,plain,
! [X0,X1,X2] : c_List_Orev(c_append(c_List_Orev(X0,X1),c_List_Olist_OCons(X2,c_List_Olist_ONil,X1),X1),X1) = c_List_Olist_OCons(X2,X0,X1),
inference(cnf_transformation,[status(thm)],[f1243]) ).
fof(f2845,plain,
! [X0] : ~ c_less(X0,c_0,tc_nat),
inference(cnf_transformation,[status(thm)],[f1279]) ).
fof(f2919,plain,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(thm)],[f1333]) ).
fof(f2920,plain,
! [V_a,V_B,T_a] :
( ! [V_b] : c_in(V_a,c_insert(V_b,V_B,T_a),T_a)
| ~ c_in(V_a,V_B,T_a) ),
inference(miniscoping,[status(thm)],[f1334]) ).
fof(f2921,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_insert(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2920]) ).
fof(f2923,plain,
! [V_a,V_b] :
( V_a = V_b
| ! [V_A,T_a] :
( c_in(V_a,V_A,T_a)
| ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a) ) ),
inference(miniscoping,[status(thm)],[f1336]) ).
fof(f2924,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| c_in(X0,X2,X3)
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
inference(cnf_transformation,[status(thm)],[f2923]) ).
fof(f2990,plain,
! [X0,X1,X2] : c_Message_Omsg_ONonce(X0) != c_Message_OHPair(X1,X2),
inference(cnf_transformation,[status(thm)],[f1382]) ).
fof(f3014,plain,
! [V_X,V_H] :
( c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
| ! [V_Y] : ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(V_H),tc_Message_Omsg) ),
inference(miniscoping,[status(thm)],[f1401]) ).
fof(f3015,plain,
! [X0,X1,X2] :
( c_in(X0,c_Message_Oparts(X2),tc_Message_Omsg)
| ~ c_in(c_Message_Omsg_OMPair(X0,X1),c_Message_Oparts(X2),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f3014]) ).
fof(f3028,plain,
! [X0] : c_Message_Oagent_OFriend(X0) != c_Message_Oagent_OSpy,
inference(cnf_transformation,[status(thm)],[f1412]) ).
fof(f3048,plain,
! [X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,X1,tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f1427]) ).
fof(f3050,plain,
! [X0,X1] :
( c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg)
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(X1)),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f1429]) ).
fof(f3060,plain,
! [X0,X1] :
( ~ c_lessequals(v_sko__upX(X1),X0,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(X0),c_Message_Oparts(c_insert(X1,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f1438]) ).
fof(f3061,plain,
! [V_k,V_n] :
( c_lessequals(V_k,V_n,tc_nat)
| ! [V_m] : ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat) ),
inference(miniscoping,[status(thm)],[f1439]) ).
fof(f3062,plain,
! [X0,X1,X2] :
( c_lessequals(X1,X2,tc_nat)
| ~ c_lessequals(c_plus(X0,X1,tc_nat),X2,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f3061]) ).
fof(f3063,plain,
! [V_m,V_n] :
( c_lessequals(V_m,V_n,tc_nat)
| ! [V_k] : ~ c_lessequals(c_plus(V_m,V_k,tc_nat),V_n,tc_nat) ),
inference(miniscoping,[status(thm)],[f1440]) ).
fof(f3064,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X2,tc_nat)
| ~ c_lessequals(c_plus(X0,X1,tc_nat),X2,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f3063]) ).
fof(f3099,plain,
! [X0] :
( ~ c_lessequals(v_x,X0,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_list),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f1469]) ).
fof(f3105,plain,
( ! [V_U] : c_lessequals(V_U,v_xd(V_U),tc_nat)
| ! [V_W] : c_lessequals(V_W,v_xd(V_W),tc_nat) ),
inference(miniscoping,[status(thm)],[f1473]) ).
fof(f3106,plain,
! [X0,X1] :
( c_lessequals(X1,v_xd(X1),tc_nat)
| c_lessequals(X0,v_xd(X0),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f3105]) ).
fof(f3114,plain,
! [V_U] :
( 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)
| c_in(c_Message_Omsg_ONonce(v_xd(V_U)),c_Event_Oused(v_list),tc_Message_Omsg)
| ! [V_X] :
( 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_X)),c_Event_Oused(v_list),tc_Message_Omsg) ) ),
inference(miniscoping,[status(thm)],[f1478]) ).
fof(f3115,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(v_xd(X1)),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(X0)),c_Message_Oparts(c_insert(v_xc,c_emptyset,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Event_Oused(v_list),tc_Message_Omsg) ),
inference(cnf_transformation,[status(thm)],[f3114]) ).
fof(f3123,definition,
! [X0] :
( sQ2_spl
<=> c_lessequals(X0,v_xd(X0),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f3124,plain,
! [X0] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(X0),tc_nat) ),
inference(component_clause,[status(thm)],[f3123]) ).
fof(f3128,plain,
sQ2_spl,
inference(split_clause,[status(thm)],[f3106,f3123]) ).
fof(f3129,definition,
! [X0] :
( sQ3_spl
<=> ( 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(X0)),c_Event_Oused(v_list),tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f3130,plain,
! [X0] :
( ~ sQ3_spl
| 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(X0)),c_Event_Oused(v_list),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f3129]) ).
fof(f3136,plain,
sQ3_spl,
inference(split_clause,[status(thm)],[f3115,f3129]) ).
fof(f3147,definition,
( sQ4_spl
<=> v_a = v_a ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f3149,plain,
( sQ4_spl
| v_a != v_a ),
inference(component_clause,[status(thm)],[f3147]) ).
fof(f3164,plain,
( sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3149]) ).
fof(f3165,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f3164]) ).
fof(f3235,plain,
! [X0,X1,X2] :
( ~ c_in(c_Message_Omsg_OMPair(X0,X2),X1,tc_Message_Omsg)
| c_in(X0,c_Message_Oparts(X1),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[f3015,f3048]) ).
fof(f4384,plain,
! [X0] : c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg),
inference(resolution,[status(thm)],[f1604,f3235]) ).
fof(f4723,definition,
! [X0,X1] :
( sQ17_spl
<=> ( X0 = X1
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(c_Message_Oparts(c_Message_Oparts(c_UNIV)))),tc_Message_Omsg) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f4724,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(c_Message_Oparts(c_Message_Oparts(c_UNIV)))),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f4723]) ).
fof(f4868,definition,
! [X0,X1] :
( sQ24_spl
<=> ( ~ c_in(X1,c_Message_Oparts(c_UNIV),tc_Message_Omsg)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f4869,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ c_in(X1,c_Message_Oparts(c_UNIV),tc_Message_Omsg)
| X0 = X1 ),
inference(component_clause,[status(thm)],[f4868]) ).
fof(f5211,plain,
! [X0,X1,X2,X3] :
( ~ c_in(c_Main_Oin__listsI__1(c_insert(X1,X2,X3),X0,X3),X2,X3)
| c_in(X0,c_List_Olists(c_insert(X1,X2,X3),X3),tc_List_Olist(X3)) ),
inference(resolution,[status(thm)],[f1545,f2921]) ).
fof(f5320,plain,
! [X0,X1,X2] : c_in(X0,c_List_Olists(c_insert(X1,c_UNIV,X2),X2),tc_List_Olist(X2)),
inference(resolution,[status(thm)],[f5211,f1604]) ).
fof(f6101,plain,
! [X0,X1,X2] : c_in(X0,c_insert(X1,c_UNIV,X2),X2),
inference(resolution,[status(thm)],[f1560,f5320]) ).
fof(f6174,plain,
! [X0,X1] :
( ~ sQ24_spl
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f4869,f4384]) ).
fof(f6175,plain,
( ~ sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3028,f6174]) ).
fof(f6187,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f6175]) ).
fof(f6191,definition,
! [X2,X3] :
( sQ66_spl
<=> X2 = X3 ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f6192,plain,
! [X0,X1] :
( ~ sQ66_spl
| X0 = X1 ),
inference(component_clause,[status(thm)],[f6191]) ).
fof(f6222,plain,
( ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2990,f6192]) ).
fof(f6223,plain,
~ sQ66_spl,
inference(contradiction_clause,[status(thm)],[f6222]) ).
fof(f6308,definition,
! [X0] :
( sQ72_spl
<=> ~ class_Orderings_Oorder(tc_set(X0)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f6309,plain,
! [X0] :
( ~ sQ72_spl
| ~ class_Orderings_Oorder(tc_set(X0)) ),
inference(component_clause,[status(thm)],[f6308]) ).
fof(f6316,plain,
( ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6309,f1768]) ).
fof(f6317,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f6316]) ).
fof(f10112,plain,
! [X0,X1] : c_in(X0,c_Inter(c_emptyset,X1),X1),
inference(resolution,[status(thm)],[f1602,f2919]) ).
fof(f10547,plain,
! [X0,X1] : ~ c_less(X0,c_emptyset,tc_set(X1)),
inference(resolution,[status(thm)],[f1608,f1607]) ).
fof(f11064,plain,
! [X0,X1,X2,X3] :
( c_Main_OsubsetI__1(c_insert(X0,X1,X2),X3,X2) = X0
| c_in(c_Main_OsubsetI__1(c_insert(X0,X1,X2),X3,X2),X1,X2)
| c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(resolution,[status(thm)],[f1619,f2924]) ).
fof(f11081,plain,
! [X0,X1] :
( c_in(c_Main_OsubsetI__1(c_Message_Oparts(c_Message_Oparts(X0)),X1,tc_Message_Omsg),c_Message_Oparts(X0),tc_Message_Omsg)
| c_lessequals(c_Message_Oparts(c_Message_Oparts(X0)),X1,tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1619,f3050]) ).
fof(f11095,plain,
! [X0,X1] : c_lessequals(X0,c_Inter(c_emptyset,X1),tc_set(X1)),
inference(resolution,[status(thm)],[f1620,f10112]) ).
fof(f11112,plain,
! [X0] : c_lessequals(X0,c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)),
inference(resolution,[status(thm)],[f1620,f4384]) ).
fof(f11143,plain,
! [X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_Message_Oparts(X1),tc_Message_Omsg),X1,tc_Message_Omsg)
| c_lessequals(X0,c_Message_Oparts(X1),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f1620,f3048]) ).
fof(f11146,plain,
! [X0,X1,X2] : c_lessequals(X0,c_insert(X1,c_UNIV,X2),tc_set(X2)),
inference(resolution,[status(thm)],[f1620,f6101]) ).
fof(f11147,plain,
! [X0,X1,X2,X3] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_insert(X1,X2,X3),X3),X2,X3)
| c_lessequals(X0,c_insert(X1,X2,X3),tc_set(X3)) ),
inference(resolution,[status(thm)],[f1620,f2921]) ).
fof(f11237,plain,
! [X0,X1] :
( X0 = c_Inter(c_emptyset,X1)
| c_less(X0,c_Inter(c_emptyset,X1),tc_set(X1)) ),
inference(resolution,[status(thm)],[f11095,f1611]) ).
fof(f11238,plain,
! [X0,X1] : ~ c_less(c_Inter(c_emptyset,X0),X1,tc_set(X0)),
inference(resolution,[status(thm)],[f11095,f1608]) ).
fof(f11241,plain,
! [X0] :
( X0 = c_Message_Oparts(c_UNIV)
| c_less(X0,c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f11112,f1611]) ).
fof(f11242,plain,
! [X0] : ~ c_less(c_Message_Oparts(c_UNIV),X0,tc_set(tc_Message_Omsg)),
inference(resolution,[status(thm)],[f11112,f1608]) ).
fof(f11419,plain,
! [X0,X1,X2] : ~ c_less(c_insert(X0,c_UNIV,X1),X2,tc_set(X1)),
inference(resolution,[status(thm)],[f11146,f1608]) ).
fof(f11867,plain,
c_Inter(c_emptyset,tc_Message_Omsg) = c_Message_Oparts(c_UNIV),
inference(resolution,[status(thm)],[f11241,f11238]) ).
fof(f12967,plain,
! [X0,X1] : c_insert(X0,c_UNIV,X1) = c_Inter(c_emptyset,X1),
inference(resolution,[status(thm)],[f11237,f11419]) ).
fof(f13876,plain,
! [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)) ),
inference(resolution,[status(thm)],[f11064,f1620]) ).
fof(f13920,plain,
! [X0,X1,X2] :
( c_Main_OsubsetI__1(c_insert(X0,X1,X2),X1,X2) = X0
| c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f13876]) ).
fof(f13952,plain,
! [X0] :
( c_lessequals(c_Message_Oparts(c_Message_Oparts(X0)),c_Message_Oparts(X0),tc_set(tc_Message_Omsg))
| c_lessequals(c_Message_Oparts(c_Message_Oparts(X0)),c_Message_Oparts(X0),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f11081,f1620]) ).
fof(f13964,plain,
! [X0] : c_lessequals(c_Message_Oparts(c_Message_Oparts(X0)),c_Message_Oparts(X0),tc_set(tc_Message_Omsg)),
inference(duplicate_literals_removal,[status(thm)],[f13952]) ).
fof(f13984,plain,
! [X0] :
( c_lessequals(X0,c_Message_Oparts(X0),tc_set(tc_Message_Omsg))
| c_lessequals(X0,c_Message_Oparts(X0),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f11143,f1619]) ).
fof(f14007,plain,
! [X0] : c_lessequals(X0,c_Message_Oparts(X0),tc_set(tc_Message_Omsg)),
inference(duplicate_literals_removal,[status(thm)],[f13984]) ).
fof(f14039,plain,
! [X0] : ~ c_less(c_Message_Oparts(X0),X0,tc_set(tc_Message_Omsg)),
inference(resolution,[status(thm)],[f14007,f1608]) ).
fof(f14052,plain,
! [X0] :
( c_Message_Oparts(c_Message_Oparts(X0)) = c_Message_Oparts(X0)
| c_less(c_Message_Oparts(c_Message_Oparts(X0)),c_Message_Oparts(X0),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[f13964,f1611]) ).
fof(f14061,plain,
! [X0] : c_Message_Oparts(c_Message_Oparts(X0)) = c_Message_Oparts(X0),
inference(forward_subsumption_resolution,[status(thm)],[f14052,f14039]) ).
fof(f14145,plain,
! [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)) ),
inference(resolution,[status(thm)],[f11147,f1619]) ).
fof(f14166,plain,
! [X0,X1,X2] : c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)),
inference(duplicate_literals_removal,[status(thm)],[f14145]) ).
fof(f14180,plain,
! [X0,X1,X2] :
( X1 = c_insert(X0,X1,X2)
| ~ c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2)) ),
inference(resolution,[status(thm)],[f14166,f1622]) ).
fof(f14199,definition,
( sQ148_spl
<=> c_less(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f14200,plain,
( ~ sQ148_spl
| c_less(c_emptyset,c_emptyset,tc_set(tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f14199]) ).
fof(f14206,plain,
( ~ sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14200,f10547]) ).
fof(f14207,plain,
~ sQ148_spl,
inference(contradiction_clause,[status(thm)],[f14206]) ).
fof(f14234,definition,
( sQ151_spl
<=> c_less(c_Message_Oparts(c_UNIV),c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f14235,plain,
( ~ sQ151_spl
| c_less(c_Message_Oparts(c_UNIV),c_Message_Oparts(c_UNIV),tc_set(tc_Message_Omsg)) ),
inference(component_clause,[status(thm)],[f14234]) ).
fof(f14242,plain,
( ~ sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14235,f11242]) ).
fof(f14243,plain,
~ sQ151_spl,
inference(contradiction_clause,[status(thm)],[f14242]) ).
fof(f16107,plain,
! [X0,X1,X2] :
( c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))
| c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f13920,f1620]) ).
fof(f16116,plain,
! [X0,X1,X2] :
( c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f16107]) ).
fof(f16118,plain,
! [X0,X1,X2] :
( X1 = c_insert(X0,X1,X2)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[status(thm)],[f16116,f14180]) ).
fof(f16131,definition,
! [X0] :
( sQ164_spl
<=> ~ c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f16132,plain,
! [X0] :
( ~ sQ164_spl
| ~ c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg) ),
inference(component_clause,[status(thm)],[f16131]) ).
fof(f16136,plain,
( ~ sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16132,f4384]) ).
fof(f16137,plain,
~ sQ164_spl,
inference(contradiction_clause,[status(thm)],[f16136]) ).
fof(f16142,plain,
! [X0,X1] :
( c_UNIV = c_Inter(c_emptyset,X1)
| ~ c_in(X0,c_UNIV,X1) ),
inference(paramodulation,[status(thm)],[f12967,f16118]) ).
fof(f16145,plain,
! [X0] : c_UNIV = c_Inter(c_emptyset,X0),
inference(forward_subsumption_resolution,[status(thm)],[f16142,f1604]) ).
fof(f16150,plain,
c_UNIV = c_Message_Oparts(c_UNIV),
inference(backward_demodulation,[status(thm)],[f16145,f11867]) ).
fof(f16567,definition,
! [X0,X1] :
( sQ168_spl
<=> ~ c_in(X0,c_UNIV,X1) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f16568,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ c_in(X0,c_UNIV,X1) ),
inference(component_clause,[status(thm)],[f16567]) ).
fof(f16584,plain,
( ~ sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16568,f1604]) ).
fof(f16585,plain,
~ sQ168_spl,
inference(contradiction_clause,[status(thm)],[f16584]) ).
fof(f18714,definition,
! [X0] :
( sQ214_spl
<=> X0 != X0 ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f18715,plain,
! [X0] :
( ~ sQ214_spl
| X0 != X0 ),
inference(component_clause,[status(thm)],[f18714]) ).
fof(f18718,plain,
( ~ sQ214_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18715]) ).
fof(f18719,plain,
~ sQ214_spl,
inference(contradiction_clause,[status(thm)],[f18718]) ).
fof(f19193,definition,
( sQ217_spl
<=> class_Orderings_Oorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f19195,plain,
( sQ217_spl
| ~ class_Orderings_Oorder(tc_nat) ),
inference(component_clause,[status(thm)],[f19193]) ).
fof(f22321,definition,
( sQ237_spl
<=> c_less(c_0,c_0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f22322,plain,
( ~ sQ237_spl
| c_less(c_0,c_0,tc_nat) ),
inference(component_clause,[status(thm)],[f22321]) ).
fof(f22724,plain,
( sQ217_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19195,f1739]) ).
fof(f22725,plain,
sQ217_spl,
inference(contradiction_clause,[status(thm)],[f22724]) ).
fof(f24742,plain,
! [X0,X1,X2] :
( c_List_Olist_OCons(X2,c_List_Olist_ONil,X1) = c_List_Olist_ONil
| c_List_Orev(c_List_Orev(X0,X1),X1) != c_List_Olist_OCons(X2,X0,X1) ),
inference(resolution,[status(thm)],[f2796,f2776]) ).
fof(f24747,plain,
! [X0,X1,X2] : c_List_Orev(c_List_Orev(X0,X1),X1) != c_List_Olist_OCons(X2,X0,X1),
inference(forward_subsumption_resolution,[status(thm)],[f24742,f2790]) ).
fof(f24750,plain,
! [X0,X1] : c_List_Orev(c_append(c_List_Olist_ONil,c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1),X1) = c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),
inference(paramodulation,[status(thm)],[f2754,f2797]) ).
fof(f24755,plain,
! [X0,X1] : c_List_Orev(c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1) = c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),
inference(forward_demodulation,[status(thm)],[f2774,f24750]) ).
fof(f25066,plain,
! [X0,X1,X2] : c_List_Orev(c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1) != c_List_Olist_OCons(X2,c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1),
inference(paramodulation,[status(thm)],[f24755,f24747]) ).
fof(f25072,plain,
! [X0,X1,X2] : c_List_Olist_OCons(X0,c_List_Olist_ONil,X1) != c_List_Olist_OCons(X2,c_List_Olist_OCons(X0,c_List_Olist_ONil,X1),X1),
inference(forward_demodulation,[status(thm)],[f24755,f25066]) ).
fof(f25079,plain,
! [X0,X1] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(c_plus(X1,X0,tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f3062,f3124]) ).
fof(f25096,plain,
! [X0,X1] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(c_plus(X0,X1,tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f3064,f3124]) ).
fof(f25107,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(c_plus(c_plus(X0,X1,tc_nat),X2,tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f25096,f3064]) ).
fof(f25188,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(c_plus(c_plus(c_plus(X0,X1,tc_nat),X2,tc_nat),X3,tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f25107,f3064]) ).
fof(f25816,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ2_spl
| c_lessequals(X0,v_xd(c_plus(c_plus(c_plus(c_plus(X0,X1,tc_nat),X2,tc_nat),X3,tc_nat),X4,tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f25188,f3064]) ).
fof(f27608,definition,
( sQ405_spl
<=> class_Orderings_Olinorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition]) ).
fof(f27610,plain,
( sQ405_spl
| ~ class_Orderings_Olinorder(tc_nat) ),
inference(component_clause,[status(thm)],[f27608]) ).
fof(f28656,plain,
( sQ405_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27610,f1761]) ).
fof(f28657,plain,
sQ405_spl,
inference(contradiction_clause,[status(thm)],[f28656]) ).
fof(f28661,plain,
( ~ sQ237_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22322,f2845]) ).
fof(f28662,plain,
~ sQ237_spl,
inference(contradiction_clause,[status(thm)],[f28661]) ).
fof(f28663,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(c_Message_Oparts(c_UNIV))),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f14061,f4724]) ).
fof(f28664,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1
| ~ c_in(X0,c_Message_Oparts(c_Message_Oparts(c_UNIV)),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f14061,f28663]) ).
fof(f28665,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1
| ~ c_in(X0,c_Message_Oparts(c_UNIV),tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f14061,f28664]) ).
fof(f28666,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1
| ~ c_in(X0,c_UNIV,tc_Message_Omsg) ),
inference(forward_demodulation,[status(thm)],[f16150,f28665]) ).
fof(f28667,plain,
! [X0,X1] :
( ~ sQ17_spl
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f28666,f1604]) ).
fof(f28699,plain,
( ~ sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f25072,f28667]) ).
fof(f28737,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f28699]) ).
fof(f30402,plain,
! [X0] :
( ~ sQ3_spl
| c_in(c_Message_Omsg_ONonce(v_xd(X0)),c_Event_Oused(v_list),tc_Message_Omsg)
| ~ c_lessequals(v_sko__upX(v_xc),v_xd(X0),tc_nat) ),
inference(resolution,[status(thm)],[f3060,f3130]) ).
fof(f30441,plain,
! [X0] :
( ~ sQ3_spl
| ~ c_lessequals(v_x,v_xd(X0),tc_nat)
| ~ c_lessequals(v_sko__upX(v_xc),v_xd(X0),tc_nat) ),
inference(resolution,[status(thm)],[f30402,f3099]) ).
fof(f30482,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ c_lessequals(v_x,v_xd(c_plus(X0,v_sko__upX(v_xc),tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f30441,f25079]) ).
fof(f30485,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| $false ),
inference(resolution,[status(thm)],[f30482,f25816]) ).
fof(f30500,plain,
( ~ sQ2_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f30485]) ).
fof(f30501,plain,
$false,
inference(sat_refutation,[status(thm)],[f3128,f3136,f3165,f6187,f6223,f6317,f14207,f14243,f16137,f16585,f18719,f22725,f28657,f28662,f28737,f30500]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV283-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n002.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 08:40:46 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.27/0.52 % Drodi V4.1.1
% 49.00/6.72 % Refutation found
% 49.00/6.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 49.00/6.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.02/6.92 % Elapsed time: 6.466002 seconds
% 5.02/6.92 % CPU time: 49.820632 seconds
% 5.02/6.92 % Total memory used: 677.951 MB
% 5.02/6.92 % Net memory used: 635.600 MB
%------------------------------------------------------------------------------