%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV282-2 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:30:01 PM UTC 2025
% Result : Timeout 293.19s 222.68s
% Output : None
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 13
% Syntax : Number of formulae : 138 ( 60 unt; 0 typ; 0 def)
% Number of atoms : 290 ( 148 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 211 ( 59 ~; 152 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 184 ( 184 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ c_lessequals > c_less > c_in > c_plus > c_minus > c_SetInterval_OatMost > c_Finite__Set_Ocard > c_Binomial_Obinomial > #nlpp > v_sko__urX > c_Suc > c_Message_Omsg_ONonce > c_Event_Oused > v_evs_H_H > v_evs_H > v_evs > tc_nat > tc_Message_Omsg > c_1 > c_0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v_evs_H_H,type,
v_evs_H_H: $i ).
tff(v_sko__urX,type,
v_sko__urX: $i > $i ).
tff(c_minus,type,
c_minus: ( $i * $i * $i ) > $i ).
tff(c_SetInterval_OatMost,type,
c_SetInterval_OatMost: ( $i * $i ) > $i ).
tff(c_0,type,
c_0: $i ).
tff(c_1,type,
c_1: $i ).
tff(c_Suc,type,
c_Suc: $i > $i ).
tff(c_lessequals,type,
c_lessequals: ( $i * $i * $i ) > $o ).
tff(c_in,type,
c_in: ( $i * $i * $i ) > $o ).
tff(tc_nat,type,
tc_nat: $i ).
tff(c_Finite__Set_Ocard,type,
c_Finite__Set_Ocard: ( $i * $i ) > $i ).
tff(c_Event_Oused,type,
c_Event_Oused: $i > $i ).
tff(c_Binomial_Obinomial,type,
c_Binomial_Obinomial: ( $i * $i ) > $i ).
tff(tc_Message_Omsg,type,
tc_Message_Omsg: $i ).
tff(c_less,type,
c_less: ( $i * $i * $i ) > $o ).
tff(v_evs_H,type,
v_evs_H: $i ).
tff(v_evs,type,
v_evs: $i ).
tff(c_plus,type,
c_plus: ( $i * $i * $i ) > $i ).
tff(c_Message_Omsg_ONonce,type,
c_Message_Omsg_ONonce: $i > $i ).
tff(f_55,axiom,
! [V_n] : c_less(V_n,c_Suc(V_n),tc_nat),
file(unknown,unknown) ).
tff(f_53,axiom,
! [V_n,V_m] : c_lessequals(V_n,c_plus(V_n,V_m,tc_nat),tc_nat),
file(unknown,unknown) ).
tff(f_51,axiom,
! [V_m] : ( c_minus(V_m,V_m,tc_nat) = c_0 ),
file(unknown,unknown) ).
tff(f_49,axiom,
! [V_m,V_n] :
( ( c_minus(V_m,V_n,tc_nat) != c_0 )
| c_lessequals(V_m,V_n,tc_nat) ),
file(unknown,unknown) ).
tff(f_44,axiom,
c_1 = c_Suc(c_0),
file(unknown,unknown) ).
tff(f_39,axiom,
! [V_y] : ( c_Binomial_Obinomial(V_y,c_Suc(c_0)) = V_y ),
file(unknown,unknown) ).
tff(f_43,axiom,
! [V_n] : ( c_Binomial_Obinomial(V_n,c_0) = c_1 ),
file(unknown,unknown) ).
tff(f_41,axiom,
! [V_n,V_k] : ( c_Binomial_Obinomial(c_Suc(V_n),c_Suc(V_k)) = c_plus(c_Binomial_Obinomial(V_n,V_k),c_Binomial_Obinomial(V_n,c_Suc(V_k)),tc_nat) ),
file(unknown,unknown) ).
tff(f_65,axiom,
! [V_k,V_m,V_n] :
( ~ c_lessequals(c_plus(V_k,V_m,tc_nat),c_plus(V_k,V_n,tc_nat),tc_nat)
| c_lessequals(V_m,V_n,tc_nat) ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [V_U,V_W,V_V] :
( ( V_U = V_W )
| ( V_V = V_W )
| ( V_U = V_V )
| c_in(c_Message_Omsg_ONonce(V_W),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_V),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(v_evs),tc_Message_Omsg) ),
file(unknown,unknown) ).
tff(f_74,axiom,
! [V_U,V_evs] :
( ~ c_in(c_Message_Omsg_ONonce(V_U),c_Event_Oused(V_evs),tc_Message_Omsg)
| ~ c_lessequals(v_sko__urX(V_evs),V_U,tc_nat) ),
file(unknown,unknown) ).
tff(f_68,axiom,
! [V_j,V_i] : ~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
file(unknown,unknown) ).
tff(f_60,axiom,
! [V_m,V_n] :
( ~ c_lessequals(V_m,V_n,tc_nat)
| c_less(V_m,c_Suc(V_n),tc_nat) ),
file(unknown,unknown) ).
tff(c_18,plain,
! [V_n_13] : c_less(V_n_13,c_Suc(V_n_13),tc_nat),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_16,plain,
! [V_n_11,V_m_12] : c_lessequals(V_n_11,c_plus(V_n_11,V_m_12,tc_nat),tc_nat),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_14,plain,
! [V_m_10] : ( c_minus(V_m_10,V_m_10,tc_nat) = c_0 ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_12,plain,
! [V_m_8,V_n_9] :
( c_lessequals(V_m_8,V_n_9,tc_nat)
| ( c_minus(V_m_8,V_n_9,tc_nat) != c_0 ) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_10,plain,
c_Suc(c_0) = c_1,
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_4,plain,
! [V_y_4] : ( c_Binomial_Obinomial(V_y_4,c_Suc(c_0)) = V_y_4 ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_29,plain,
! [V_y_4] : ( c_Binomial_Obinomial(V_y_4,c_1) = V_y_4 ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_4]) ).
tff(c_8,plain,
! [V_n_7] : ( c_Binomial_Obinomial(V_n_7,c_0) = c_1 ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_114,plain,
! [V_n_47,V_k_48] : ( c_plus(c_Binomial_Obinomial(V_n_47,V_k_48),c_Binomial_Obinomial(V_n_47,c_Suc(V_k_48)),tc_nat) = c_Binomial_Obinomial(c_Suc(V_n_47),c_Suc(V_k_48)) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_132,plain,
! [V_n_7] : ( c_plus(c_1,c_Binomial_Obinomial(V_n_7,c_Suc(c_0)),tc_nat) = c_Binomial_Obinomial(c_Suc(V_n_7),c_Suc(c_0)) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_114]) ).
tff(c_138,plain,
! [V_n_7] : ( c_plus(c_1,V_n_7,tc_nat) = c_Suc(V_n_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_29,c_29,c_10,c_10,c_132]) ).
tff(c_151,plain,
! [V_n_52] : ( c_plus(c_1,V_n_52,tc_nat) = c_Suc(V_n_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_29,c_29,c_10,c_10,c_132]) ).
tff(c_22,plain,
! [V_m_17,V_n_18,V_k_16] :
( c_lessequals(V_m_17,V_n_18,tc_nat)
| ~ c_lessequals(c_plus(V_k_16,V_m_17,tc_nat),c_plus(V_k_16,V_n_18,tc_nat),tc_nat) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_157,plain,
! [V_n_52,V_n_18] :
( c_lessequals(V_n_52,V_n_18,tc_nat)
| ~ c_lessequals(c_Suc(V_n_52),c_plus(c_1,V_n_18,tc_nat),tc_nat) ),
inference(superposition,[status(thm),theory(equality)],[c_151,c_22]) ).
tff(c_19304,plain,
! [V_n_3556,V_n_3557] :
( c_lessequals(V_n_3556,V_n_3557,tc_nat)
| ~ c_lessequals(c_Suc(V_n_3556),c_Suc(V_n_3557),tc_nat) ),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_157]) ).
tff(c_23018,plain,
! [V_n_4235,V_n_4236] :
( c_lessequals(V_n_4235,V_n_4236,tc_nat)
| ( c_minus(c_Suc(V_n_4235),c_Suc(V_n_4236),tc_nat) != c_0 ) ),
inference(resolution,[status(thm)],[c_12,c_19304]) ).
tff(c_23185,plain,
! [V_n_4235] : c_lessequals(V_n_4235,V_n_4235,tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_14,c_23018]) ).
tff(c_345,plain,
! [V_U_55,V_V_56,V_W_57] :
( c_in(c_Message_Omsg_ONonce(V_U_55),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_V_56),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_W_57),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( V_V_56 = V_U_55 )
| ( V_W_57 = V_V_56 )
| ( V_W_57 = V_U_55 ) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_26,plain,
! [V_evs_22,V_U_21] :
( ~ c_lessequals(v_sko__urX(V_evs_22),V_U_21,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(V_U_21),c_Event_Oused(V_evs_22),tc_Message_Omsg) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_38033,plain,
! [V_U_6475,V_V_6476,V_W_6477] :
( ~ c_lessequals(v_sko__urX(v_evs),V_U_6475,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_V_6476),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_W_6477),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( V_V_6476 = V_U_6475 )
| ( V_W_6477 = V_V_6476 )
| ( V_W_6477 = V_U_6475 ) ),
inference(resolution,[status(thm)],[c_345,c_26]) ).
tff(c_38850,plain,
! [V_V_6574,V_W_6575] :
( c_in(c_Message_Omsg_ONonce(V_V_6574),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_W_6575),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_V_6574 )
| ( V_W_6575 = V_V_6574 )
| ( v_sko__urX(v_evs) = V_W_6575 ) ),
inference(resolution,[status(thm)],[c_23185,c_38033]) ).
tff(c_53469,plain,
! [V_V_8784,V_W_8785] :
( ~ c_lessequals(v_sko__urX(v_evs_H),V_V_8784,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_W_8785),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_V_8784 )
| ( V_W_8785 = V_V_8784 )
| ( v_sko__urX(v_evs) = V_W_8785 ) ),
inference(resolution,[status(thm)],[c_38850,c_26]) ).
tff(c_54530,plain,
! [V_W_8785] :
( c_in(c_Message_Omsg_ONonce(V_W_8785),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs_H) = v_sko__urX(v_evs) )
| ( v_sko__urX(v_evs_H) = V_W_8785 )
| ( v_sko__urX(v_evs) = V_W_8785 ) ),
inference(resolution,[status(thm)],[c_23185,c_53469]) ).
tff(c_54534,plain,
v_sko__urX(v_evs_H) = v_sko__urX(v_evs),
inference(splitLeft,[status(thm)],[c_54530]) ).
tff(c_54535,plain,
! [V_W_8914,V_V_8915] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),V_W_8914,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_V_8915),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_V_8915 )
| ( V_W_8914 = V_V_8915 )
| ( v_sko__urX(v_evs) = V_W_8914 ) ),
inference(resolution,[status(thm)],[c_38850,c_26]) ).
tff(c_55596,plain,
! [V_V_8915] :
( c_in(c_Message_Omsg_ONonce(V_V_8915),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_V_8915 )
| ( v_sko__urX(v_evs_H_H) = V_V_8915 )
| ( v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs) ) ),
inference(resolution,[status(thm)],[c_23185,c_54535]) ).
tff(c_56245,plain,
v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs),
inference(splitLeft,[status(thm)],[c_55596]) ).
tff(c_54533,plain,
! [V_W_8785,V_m_12] :
( c_in(c_Message_Omsg_ONonce(V_W_8785),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs_H),V_m_12,tc_nat) = v_sko__urX(v_evs) )
| ( c_plus(v_sko__urX(v_evs_H),V_m_12,tc_nat) = V_W_8785 )
| ( v_sko__urX(v_evs) = V_W_8785 ) ),
inference(resolution,[status(thm)],[c_16,c_53469]) ).
tff(c_123242,plain,
! [V_W_19671,V_m_19672] :
( c_in(c_Message_Omsg_ONonce(V_W_19671),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),V_m_19672,tc_nat) = v_sko__urX(v_evs) )
| ( c_plus(v_sko__urX(v_evs),V_m_19672,tc_nat) = V_W_19671 )
| ( v_sko__urX(v_evs) = V_W_19671 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_54534,c_54534,c_54533]) ).
tff(c_123276,plain,
! [V_m_19672,V_n_18,V_W_19671] :
( c_lessequals(V_m_19672,V_n_18,tc_nat)
| ~ c_lessequals(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),V_n_18,tc_nat),tc_nat)
| c_in(c_Message_Omsg_ONonce(V_W_19671),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),V_m_19672,tc_nat) = V_W_19671 )
| ( v_sko__urX(v_evs) = V_W_19671 ) ),
inference(superposition,[status(thm),theory(equality)],[c_123242,c_22]) ).
tff(c_129666,plain,
! [V_m_21273,V_n_21274,V_W_21275] :
( c_lessequals(V_m_21273,V_n_21274,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_W_21275),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),V_m_21273,tc_nat) = V_W_21275 )
| ( v_sko__urX(v_evs) = V_W_21275 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_123276]) ).
tff(c_24,plain,
! [V_j_19,V_i_20] : ~ c_less(c_plus(V_j_19,V_i_20,tc_nat),V_i_20,tc_nat),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_4063336,plain,
! [V_W_1789887,V_m_1789888,V_n_1789889] :
( ~ c_less(V_W_1789887,V_m_1789888,tc_nat)
| c_lessequals(V_m_1789888,V_n_1789889,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_W_1789887),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_W_1789887 ) ),
inference(superposition,[status(thm),theory(equality)],[c_129666,c_24]) ).
tff(c_4064849,plain,
! [V_n_1790450,V_n_1790451] :
( c_lessequals(c_Suc(V_n_1790450),V_n_1790451,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_n_1790450),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_n_1790450 ) ),
inference(resolution,[status(thm)],[c_18,c_4063336]) ).
tff(c_187,plain,
! [V_n_52,V_n_18] :
( c_lessequals(V_n_52,V_n_18,tc_nat)
| ~ c_lessequals(c_Suc(V_n_52),c_Suc(V_n_18),tc_nat) ),
inference(demodulation,[status(thm),theory(equality)],[c_138,c_157]) ).
tff(c_4072984,plain,
! [V_n_1791573,V_n_1791574] :
( c_lessequals(V_n_1791573,V_n_1791574,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_n_1791573),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_n_1791573 ) ),
inference(resolution,[status(thm)],[c_4064849,c_187]) ).
tff(c_72,plain,
! [V_m_33,V_n_34] :
( c_less(V_m_33,c_Suc(V_n_34),tc_nat)
| ~ c_lessequals(V_m_33,V_n_34,tc_nat) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_80,plain,
! [V_j_19,V_n_34] : ~ c_lessequals(c_plus(V_j_19,c_Suc(V_n_34),tc_nat),V_n_34,tc_nat),
inference(resolution,[status(thm)],[c_72,c_24]) ).
tff(c_176,plain,
! [V_n_34] : ~ c_lessequals(c_Suc(c_Suc(V_n_34)),V_n_34,tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_151,c_80]) ).
tff(c_134633,plain,
! [V_W_22908,V_n_22909] :
( c_in(c_Message_Omsg_ONonce(V_W_22908),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),c_Suc(c_Suc(V_n_22909)),tc_nat) = V_W_22908 )
| ( v_sko__urX(v_evs) = V_W_22908 ) ),
inference(resolution,[status(thm)],[c_129666,c_176]) ).
tff(c_135512,plain,
! [V_W_22908,V_n_22909] :
( ~ c_lessequals(V_W_22908,c_Suc(V_n_22909),tc_nat)
| c_in(c_Message_Omsg_ONonce(V_W_22908),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_W_22908 ) ),
inference(superposition,[status(thm),theory(equality)],[c_134633,c_80]) ).
tff(c_4075548,plain,
! [V_n_1792135] :
( c_in(c_Message_Omsg_ONonce(V_n_1792135),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_n_1792135 ) ),
inference(resolution,[status(thm)],[c_4072984,c_135512]) ).
tff(c_4075551,plain,
! [V_n_1792135] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),V_n_1792135,tc_nat)
| ( v_sko__urX(v_evs) = V_n_1792135 ) ),
inference(resolution,[status(thm)],[c_4075548,c_26]) ).
tff(c_4077113,plain,
! [V_n_1792584] :
( ~ c_lessequals(v_sko__urX(v_evs),V_n_1792584,tc_nat)
| ( v_sko__urX(v_evs) = V_n_1792584 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56245,c_4075551]) ).
tff(c_4077468,plain,
! [V_m_12] : ( c_plus(v_sko__urX(v_evs),V_m_12,tc_nat) = v_sko__urX(v_evs) ),
inference(resolution,[status(thm)],[c_16,c_4077113]) ).
tff(c_4077473,plain,
! [V_m_1793033] : ( c_plus(v_sko__urX(v_evs),V_m_1793033,tc_nat) = v_sko__urX(v_evs) ),
inference(resolution,[status(thm)],[c_16,c_4077113]) ).
tff(c_140,plain,
! [V_m_49,V_n_50,V_k_51] :
( c_lessequals(V_m_49,V_n_50,tc_nat)
| ~ c_lessequals(c_plus(V_k_51,V_m_49,tc_nat),c_plus(V_k_51,V_n_50,tc_nat),tc_nat) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_150,plain,
! [V_m_49,V_n_50,V_k_51] :
( c_lessequals(V_m_49,V_n_50,tc_nat)
| ( c_minus(c_plus(V_k_51,V_m_49,tc_nat),c_plus(V_k_51,V_n_50,tc_nat),tc_nat) != c_0 ) ),
inference(resolution,[status(thm)],[c_12,c_140]) ).
tff(c_4077490,plain,
! [V_m_1793033,V_n_50] :
( c_lessequals(V_m_1793033,V_n_50,tc_nat)
| ( c_minus(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),V_n_50,tc_nat),tc_nat) != c_0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4077473,c_150]) ).
tff(c_4078954,plain,
! [V_m_1793033,V_n_50] : c_lessequals(V_m_1793033,V_n_50,tc_nat),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_4077468,c_4077490]) ).
tff(c_135584,plain,
! [V_n_22909] :
( c_in(c_Message_Omsg_ONonce(v_evs_H_H),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),c_Suc(c_Suc(V_n_22909)),tc_nat) = v_evs_H_H )
| ( v_sko__urX(v_evs) = v_evs_H_H ) ),
inference(resolution,[status(thm)],[c_129666,c_176]) ).
tff(c_135587,plain,
( c_lessequals(v_sko__urX(v_evs),v_evs_H_H,tc_nat)
| c_in(c_Message_Omsg_ONonce(v_evs_H_H),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = v_evs_H_H ) ),
inference(superposition,[status(thm),theory(equality)],[c_135584,c_16]) ).
tff(c_3641809,plain,
v_sko__urX(v_evs) = v_evs_H_H,
inference(splitLeft,[status(thm)],[c_135587]) ).
tff(c_3641848,plain,
v_sko__urX(v_evs_H_H) = v_evs_H_H,
inference(demodulation,[status(thm),theory(equality)],[c_3641809,c_56245]) ).
tff(c_134612,plain,
! [V_W_21275,V_n_21274] :
( c_in(c_Message_Omsg_ONonce(V_W_21275),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_sko__urX(v_evs),c_Suc(c_Suc(V_n_21274)),tc_nat) = V_W_21275 )
| ( v_sko__urX(v_evs) = V_W_21275 ) ),
inference(resolution,[status(thm)],[c_129666,c_176]) ).
tff(c_3744357,plain,
! [V_W_1688264,V_n_1688265] :
( c_in(c_Message_Omsg_ONonce(V_W_1688264),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1688265)),tc_nat) = V_W_1688264 )
| ( v_evs_H_H = V_W_1688264 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3641809,c_3641809,c_134612]) ).
tff(c_3744360,plain,
! [V_W_1688264,V_n_1688265] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),V_W_1688264,tc_nat)
| ( c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1688265)),tc_nat) = V_W_1688264 )
| ( v_evs_H_H = V_W_1688264 ) ),
inference(resolution,[status(thm)],[c_3744357,c_26]) ).
tff(c_3750110,plain,
! [V_W_1690842,V_n_1690843] :
( ~ c_lessequals(v_evs_H_H,V_W_1690842,tc_nat)
| ( c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1690843)),tc_nat) = V_W_1690842 )
| ( v_evs_H_H = V_W_1690842 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3641848,c_3744360]) ).
tff(c_3781871,plain,
! [V_n_1699461,V_m_1699462] :
( ( c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1699461)),tc_nat) = c_plus(v_evs_H_H,V_m_1699462,tc_nat) )
| ( c_plus(v_evs_H_H,V_m_1699462,tc_nat) = v_evs_H_H ) ),
inference(resolution,[status(thm)],[c_16,c_3750110]) ).
tff(c_3788286,plain,
! [V_n_1701147,V_m_1701148] :
( ~ c_less(c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1701147)),tc_nat),V_m_1701148,tc_nat)
| ( c_plus(v_evs_H_H,V_m_1701148,tc_nat) = v_evs_H_H ) ),
inference(superposition,[status(thm),theory(equality)],[c_3781871,c_24]) ).
tff(c_3805478,plain,
! [V_n_1706816] : ( c_plus(v_evs_H_H,c_Suc(c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1706816)),tc_nat)),tc_nat) = v_evs_H_H ),
inference(resolution,[status(thm)],[c_18,c_3788286]) ).
tff(c_3805525,plain,
! [V_n_1706816] : ~ c_lessequals(v_evs_H_H,c_plus(v_evs_H_H,c_Suc(c_Suc(V_n_1706816)),tc_nat),tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_3805478,c_80]) ).
tff(c_3811652,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3805525]) ).
tff(c_3811654,plain,
v_sko__urX(v_evs) != v_evs_H_H,
inference(splitRight,[status(thm)],[c_135587]) ).
tff(c_3811653,plain,
( c_in(c_Message_Omsg_ONonce(v_evs_H_H),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| c_lessequals(v_sko__urX(v_evs),v_evs_H_H,tc_nat) ),
inference(splitRight,[status(thm)],[c_135587]) ).
tff(c_3811694,plain,
c_lessequals(v_sko__urX(v_evs),v_evs_H_H,tc_nat),
inference(splitLeft,[status(thm)],[c_3811653]) ).
tff(c_13911,plain,
! [V_W_57,V_U_55,V_V_56] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),V_W_57,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_U_55),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_V_56),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( V_V_56 = V_U_55 )
| ( V_W_57 = V_V_56 )
| ( V_W_57 = V_U_55 ) ),
inference(resolution,[status(thm)],[c_345,c_26]) ).
tff(c_59032,plain,
! [V_W_9560,V_U_9561,V_V_9562] :
( ~ c_lessequals(v_sko__urX(v_evs),V_W_9560,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_U_9561),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_V_9562),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( V_V_9562 = V_U_9561 )
| ( V_W_9560 = V_V_9562 )
| ( V_W_9560 = V_U_9561 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56245,c_13911]) ).
tff(c_62269,plain,
! [V_U_9951,V_V_9952] :
( c_in(c_Message_Omsg_ONonce(V_U_9951),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(V_V_9952),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( V_V_9952 = V_U_9951 )
| ( v_sko__urX(v_evs) = V_V_9952 )
| ( v_sko__urX(v_evs) = V_U_9951 ) ),
inference(resolution,[status(thm)],[c_23185,c_59032]) ).
tff(c_62275,plain,
! [V_V_9952,V_U_9951] :
( ~ c_lessequals(v_sko__urX(v_evs_H),V_V_9952,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_U_9951),c_Event_Oused(v_evs),tc_Message_Omsg)
| ( V_V_9952 = V_U_9951 )
| ( v_sko__urX(v_evs) = V_V_9952 )
| ( v_sko__urX(v_evs) = V_U_9951 ) ),
inference(resolution,[status(thm)],[c_62269,c_26]) ).
tff(c_79580,plain,
! [V_V_9952,V_U_9951] :
( ~ c_lessequals(v_sko__urX(v_evs),V_V_9952,tc_nat)
| c_in(c_Message_Omsg_ONonce(V_U_9951),c_Event_Oused(v_evs),tc_Message_Omsg)
| ( V_V_9952 = V_U_9951 )
| ( v_sko__urX(v_evs) = V_V_9952 )
| ( v_sko__urX(v_evs) = V_U_9951 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_54534,c_62275]) ).
tff(c_3813187,plain,
! [V_U_9951] :
( c_in(c_Message_Omsg_ONonce(V_U_9951),c_Event_Oused(v_evs),tc_Message_Omsg)
| ( v_evs_H_H = V_U_9951 )
| ( v_sko__urX(v_evs) = v_evs_H_H )
| ( v_sko__urX(v_evs) = V_U_9951 ) ),
inference(resolution,[status(thm)],[c_3811694,c_79580]) ).
tff(c_3814411,plain,
! [V_U_1709731] :
( c_in(c_Message_Omsg_ONonce(V_U_1709731),c_Event_Oused(v_evs),tc_Message_Omsg)
| ( v_evs_H_H = V_U_1709731 )
| ( v_sko__urX(v_evs) = V_U_1709731 ) ),
inference(negUnitSimplification,[status(thm)],[c_3811654,c_3813187]) ).
tff(c_3816679,plain,
! [V_U_1710196] :
( ~ c_lessequals(v_sko__urX(v_evs),V_U_1710196,tc_nat)
| ( v_evs_H_H = V_U_1710196 )
| ( v_sko__urX(v_evs) = V_U_1710196 ) ),
inference(resolution,[status(thm)],[c_3814411,c_26]) ).
tff(c_3840516,plain,
! [V_m_1716875] :
( ( c_plus(v_sko__urX(v_evs),V_m_1716875,tc_nat) = v_evs_H_H )
| ( c_plus(v_sko__urX(v_evs),V_m_1716875,tc_nat) = v_sko__urX(v_evs) ) ),
inference(resolution,[status(thm)],[c_16,c_3816679]) ).
tff(c_3840556,plain,
! [V_m_1716875,V_n_18] :
( c_lessequals(V_m_1716875,V_n_18,tc_nat)
| ~ c_lessequals(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),V_n_18,tc_nat),tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1716875,tc_nat) = v_evs_H_H ) ),
inference(superposition,[status(thm),theory(equality)],[c_3840516,c_22]) ).
tff(c_3843872,plain,
! [V_m_1717372,V_n_1717373] :
( c_lessequals(V_m_1717372,V_n_1717373,tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1717372,tc_nat) = v_evs_H_H ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3840556]) ).
tff(c_3975083,plain,
! [V_n_1764176,V_n_1764177] :
( ~ c_lessequals(v_evs_H_H,V_n_1764176,tc_nat)
| c_lessequals(c_Suc(V_n_1764176),V_n_1764177,tc_nat) ),
inference(superposition,[status(thm),theory(equality)],[c_3843872,c_80]) ).
tff(c_19451,plain,
! [V_n_3556] :
( c_lessequals(V_n_3556,c_0,tc_nat)
| ~ c_lessequals(c_Suc(V_n_3556),c_1,tc_nat) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_19304]) ).
tff(c_3977016,plain,
! [V_n_1764786] :
( c_lessequals(V_n_1764786,c_0,tc_nat)
| ~ c_lessequals(v_evs_H_H,V_n_1764786,tc_nat) ),
inference(resolution,[status(thm)],[c_3975083,c_19451]) ).
tff(c_3977460,plain,
! [V_m_1765395] : c_lessequals(c_plus(v_evs_H_H,V_m_1765395,tc_nat),c_0,tc_nat),
inference(resolution,[status(thm)],[c_16,c_3977016]) ).
tff(c_81,plain,
! [V_j_35,V_n_36] : ~ c_lessequals(c_plus(V_j_35,c_Suc(V_n_36),tc_nat),V_n_36,tc_nat),
inference(resolution,[status(thm)],[c_72,c_24]) ).
tff(c_84,plain,
! [V_j_35] : ~ c_lessequals(c_plus(V_j_35,c_1,tc_nat),c_0,tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_10,c_81]) ).
tff(c_3979206,plain,
$false,
inference(resolution,[status(thm)],[c_3977460,c_84]) ).
tff(c_3979208,plain,
~ c_lessequals(v_sko__urX(v_evs),v_evs_H_H,tc_nat),
inference(splitRight,[status(thm)],[c_3811653]) ).
tff(c_4079143,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4078954,c_3979208]) ).
tff(c_4080227,plain,
! [V_V_1793741] :
( c_in(c_Message_Omsg_ONonce(V_V_1793741),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs) = V_V_1793741 )
| ( v_sko__urX(v_evs_H_H) = V_V_1793741 ) ),
inference(splitRight,[status(thm)],[c_55596]) ).
tff(c_4080230,plain,
! [V_V_1793741] :
( ~ c_lessequals(v_sko__urX(v_evs_H),V_V_1793741,tc_nat)
| ( v_sko__urX(v_evs) = V_V_1793741 )
| ( v_sko__urX(v_evs_H_H) = V_V_1793741 ) ),
inference(resolution,[status(thm)],[c_4080227,c_26]) ).
tff(c_4081721,plain,
! [V_V_1793870] :
( ~ c_lessequals(v_sko__urX(v_evs),V_V_1793870,tc_nat)
| ( v_sko__urX(v_evs) = V_V_1793870 )
| ( v_sko__urX(v_evs_H_H) = V_V_1793870 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_54534,c_4080230]) ).
tff(c_4082854,plain,
! [V_m_1794128] :
( ( c_plus(v_sko__urX(v_evs),V_m_1794128,tc_nat) = v_sko__urX(v_evs) )
| ( c_plus(v_sko__urX(v_evs),V_m_1794128,tc_nat) = v_sko__urX(v_evs_H_H) ) ),
inference(resolution,[status(thm)],[c_16,c_4081721]) ).
tff(c_4090138,plain,
! [V_m_1795158] :
( ~ c_less(v_sko__urX(v_evs_H_H),V_m_1795158,tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1795158,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4082854,c_24]) ).
tff(c_4090945,plain,
c_plus(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs_H_H)),tc_nat) = v_sko__urX(v_evs),
inference(resolution,[status(thm)],[c_18,c_4090138]) ).
tff(c_4094789,plain,
~ c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H),tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_4090945,c_80]) ).
tff(c_4082904,plain,
! [V_m_1794128] :
( c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H),tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1794128,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4082854,c_16]) ).
tff(c_4108047,plain,
! [V_m_1794128] : ( c_plus(v_sko__urX(v_evs),V_m_1794128,tc_nat) = v_sko__urX(v_evs) ),
inference(negUnitSimplification,[status(thm)],[c_4094789,c_4082904]) ).
tff(c_4108052,plain,
! [V_m_1800160] : ( c_plus(v_sko__urX(v_evs),V_m_1800160,tc_nat) = v_sko__urX(v_evs) ),
inference(negUnitSimplification,[status(thm)],[c_4094789,c_4082904]) ).
tff(c_4108069,plain,
! [V_m_1800160,V_n_50] :
( c_lessequals(V_m_1800160,V_n_50,tc_nat)
| ( c_minus(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),V_n_50,tc_nat),tc_nat) != c_0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4108052,c_150]) ).
tff(c_4109375,plain,
! [V_m_1800160,V_n_50] : c_lessequals(V_m_1800160,V_n_50,tc_nat),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_4108047,c_4108069]) ).
tff(c_4109526,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4109375,c_4094789]) ).
tff(c_4110610,plain,
! [V_W_1800580] :
( c_in(c_Message_Omsg_ONonce(V_W_1800580),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| ( v_sko__urX(v_evs_H) = V_W_1800580 )
| ( v_sko__urX(v_evs) = V_W_1800580 ) ),
inference(splitRight,[status(thm)],[c_54530]) ).
tff(c_4112111,plain,
! [V_W_1800709] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),V_W_1800709,tc_nat)
| ( v_sko__urX(v_evs_H) = V_W_1800709 )
| ( v_sko__urX(v_evs) = V_W_1800709 ) ),
inference(resolution,[status(thm)],[c_4110610,c_26]) ).
tff(c_4112664,plain,
( ( v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs_H) )
| ( v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs) ) ),
inference(resolution,[status(thm)],[c_23185,c_4112111]) ).
tff(c_4113234,plain,
v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs),
inference(splitLeft,[status(thm)],[c_4112664]) ).
tff(c_4112667,plain,
! [V_m_12] :
( ( c_plus(v_sko__urX(v_evs_H_H),V_m_12,tc_nat) = v_sko__urX(v_evs_H) )
| ( c_plus(v_sko__urX(v_evs_H_H),V_m_12,tc_nat) = v_sko__urX(v_evs) ) ),
inference(resolution,[status(thm)],[c_16,c_4112111]) ).
tff(c_4116091,plain,
! [V_m_1801484] :
( ( c_plus(v_sko__urX(v_evs),V_m_1801484,tc_nat) = v_sko__urX(v_evs_H) )
| ( c_plus(v_sko__urX(v_evs),V_m_1801484,tc_nat) = v_sko__urX(v_evs) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4113234,c_4113234,c_4112667]) ).
tff(c_4146025,plain,
! [V_m_1808950] :
( ~ c_less(v_sko__urX(v_evs_H),V_m_1808950,tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1808950,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4116091,c_24]) ).
tff(c_4146846,plain,
c_plus(v_sko__urX(v_evs),c_Suc(v_sko__urX(v_evs_H)),tc_nat) = v_sko__urX(v_evs),
inference(resolution,[status(thm)],[c_18,c_4146025]) ).
tff(c_4146880,plain,
~ c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_4146846,c_80]) ).
tff(c_4116141,plain,
! [V_m_1801484] :
( c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat)
| ( c_plus(v_sko__urX(v_evs),V_m_1801484,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4116091,c_16]) ).
tff(c_4161749,plain,
! [V_m_1801484] : ( c_plus(v_sko__urX(v_evs),V_m_1801484,tc_nat) = v_sko__urX(v_evs) ),
inference(negUnitSimplification,[status(thm)],[c_4146880,c_4116141]) ).
tff(c_4161754,plain,
! [V_m_1813564] : ( c_plus(v_sko__urX(v_evs),V_m_1813564,tc_nat) = v_sko__urX(v_evs) ),
inference(negUnitSimplification,[status(thm)],[c_4146880,c_4116141]) ).
tff(c_4161771,plain,
! [V_m_1813564,V_n_50] :
( c_lessequals(V_m_1813564,V_n_50,tc_nat)
| ( c_minus(v_sko__urX(v_evs),c_plus(v_sko__urX(v_evs),V_n_50,tc_nat),tc_nat) != c_0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4161754,c_150]) ).
tff(c_4163093,plain,
! [V_m_1813564,V_n_50] : c_lessequals(V_m_1813564,V_n_50,tc_nat),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_4161749,c_4161771]) ).
tff(c_4163248,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4163093,c_4146880]) ).
tff(c_4163249,plain,
v_sko__urX(v_evs_H_H) = v_sko__urX(v_evs_H),
inference(splitRight,[status(thm)],[c_4112664]) ).
tff(c_4166108,plain,
! [V_m_1814306] :
( ( c_plus(v_sko__urX(v_evs_H),V_m_1814306,tc_nat) = v_sko__urX(v_evs_H) )
| ( c_plus(v_sko__urX(v_evs_H),V_m_1814306,tc_nat) = v_sko__urX(v_evs) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4163249,c_4163249,c_4112667]) ).
tff(c_4166136,plain,
! [V_m_1814306,V_n_18] :
( c_lessequals(V_m_1814306,V_n_18,tc_nat)
| ~ c_lessequals(v_sko__urX(v_evs_H),c_plus(v_sko__urX(v_evs_H),V_n_18,tc_nat),tc_nat)
| ( c_plus(v_sko__urX(v_evs_H),V_m_1814306,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4166108,c_22]) ).
tff(c_4180944,plain,
! [V_m_1817959,V_n_1817960] :
( c_lessequals(V_m_1817959,V_n_1817960,tc_nat)
| ( c_plus(v_sko__urX(v_evs_H),V_m_1817959,tc_nat) = v_sko__urX(v_evs) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_4166136]) ).
tff(c_4184059,plain,
! [V_m_1818441,V_n_1818442] :
( ~ c_less(v_sko__urX(v_evs),V_m_1818441,tc_nat)
| c_lessequals(V_m_1818441,V_n_1818442,tc_nat) ),
inference(superposition,[status(thm),theory(equality)],[c_4180944,c_24]) ).
tff(c_4184227,plain,
! [V_n_1818603] : c_lessequals(c_Suc(v_sko__urX(v_evs)),V_n_1818603,tc_nat),
inference(resolution,[status(thm)],[c_18,c_4184059]) ).
tff(c_4185061,plain,
! [V_n_18] : c_lessequals(v_sko__urX(v_evs),V_n_18,tc_nat),
inference(resolution,[status(thm)],[c_4184227,c_187]) ).
tff(c_4168210,plain,
! [V_m_1814435] :
( ~ c_less(v_sko__urX(v_evs_H),V_m_1814435,tc_nat)
| ( c_plus(v_sko__urX(v_evs_H),V_m_1814435,tc_nat) = v_sko__urX(v_evs) ) ),
inference(superposition,[status(thm),theory(equality)],[c_4166108,c_24]) ).
tff(c_4169017,plain,
c_plus(v_sko__urX(v_evs_H),c_Suc(v_sko__urX(v_evs_H)),tc_nat) = v_sko__urX(v_evs),
inference(resolution,[status(thm)],[c_18,c_4168210]) ).
tff(c_4169051,plain,
~ c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat),
inference(superposition,[status(thm),theory(equality)],[c_4169017,c_80]) ).
tff(c_4185733,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4185061,c_4169051]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV282-2 : TPTP v9.0.0. Released v3.2.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Apr 9 02:57:07 EDT 2025
% 0.13/0.35 % CPUTime :
% 293.19/222.68 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 293.19/222.70
% 293.19/222.70 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------