%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM926+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 08:53:38 AM UTC 2026
% Result : Theorem 0.89s 1.17s
% Output : Proof 0.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Groups_Oone__class_Oone_res,axiom,
! [X_a] :
( semiring_1(X_a)
=> ti(X_a,one_one(X_a)) = one_one(X_a) ),
file('theBenchmark.p',tsy_c_Groups_Oone__class_Oone_res) ).
fof(tsy_c_Groups_Oplus__class_Oplus_arg1,axiom,
! [B_1,B_2,X_a] :
( comm_semiring_1(X_a)
=> plus_plus(X_a,ti(X_a,B_1),B_2) = plus_plus(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Oplus__class_Oplus_arg1) ).
fof(tsy_c_Groups_Oplus__class_Oplus_arg2,axiom,
! [B_1,B_2,X_a] :
( comm_semiring_1(X_a)
=> plus_plus(X_a,B_1,ti(X_a,B_2)) = plus_plus(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Oplus__class_Oplus_arg2) ).
fof(tsy_c_Groups_Oplus__class_Oplus_res,axiom,
! [B_1,B_2,X_a] :
( comm_semiring_1(X_a)
=> ti(X_a,plus_plus(X_a,B_1,B_2)) = plus_plus(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Oplus__class_Oplus_res) ).
fof(tsy_c_Groups_Otimes__class_Otimes_arg1,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> times_times(X_a,ti(X_a,B_1),B_2) = times_times(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Otimes__class_Otimes_arg1) ).
fof(tsy_c_Groups_Otimes__class_Otimes_arg2,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> times_times(X_a,B_1,ti(X_a,B_2)) = times_times(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Otimes__class_Otimes_arg2) ).
fof(tsy_c_Groups_Otimes__class_Otimes_res,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> ti(X_a,times_times(X_a,B_1,B_2)) = times_times(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Groups_Otimes__class_Otimes_res) ).
fof(tsy_c_HOL_Oundefined_res,axiom,
! [X_a] : ti(X_a,undefined(X_a)) = undefined(X_a),
file('theBenchmark.p',tsy_c_HOL_Oundefined_res) ).
fof(tsy_c_IntPrimes_Ozprime_arg1,axiom,
! [B_1] :
( zprime(ti(int,B_1))
<=> zprime(B_1) ),
file('theBenchmark.p',tsy_c_IntPrimes_Ozprime_arg1) ).
fof(tsy_c_Int_OBit0_arg1,hypothesis,
! [B_1] : bit0(ti(int,B_1)) = bit0(B_1),
file('theBenchmark.p',tsy_c_Int_OBit0_arg1) ).
fof(tsy_c_Int_OBit0_res,hypothesis,
! [B_1] : ti(int,bit0(B_1)) = bit0(B_1),
file('theBenchmark.p',tsy_c_Int_OBit0_res) ).
fof(tsy_c_Int_OBit1_arg1,hypothesis,
! [B_1] : bit1(ti(int,B_1)) = bit1(B_1),
file('theBenchmark.p',tsy_c_Int_OBit1_arg1) ).
fof(tsy_c_Int_OBit1_res,hypothesis,
! [B_1] : ti(int,bit1(B_1)) = bit1(B_1),
file('theBenchmark.p',tsy_c_Int_OBit1_res) ).
fof(tsy_c_Int_OPls_res,hypothesis,
ti(int,pls) = pls,
file('theBenchmark.p',tsy_c_Int_OPls_res) ).
fof(tsy_c_Int_Onumber__class_Onumber__of_arg1,axiom,
! [B_1,X_a] :
( number(X_a)
=> number_number_of(X_a,ti(int,B_1)) = number_number_of(X_a,B_1) ),
file('theBenchmark.p',tsy_c_Int_Onumber__class_Onumber__of_arg1) ).
fof(tsy_c_Int_Onumber__class_Onumber__of_res,axiom,
! [B_1,X_a] :
( number(X_a)
=> ti(X_a,number_number_of(X_a,B_1)) = number_number_of(X_a,B_1) ),
file('theBenchmark.p',tsy_c_Int_Onumber__class_Onumber__of_res) ).
fof(tsy_c_Orderings_Oord__class_Oless_arg1,axiom,
! [B_1,B_2,X_a] :
( ( linorder(X_a)
& number(X_a) )
=> ( ord_less(X_a,ti(X_a,B_1),B_2)
<=> ord_less(X_a,B_1,B_2) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless_arg1) ).
fof(tsy_c_Orderings_Oord__class_Oless_arg2,axiom,
! [B_1,B_2,X_a] :
( ( linorder(X_a)
& number(X_a) )
=> ( ord_less(X_a,B_1,ti(X_a,B_2))
<=> ord_less(X_a,B_1,B_2) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless_arg2) ).
fof(tsy_c_Orderings_Oord__class_Oless__eq_arg1,axiom,
! [B_1,B_2,X_a] :
( ( linorder(X_a)
& number(X_a) )
=> ( ord_less_eq(X_a,ti(X_a,B_1),B_2)
<=> ord_less_eq(X_a,B_1,B_2) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless__eq_arg1) ).
fof(tsy_c_Orderings_Oord__class_Oless__eq_arg2,axiom,
! [B_1,B_2,X_a] :
( ( linorder(X_a)
& number(X_a) )
=> ( ord_less_eq(X_a,B_1,ti(X_a,B_2))
<=> ord_less_eq(X_a,B_1,B_2) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless__eq_arg2) ).
fof(tsy_c_Power_Opower__class_Opower_arg1,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> power_power(X_a,ti(X_a,B_1),B_2) = power_power(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Power_Opower__class_Opower_arg1) ).
fof(tsy_c_Power_Opower__class_Opower_arg2,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> power_power(X_a,B_1,ti(nat,B_2)) = power_power(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Power_Opower__class_Opower_arg2) ).
fof(tsy_c_Power_Opower__class_Opower_res,axiom,
! [B_1,B_2,X_a] :
( monoid_mult(X_a)
=> ti(X_a,power_power(X_a,B_1,B_2)) = power_power(X_a,B_1,B_2) ),
file('theBenchmark.p',tsy_c_Power_Opower__class_Opower_res) ).
fof(tsy_c_TwoSquares__Mirabelle__vsgmegnqdl_Ois__sum2sq_arg1,axiom,
! [B_1] :
( twoSqu33214720sum2sq(ti(int,B_1))
<=> twoSqu33214720sum2sq(B_1) ),
file('theBenchmark.p',tsy_c_TwoSquares__Mirabelle__vsgmegnqdl_Ois__sum2sq_arg1) ).
fof(tsy_v_m_res,hypothesis,
ti(int,m) = m,
file('theBenchmark.p',tsy_v_m_res) ).
fof(tsy_v_s_____res,axiom,
ti(int,s) = s,
file('theBenchmark.p',tsy_v_s_____res) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t,
file('theBenchmark.p',tsy_v_t_____res) ).
fof(fact_0_tpos,axiom,
ord_less_eq(int,one_one(int),t),
file('theBenchmark.p',fact_0_tpos) ).
fof(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( t = one_one(int)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( ord_less(int,one_one(int),t)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_3_t__l__p,axiom,
ord_less(int,t,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
file('theBenchmark.p',fact_3_t__l__p) ).
fof(fact_4_p,axiom,
zprime(plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
file('theBenchmark.p',fact_4_p) ).
fof(fact_5_t,axiom,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
file('theBenchmark.p',fact_5_t) ).
fof(fact_6_qf1pt,axiom,
twoSqu33214720sum2sq(times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t)),
file('theBenchmark.p',fact_6_qf1pt) ).
fof(fact_7_zadd__power2,axiom,
! [A_1,B] : power_power(int,plus_plus(int,A_1,B),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,plus_plus(int,power_power(int,A_1,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),A_1),B)),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))),
file('theBenchmark.p',fact_7_zadd__power2) ).
fof(fact_8_zadd__power3,axiom,
! [A_1,B] : power_power(int,plus_plus(int,A_1,B),number_number_of(nat,bit1(bit1(pls)))) = plus_plus(int,plus_plus(int,plus_plus(int,power_power(int,A_1,number_number_of(nat,bit1(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),power_power(int,A_1,number_number_of(nat,bit0(bit1(pls))))),B)),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),A_1),power_power(int,B,number_number_of(nat,bit0(bit1(pls)))))),power_power(int,B,number_number_of(nat,bit1(bit1(pls))))),
file('theBenchmark.p',fact_8_zadd__power3) ).
fof(fact_9_power2__sum,axiom,
! [X_a] :
( number_semiring(X_a)
=> ! [X_1,Y_1] : power_power(X_a,plus_plus(X_a,X_1,Y_1),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(X_a,plus_plus(X_a,power_power(X_a,X_1,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Y_1,number_number_of(nat,bit0(bit1(pls))))),times_times(X_a,times_times(X_a,number_number_of(X_a,bit0(bit1(pls))),X_1),Y_1)) ),
file('theBenchmark.p',fact_9_power2__sum) ).
fof(fact_10_power2__eq__square__number__of,axiom,
! [X_b] :
( ( number(X_b)
& monoid_mult(X_b) )
=> ! [W] : power_power(X_b,number_number_of(X_b,W),number_number_of(nat,bit0(bit1(pls)))) = times_times(X_b,number_number_of(X_b,W),number_number_of(X_b,W)) ),
file('theBenchmark.p',fact_10_power2__eq__square__number__of) ).
fof(fact_11_cube__square,axiom,
! [A_1] : times_times(int,A_1,power_power(int,A_1,number_number_of(nat,bit0(bit1(pls))))) = power_power(int,A_1,number_number_of(nat,bit1(bit1(pls)))),
file('theBenchmark.p',fact_11_cube__square) ).
fof(fact_12_one__power2,axiom,
! [X_a] :
( semiring_1(X_a)
=> power_power(X_a,one_one(X_a),number_number_of(nat,bit0(bit1(pls)))) = one_one(X_a) ),
file('theBenchmark.p',fact_12_one__power2) ).
fof(fact_13_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [X_1] : times_times(X_a,X_1,X_1) = power_power(X_a,X_1,number_number_of(nat,bit0(bit1(pls)))) ),
file('theBenchmark.p',fact_13_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
fof(fact_14_power2__eq__square,axiom,
! [X_a] :
( monoid_mult(X_a)
=> ! [A_1] : power_power(X_a,A_1,number_number_of(nat,bit0(bit1(pls)))) = times_times(X_a,A_1,A_1) ),
file('theBenchmark.p',fact_14_power2__eq__square) ).
fof(fact_15_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [X_1,N] : power_power(X_a,X_1,times_times(nat,number_number_of(nat,bit0(bit1(pls))),N)) = times_times(X_a,power_power(X_a,X_1,N),power_power(X_a,X_1,N)) ),
file('theBenchmark.p',fact_15_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J) ).
fof(fact_16_add__special_I2_J,axiom,
! [X_a] :
( number_ring(X_a)
=> ! [W] : plus_plus(X_a,one_one(X_a),number_number_of(X_a,W)) = number_number_of(X_a,plus_plus(int,bit1(pls),W)) ),
file('theBenchmark.p',fact_16_add__special_I2_J) ).
fof(fact_17_add__special_I3_J,axiom,
! [X_a] :
( number_ring(X_a)
=> ! [V] : plus_plus(X_a,number_number_of(X_a,V),one_one(X_a)) = number_number_of(X_a,plus_plus(int,V,bit1(pls))) ),
file('theBenchmark.p',fact_17_add__special_I3_J) ).
fof(fact_18_one__add__one__is__two,axiom,
! [X_a] :
( number_ring(X_a)
=> plus_plus(X_a,one_one(X_a),one_one(X_a)) = number_number_of(X_a,bit0(bit1(pls))) ),
file('theBenchmark.p',fact_18_one__add__one__is__two) ).
fof(fact_19__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,axiom,
~ ! [T_1] : plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) != times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),T_1),
file('theBenchmark.p',fact_19__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_) ).
fof(fact_20_zle__refl,axiom,
! [W] : ord_less_eq(int,W,W),
file('theBenchmark.p',fact_20_zle__refl) ).
fof(fact_21_zle__linear,axiom,
! [Z,W] :
( ord_less_eq(int,W,Z)
| ord_less_eq(int,Z,W) ),
file('theBenchmark.p',fact_21_zle__linear) ).
fof(fact_22_zless__le,axiom,
! [Z_1,W_1] :
( ord_less(int,Z_1,W_1)
<=> ( Z_1 != W_1
& ord_less_eq(int,Z_1,W_1) ) ),
file('theBenchmark.p',fact_22_zless__le) ).
fof(fact_23_zless__linear,axiom,
! [X_1,Y_1] :
( ord_less(int,Y_1,X_1)
| X_1 = Y_1
| ord_less(int,X_1,Y_1) ),
file('theBenchmark.p',fact_23_zless__linear) ).
fof(fact_24_zle__trans,axiom,
! [K_1,I,J] :
( ord_less_eq(int,I,J)
=> ( ord_less_eq(int,J,K_1)
=> ord_less_eq(int,I,K_1) ) ),
file('theBenchmark.p',fact_24_zle__trans) ).
fof(fact_25_zle__antisym,axiom,
! [Z,W] :
( ord_less_eq(int,Z,W)
=> ( ord_less_eq(int,W,Z)
=> Z = W ) ),
file('theBenchmark.p',fact_25_zle__antisym) ).
fof(fact_26_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [X_1,P,Q] : power_power(X_a,power_power(X_a,X_1,P),Q) = power_power(X_a,X_1,times_times(nat,P,Q)) ),
file('theBenchmark.p',fact_26_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J) ).
fof(fact_27_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [X_1] : power_power(X_a,X_1,one_one(nat)) = ti(X_a,X_1) ),
file('theBenchmark.p',fact_27_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J) ).
fof(fact_28_zpower__zpower,axiom,
! [X_1,Y_1,Z] : power_power(int,power_power(int,X_1,Y_1),Z) = power_power(int,X_1,times_times(nat,Y_1,Z)),
file('theBenchmark.p',fact_28_zpower__zpower) ).
fof(fact_29_le__number__of__eq__not__less,axiom,
! [X_a] :
( ( linorder(X_a)
& number(X_a) )
=> ! [V_2,W_1] :
( ord_less_eq(X_a,number_number_of(X_a,V_2),number_number_of(X_a,W_1))
<=> ~ ord_less(X_a,number_number_of(X_a,W_1),number_number_of(X_a,V_2)) ) ),
file('theBenchmark.p',fact_29_le__number__of__eq__not__less) ).
fof(fact_30_less__number__of,axiom,
! [X_a] :
( ( linordered_idom(X_a)
& number_ring(X_a) )
=> ! [X_2,Y_2] :
( ord_less(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2))
<=> ord_less(int,X_2,Y_2) ) ),
file('theBenchmark.p',fact_30_less__number__of) ).
fof(fact_31_le__number__of,axiom,
! [X_a] :
( ( linordered_idom(X_a)
& number_ring(X_a) )
=> ! [X_2,Y_2] :
( ord_less_eq(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2))
<=> ord_less_eq(int,X_2,Y_2) ) ),
file('theBenchmark.p',fact_31_le__number__of) ).
fof(fact_32_zadd__zless__mono,axiom,
! [Z_2,Z,W_2,W] :
( ord_less(int,W_2,W)
=> ( ord_less_eq(int,Z_2,Z)
=> ord_less(int,plus_plus(int,W_2,Z_2),plus_plus(int,W,Z)) ) ),
file('theBenchmark.p',fact_32_zadd__zless__mono) ).
fof(fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [X_1,P,Q] : times_times(X_a,power_power(X_a,X_1,P),power_power(X_a,X_1,Q)) = power_power(X_a,X_1,plus_plus(nat,P,Q)) ),
file('theBenchmark.p',fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J) ).
fof(fact_34_zpower__zadd__distrib,axiom,
! [X_1,Y_1,Z] : power_power(int,X_1,plus_plus(nat,Y_1,Z)) = times_times(int,power_power(int,X_1,Y_1),power_power(int,X_1,Z)),
file('theBenchmark.p',fact_34_zpower__zadd__distrib) ).
fof(fact_35_nat__mult__2,axiom,
! [Z] : times_times(nat,number_number_of(nat,bit0(bit1(pls))),Z) = plus_plus(nat,Z,Z),
file('theBenchmark.p',fact_35_nat__mult__2) ).
fof(fact_36_nat__mult__2__right,axiom,
! [Z] : times_times(nat,Z,number_number_of(nat,bit0(bit1(pls)))) = plus_plus(nat,Z,Z),
file('theBenchmark.p',fact_36_nat__mult__2__right) ).
fof(fact_37_nat__1__add__1,axiom,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
file('theBenchmark.p',fact_37_nat__1__add__1) ).
fof(fact_38_less__int__code_I16_J,axiom,
! [K1,K2] :
( ord_less(int,bit1(K1),bit1(K2))
<=> ord_less(int,K1,K2) ),
file('theBenchmark.p',fact_38_less__int__code_I16_J) ).
fof(fact_39_rel__simps_I17_J,axiom,
! [K,L] :
( ord_less(int,bit1(K),bit1(L))
<=> ord_less(int,K,L) ),
file('theBenchmark.p',fact_39_rel__simps_I17_J) ).
fof(fact_40_less__eq__int__code_I16_J,axiom,
! [K1,K2] :
( ord_less_eq(int,bit1(K1),bit1(K2))
<=> ord_less_eq(int,K1,K2) ),
file('theBenchmark.p',fact_40_less__eq__int__code_I16_J) ).
fof(fact_41_rel__simps_I34_J,axiom,
! [K,L] :
( ord_less_eq(int,bit1(K),bit1(L))
<=> ord_less_eq(int,K,L) ),
file('theBenchmark.p',fact_41_rel__simps_I34_J) ).
fof(fact_42_rel__simps_I2_J,axiom,
~ ord_less(int,pls,pls),
file('theBenchmark.p',fact_42_rel__simps_I2_J) ).
fof(fact_43_less__int__code_I13_J,axiom,
! [K1,K2] :
( ord_less(int,bit0(K1),bit0(K2))
<=> ord_less(int,K1,K2) ),
file('theBenchmark.p',fact_43_less__int__code_I13_J) ).
fof(fact_44_rel__simps_I14_J,axiom,
! [K,L] :
( ord_less(int,bit0(K),bit0(L))
<=> ord_less(int,K,L) ),
file('theBenchmark.p',fact_44_rel__simps_I14_J) ).
fof(fact_45_rel__simps_I19_J,axiom,
ord_less_eq(int,pls,pls),
file('theBenchmark.p',fact_45_rel__simps_I19_J) ).
fof(fact_46_less__eq__int__code_I13_J,axiom,
! [K1,K2] :
( ord_less_eq(int,bit0(K1),bit0(K2))
<=> ord_less_eq(int,K1,K2) ),
file('theBenchmark.p',fact_46_less__eq__int__code_I13_J) ).
fof(fact_47_rel__simps_I31_J,axiom,
! [K,L] :
( ord_less_eq(int,bit0(K),bit0(L))
<=> ord_less_eq(int,K,L) ),
file('theBenchmark.p',fact_47_rel__simps_I31_J) ).
fof(fact_48_less__number__of__int__code,axiom,
! [K,L] :
( ord_less(int,number_number_of(int,K),number_number_of(int,L))
<=> ord_less(int,K,L) ),
file('theBenchmark.p',fact_48_less__number__of__int__code) ).
fof(fact_49_less__eq__number__of__int__code,axiom,
! [K,L] :
( ord_less_eq(int,number_number_of(int,K),number_number_of(int,L))
<=> ord_less_eq(int,K,L) ),
file('theBenchmark.p',fact_49_less__eq__number__of__int__code) ).
fof(fact_50_zadd__strict__right__mono,axiom,
! [K_1,I,J] :
( ord_less(int,I,J)
=> ord_less(int,plus_plus(int,I,K_1),plus_plus(int,J,K_1)) ),
file('theBenchmark.p',fact_50_zadd__strict__right__mono) ).
fof(fact_51_zadd__left__mono,axiom,
! [K_1,I,J] :
( ord_less_eq(int,I,J)
=> ord_less_eq(int,plus_plus(int,K_1,I),plus_plus(int,K_1,J)) ),
file('theBenchmark.p',fact_51_zadd__left__mono) ).
fof(fact_52_add__nat__number__of,axiom,
! [V_1,V] :
( ( ~ ord_less(int,V,pls)
=> ( ( ~ ord_less(int,V_1,pls)
=> plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,plus_plus(int,V,V_1)) )
& ( ord_less(int,V_1,pls)
=> plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,V) ) ) )
& ( ord_less(int,V,pls)
=> plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,V_1) ) ),
file('theBenchmark.p',fact_52_add__nat__number__of) ).
fof(fact_53_nat__numeral__1__eq__1,axiom,
number_number_of(nat,bit1(pls)) = one_one(nat),
file('theBenchmark.p',fact_53_nat__numeral__1__eq__1) ).
fof(fact_54_Numeral1__eq1__nat,axiom,
one_one(nat) = number_number_of(nat,bit1(pls)),
file('theBenchmark.p',fact_54_Numeral1__eq1__nat) ).
fof(fact_55_rel__simps_I29_J,axiom,
! [K] :
( ord_less_eq(int,bit1(K),pls)
<=> ord_less(int,K,pls) ),
file('theBenchmark.p',fact_55_rel__simps_I29_J) ).
fof(fact_56_rel__simps_I5_J,axiom,
! [K] :
( ord_less(int,pls,bit1(K))
<=> ord_less_eq(int,pls,K) ),
file('theBenchmark.p',fact_56_rel__simps_I5_J) ).
fof(fact_57_less__eq__int__code_I15_J,axiom,
! [K1,K2] :
( ord_less_eq(int,bit1(K1),bit0(K2))
<=> ord_less(int,K1,K2) ),
file('theBenchmark.p',fact_57_less__eq__int__code_I15_J) ).
fof(fact_58_rel__simps_I33_J,axiom,
! [K,L] :
( ord_less_eq(int,bit1(K),bit0(L))
<=> ord_less(int,K,L) ),
file('theBenchmark.p',fact_58_rel__simps_I33_J) ).
fof(fact_59_less__int__code_I14_J,axiom,
! [K1,K2] :
( ord_less(int,bit0(K1),bit1(K2))
<=> ord_less_eq(int,K1,K2) ),
file('theBenchmark.p',fact_59_less__int__code_I14_J) ).
fof(fact_60_rel__simps_I15_J,axiom,
! [K,L] :
( ord_less(int,bit0(K),bit1(L))
<=> ord_less_eq(int,K,L) ),
file('theBenchmark.p',fact_60_rel__simps_I15_J) ).
fof(fact_61_zless__imp__add1__zle,axiom,
! [W,Z] :
( ord_less(int,W,Z)
=> ord_less_eq(int,plus_plus(int,W,one_one(int)),Z) ),
file('theBenchmark.p',fact_61_zless__imp__add1__zle) ).
fof(fact_62_add1__zle__eq,axiom,
! [W_1,Z_1] :
( ord_less_eq(int,plus_plus(int,W_1,one_one(int)),Z_1)
<=> ord_less(int,W_1,Z_1) ),
file('theBenchmark.p',fact_62_add1__zle__eq) ).
fof(fact_63_zle__add1__eq__le,axiom,
! [W_1,Z_1] :
( ord_less(int,W_1,plus_plus(int,Z_1,one_one(int)))
<=> ord_less_eq(int,W_1,Z_1) ),
file('theBenchmark.p',fact_63_zle__add1__eq__le) ).
fof(fact_64_zprime__2,axiom,
zprime(number_number_of(int,bit0(bit1(pls)))),
file('theBenchmark.p',fact_64_zprime__2) ).
fof(fact_65_is__mult__sum2sq,axiom,
! [Y_1,X_1] :
( twoSqu33214720sum2sq(X_1)
=> ( twoSqu33214720sum2sq(Y_1)
=> twoSqu33214720sum2sq(times_times(int,X_1,Y_1)) ) ),
file('theBenchmark.p',fact_65_is__mult__sum2sq) ).
fof(fact_66_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,times_times(X_a,Lx,Rx),times_times(X_a,Ly,Ry)) ),
file('theBenchmark.p',fact_66_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J) ).
fof(fact_67_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,Rx,times_times(X_a,times_times(X_a,Lx,Ly),Ry)) ),
file('theBenchmark.p',fact_67_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J) ).
fof(fact_68_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,Lx,times_times(X_a,Ly,times_times(X_a,Rx,Ry))) ),
file('theBenchmark.p',fact_68_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J) ).
fof(fact_69_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Ly,Rx] : times_times(X_a,times_times(X_a,Lx,Ly),Rx) = times_times(X_a,times_times(X_a,Lx,Rx),Ly) ),
file('theBenchmark.p',fact_69_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J) ).
fof(fact_70_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Ly,Rx] : times_times(X_a,times_times(X_a,Lx,Ly),Rx) = times_times(X_a,Lx,times_times(X_a,Ly,Rx)) ),
file('theBenchmark.p',fact_70_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
fof(fact_71_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Rx,Ry] : times_times(X_a,Lx,times_times(X_a,Rx,Ry)) = times_times(X_a,times_times(X_a,Lx,Rx),Ry) ),
file('theBenchmark.p',fact_71_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J) ).
fof(fact_72_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [Lx,Rx,Ry] : times_times(X_a,Lx,times_times(X_a,Rx,Ry)) = times_times(X_a,Rx,times_times(X_a,Lx,Ry)) ),
file('theBenchmark.p',fact_72_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(fact_73_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,B] : times_times(X_a,A_1,B) = times_times(X_a,B,A_1) ),
file('theBenchmark.p',fact_73_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(fact_74_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,B,C,D] : plus_plus(X_a,plus_plus(X_a,A_1,B),plus_plus(X_a,C,D)) = plus_plus(X_a,plus_plus(X_a,A_1,C),plus_plus(X_a,B,D)) ),
file('theBenchmark.p',fact_74_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J) ).
fof(fact_75_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,B,C] : plus_plus(X_a,plus_plus(X_a,A_1,B),C) = plus_plus(X_a,plus_plus(X_a,A_1,C),B) ),
file('theBenchmark.p',fact_75_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J) ).
fof(fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,B,C] : plus_plus(X_a,plus_plus(X_a,A_1,B),C) = plus_plus(X_a,A_1,plus_plus(X_a,B,C)) ),
file('theBenchmark.p',fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
fof(fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,C,D] : plus_plus(X_a,A_1,plus_plus(X_a,C,D)) = plus_plus(X_a,plus_plus(X_a,A_1,C),D) ),
file('theBenchmark.p',fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
fof(fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,C,D] : plus_plus(X_a,A_1,plus_plus(X_a,C,D)) = plus_plus(X_a,C,plus_plus(X_a,A_1,D)) ),
file('theBenchmark.p',fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
! [X_a] :
( comm_semiring_1(X_a)
=> ! [A_1,C] : plus_plus(X_a,A_1,C) = plus_plus(X_a,C,A_1) ),
file('theBenchmark.p',fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(fact_80_eq__number__of,axiom,
! [X_a] :
( ( ring_char_0(X_a)
& number_ring(X_a) )
=> ! [X_2,Y_2] :
( number_number_of(X_a,X_2) = number_number_of(X_a,Y_2)
<=> X_2 = Y_2 ) ),
file('theBenchmark.p',fact_80_eq__number__of) ).
fof(fact_81_number__of__reorient,axiom,
! [X_a] :
( number(X_a)
=> ! [W_1,X_2] :
( number_number_of(X_a,W_1) = ti(X_a,X_2)
<=> ti(X_a,X_2) = number_number_of(X_a,W_1) ) ),
file('theBenchmark.p',fact_81_number__of__reorient) ).
fof(fact_82_rel__simps_I51_J,axiom,
! [K,L] :
( bit1(K) = bit1(L)
<=> K = L ),
file('theBenchmark.p',fact_82_rel__simps_I51_J) ).
fof(fact_83_rel__simps_I48_J,axiom,
! [K,L] :
( bit0(K) = bit0(L)
<=> K = L ),
file('theBenchmark.p',fact_83_rel__simps_I48_J) ).
fof(fact_84_zmult__assoc,axiom,
! [Z1,Z2,Z3] : times_times(int,times_times(int,Z1,Z2),Z3) = times_times(int,Z1,times_times(int,Z2,Z3)),
file('theBenchmark.p',fact_84_zmult__assoc) ).
fof(fact_85_zmult__commute,axiom,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
file('theBenchmark.p',fact_85_zmult__commute) ).
fof(fact_86_number__of__is__id,axiom,
! [K_1] : number_number_of(int,K_1) = K_1,
file('theBenchmark.p',fact_86_number__of__is__id) ).
fof(fact_87_zadd__assoc,axiom,
! [Z1,Z2,Z3] : plus_plus(int,plus_plus(int,Z1,Z2),Z3) = plus_plus(int,Z1,plus_plus(int,Z2,Z3)),
file('theBenchmark.p',fact_87_zadd__assoc) ).
fof(fact_88_zadd__left__commute,axiom,
! [X_1,Y_1,Z] : plus_plus(int,X_1,plus_plus(int,Y_1,Z)) = plus_plus(int,Y_1,plus_plus(int,X_1,Z)),
file('theBenchmark.p',fact_88_zadd__left__commute) ).
fof(fact_89_zadd__commute,axiom,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
file('theBenchmark.p',fact_89_zadd__commute) ).
fof(fact_90_rel__simps_I12_J,axiom,
! [K] :
( ord_less(int,bit1(K),pls)
<=> ord_less(int,K,pls) ),
file('theBenchmark.p',fact_90_rel__simps_I12_J) ).
fof(fact_91_less__int__code_I15_J,axiom,
! [K1,K2] :
( ord_less(int,bit1(K1),bit0(K2))
<=> ord_less(int,K1,K2) ),
file('theBenchmark.p',fact_91_less__int__code_I15_J) ).
fof(fact_92_rel__simps_I16_J,axiom,
! [K,L] :
( ord_less(int,bit1(K),bit0(L))
<=> ord_less(int,K,L) ),
file('theBenchmark.p',fact_92_rel__simps_I16_J) ).
fof(fact_93_rel__simps_I10_J,axiom,
! [K] :
( ord_less(int,bit0(K),pls)
<=> ord_less(int,K,pls) ),
file('theBenchmark.p',fact_93_rel__simps_I10_J) ).
fof(fact_94_rel__simps_I4_J,axiom,
! [K] :
( ord_less(int,pls,bit0(K))
<=> ord_less(int,pls,K) ),
file('theBenchmark.p',fact_94_rel__simps_I4_J) ).
fof(fact_95_rel__simps_I22_J,axiom,
! [K] :
( ord_less_eq(int,pls,bit1(K))
<=> ord_less_eq(int,pls,K) ),
file('theBenchmark.p',fact_95_rel__simps_I22_J) ).
fof(fact_96_less__eq__int__code_I14_J,axiom,
! [K1,K2] :
( ord_less_eq(int,bit0(K1),bit1(K2))
<=> ord_less_eq(int,K1,K2) ),
file('theBenchmark.p',fact_96_less__eq__int__code_I14_J) ).
fof(fact_97_rel__simps_I32_J,axiom,
! [K,L] :
( ord_less_eq(int,bit0(K),bit1(L))
<=> ord_less_eq(int,K,L) ),
file('theBenchmark.p',fact_97_rel__simps_I32_J) ).
fof(arity_Int_Oint___Rings_Olinordered__idom,axiom,
linordered_idom(int),
file('theBenchmark.p',arity_Int_Oint___Rings_Olinordered__idom) ).
fof(arity_Int_Oint___Rings_Ocomm__semiring__1,axiom,
comm_semiring_1(int),
file('theBenchmark.p',arity_Int_Oint___Rings_Ocomm__semiring__1) ).
fof(arity_Int_Oint___Int_Onumber__semiring,axiom,
number_semiring(int),
file('theBenchmark.p',arity_Int_Oint___Int_Onumber__semiring) ).
fof(arity_Int_Oint___Orderings_Olinorder,axiom,
linorder(int),
file('theBenchmark.p',arity_Int_Oint___Orderings_Olinorder) ).
fof(arity_Int_Oint___Groups_Omonoid__mult,axiom,
monoid_mult(int),
file('theBenchmark.p',arity_Int_Oint___Groups_Omonoid__mult) ).
fof(arity_Int_Oint___Rings_Osemiring__1,axiom,
semiring_1(int),
file('theBenchmark.p',arity_Int_Oint___Rings_Osemiring__1) ).
fof(arity_Int_Oint___Int_Oring__char__0,axiom,
ring_char_0(int),
file('theBenchmark.p',arity_Int_Oint___Int_Oring__char__0) ).
fof(arity_Int_Oint___Int_Onumber__ring,axiom,
number_ring(int),
file('theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
fof(arity_Int_Oint___Int_Onumber,axiom,
number(int),
file('theBenchmark.p',arity_Int_Oint___Int_Onumber) ).
fof(arity_Nat_Onat___Rings_Ocomm__semiring__1,axiom,
comm_semiring_1(nat),
file('theBenchmark.p',arity_Nat_Onat___Rings_Ocomm__semiring__1) ).
fof(arity_Nat_Onat___Int_Onumber__semiring,axiom,
number_semiring(nat),
file('theBenchmark.p',arity_Nat_Onat___Int_Onumber__semiring) ).
fof(arity_Nat_Onat___Orderings_Olinorder,axiom,
linorder(nat),
file('theBenchmark.p',arity_Nat_Onat___Orderings_Olinorder) ).
fof(arity_Nat_Onat___Groups_Omonoid__mult,axiom,
monoid_mult(nat),
file('theBenchmark.p',arity_Nat_Onat___Groups_Omonoid__mult) ).
fof(arity_Nat_Onat___Rings_Osemiring__1,axiom,
semiring_1(nat),
file('theBenchmark.p',arity_Nat_Onat___Rings_Osemiring__1) ).
fof(arity_Nat_Onat___Int_Onumber,axiom,
number(nat),
file('theBenchmark.p',arity_Nat_Onat___Int_Onumber) ).
fof(help_ti_idem,axiom,
! [T,A] : ti(T,ti(T,A)) = ti(T,A),
file('theBenchmark.p',help_ti_idem) ).
fof(conj_0,conjecture,
? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
file('theBenchmark.p',conj_0) ).
fof(f_1_1,plain,
! [X_a] :
( ti(X_a,one_one(X_a)) = one_one(X_a)
| ~ semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Oone__class_Oone_res]) ).
fof(f_1_2,plain,
! [U_0] :
( ti(U_0,one_one(U_0)) = one_one(U_0)
| ~ semiring_1(U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( ti(U_0,one_one(U_0)) = one_one(U_0)
| ~ semiring_1(U_0) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [B_1,B_2,X_a] :
( plus_plus(X_a,ti(X_a,B_1),B_2) = plus_plus(X_a,B_1,B_2)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Oplus__class_Oplus_arg1]) ).
fof(f_2_2,plain,
! [U_3,U_2,U_1] :
( plus_plus(U_1,ti(U_1,U_3),U_2) = plus_plus(U_1,U_3,U_2)
| ~ comm_semiring_1(U_1) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
( plus_plus(U_1,ti(U_1,U_3),U_2) = plus_plus(U_1,U_3,U_2)
| ~ comm_semiring_1(U_1) ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [B_1,B_2,X_a] :
( plus_plus(X_a,B_1,ti(X_a,B_2)) = plus_plus(X_a,B_1,B_2)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Oplus__class_Oplus_arg2]) ).
fof(f_3_2,plain,
! [U_6,U_5,U_4] :
( plus_plus(U_4,U_6,ti(U_4,U_5)) = plus_plus(U_4,U_6,U_5)
| ~ comm_semiring_1(U_4) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( plus_plus(U_4,U_6,ti(U_4,U_5)) = plus_plus(U_4,U_6,U_5)
| ~ comm_semiring_1(U_4) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [B_1,B_2,X_a] :
( ti(X_a,plus_plus(X_a,B_1,B_2)) = plus_plus(X_a,B_1,B_2)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Oplus__class_Oplus_res]) ).
fof(f_4_2,plain,
! [U_9,U_8,U_7] :
( ti(U_7,plus_plus(U_7,U_9,U_8)) = plus_plus(U_7,U_9,U_8)
| ~ comm_semiring_1(U_7) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( ti(U_7,plus_plus(U_7,U_9,U_8)) = plus_plus(U_7,U_9,U_8)
| ~ comm_semiring_1(U_7) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [B_1,B_2,X_a] :
( times_times(X_a,ti(X_a,B_1),B_2) = times_times(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Otimes__class_Otimes_arg1]) ).
fof(f_5_2,plain,
! [U_12,U_11,U_10] :
( times_times(U_10,ti(U_10,U_12),U_11) = times_times(U_10,U_12,U_11)
| ~ monoid_mult(U_10) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( times_times(U_10,ti(U_10,U_12),U_11) = times_times(U_10,U_12,U_11)
| ~ monoid_mult(U_10) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [B_1,B_2,X_a] :
( times_times(X_a,B_1,ti(X_a,B_2)) = times_times(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Otimes__class_Otimes_arg2]) ).
fof(f_6_2,plain,
! [U_15,U_14,U_13] :
( times_times(U_13,U_15,ti(U_13,U_14)) = times_times(U_13,U_15,U_14)
| ~ monoid_mult(U_13) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( times_times(U_13,U_15,ti(U_13,U_14)) = times_times(U_13,U_15,U_14)
| ~ monoid_mult(U_13) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [B_1,B_2,X_a] :
( ti(X_a,times_times(X_a,B_1,B_2)) = times_times(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Groups_Otimes__class_Otimes_res]) ).
fof(f_7_2,plain,
! [U_18,U_17,U_16] :
( ti(U_16,times_times(U_16,U_18,U_17)) = times_times(U_16,U_18,U_17)
| ~ monoid_mult(U_16) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( ti(U_16,times_times(U_16,U_18,U_17)) = times_times(U_16,U_18,U_17)
| ~ monoid_mult(U_16) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [X_a] : ti(X_a,undefined(X_a)) = undefined(X_a),
inference(fof_nnf,[status(thm)],[tsy_c_HOL_Oundefined_res]) ).
fof(f_8_2,plain,
! [U_19] : ti(U_19,undefined(U_19)) = undefined(U_19),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
ti(U_19,undefined(U_19)) = undefined(U_19),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [B_1] :
( ( zprime(ti(int,B_1))
| ~ zprime(B_1) )
& ( zprime(B_1)
| ~ zprime(ti(int,B_1)) ) ),
inference(fof_nnf,[status(thm)],[tsy_c_IntPrimes_Ozprime_arg1]) ).
fof(f_9_2,plain,
! [U_20] :
( ( zprime(ti(int,U_20))
| ~ zprime(U_20) )
& ( zprime(U_20)
| ~ zprime(ti(int,U_20)) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_22] :
( zprime(ti(int,U_22))
| ~ zprime(U_22) )
& ! [U_21] :
( zprime(U_21)
| ~ zprime(ti(int,U_21)) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( zprime(U_21)
| ~ zprime(ti(int,U_21)) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( zprime(ti(int,U_22))
| ~ zprime(U_22) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [B_1] : bit0(ti(int,B_1)) = bit0(B_1),
inference(fof_nnf,[status(thm)],[tsy_c_Int_OBit0_arg1]) ).
fof(f_10_2,plain,
! [U_23] : bit0(ti(int,U_23)) = bit0(U_23),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
bit0(ti(int,U_23)) = bit0(U_23),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [B_1] : ti(int,bit0(B_1)) = bit0(B_1),
inference(fof_nnf,[status(thm)],[tsy_c_Int_OBit0_res]) ).
fof(f_11_2,plain,
! [U_24] : ti(int,bit0(U_24)) = bit0(U_24),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
ti(int,bit0(U_24)) = bit0(U_24),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [B_1] : bit1(ti(int,B_1)) = bit1(B_1),
inference(fof_nnf,[status(thm)],[tsy_c_Int_OBit1_arg1]) ).
fof(f_12_2,plain,
! [U_25] : bit1(ti(int,U_25)) = bit1(U_25),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
bit1(ti(int,U_25)) = bit1(U_25),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [B_1] : ti(int,bit1(B_1)) = bit1(B_1),
inference(fof_nnf,[status(thm)],[tsy_c_Int_OBit1_res]) ).
fof(f_13_2,plain,
! [U_26] : ti(int,bit1(U_26)) = bit1(U_26),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
ti(int,bit1(U_26)) = bit1(U_26),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
ti(int,pls) = pls,
inference(fof_nnf,[status(thm)],[tsy_c_Int_OPls_res]) ).
cnf(f_14_2,plain,
ti(int,pls) = pls,
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_15_1,plain,
! [B_1,X_a] :
( number_number_of(X_a,ti(int,B_1)) = number_number_of(X_a,B_1)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Int_Onumber__class_Onumber__of_arg1]) ).
fof(f_15_2,plain,
! [U_28,U_27] :
( number_number_of(U_27,ti(int,U_28)) = number_number_of(U_27,U_28)
| ~ number(U_27) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( number_number_of(U_27,ti(int,U_28)) = number_number_of(U_27,U_28)
| ~ number(U_27) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [B_1,X_a] :
( ti(X_a,number_number_of(X_a,B_1)) = number_number_of(X_a,B_1)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Int_Onumber__class_Onumber__of_res]) ).
fof(f_16_2,plain,
! [U_30,U_29] :
( ti(U_29,number_number_of(U_29,U_30)) = number_number_of(U_29,U_30)
| ~ number(U_29) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
cnf(f_16_3,plain,
( ti(U_29,number_number_of(U_29,U_30)) = number_number_of(U_29,U_30)
| ~ number(U_29) ),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
! [B_1,B_2,X_a] :
( ( ( ord_less(X_a,ti(X_a,B_1),B_2)
| ~ ord_less(X_a,B_1,B_2) )
& ( ord_less(X_a,B_1,B_2)
| ~ ord_less(X_a,ti(X_a,B_1),B_2) ) )
| ~ linorder(X_a)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Orderings_Oord__class_Oless_arg1]) ).
fof(f_17_2,plain,
! [U_33,U_32,U_31] :
( ( ( ord_less(U_31,ti(U_31,U_33),U_32)
| ~ ord_less(U_31,U_33,U_32) )
& ( ord_less(U_31,U_33,U_32)
| ~ ord_less(U_31,ti(U_31,U_33),U_32) ) )
| ~ linorder(U_31)
| ~ number(U_31) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( ord_less(U_31,U_33,U_32)
| ~ ord_less(U_31,ti(U_31,U_33),U_32)
| ~ linorder(U_31)
| ~ number(U_31) ),
inference(clausify,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( ord_less(U_31,ti(U_31,U_33),U_32)
| ~ ord_less(U_31,U_33,U_32)
| ~ linorder(U_31)
| ~ number(U_31) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [B_1,B_2,X_a] :
( ( ( ord_less(X_a,B_1,ti(X_a,B_2))
| ~ ord_less(X_a,B_1,B_2) )
& ( ord_less(X_a,B_1,B_2)
| ~ ord_less(X_a,B_1,ti(X_a,B_2)) ) )
| ~ linorder(X_a)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Orderings_Oord__class_Oless_arg2]) ).
fof(f_18_2,plain,
! [U_36,U_35,U_34] :
( ( ( ord_less(U_34,U_36,ti(U_34,U_35))
| ~ ord_less(U_34,U_36,U_35) )
& ( ord_less(U_34,U_36,U_35)
| ~ ord_less(U_34,U_36,ti(U_34,U_35)) ) )
| ~ linorder(U_34)
| ~ number(U_34) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( ord_less(U_34,U_36,U_35)
| ~ ord_less(U_34,U_36,ti(U_34,U_35))
| ~ linorder(U_34)
| ~ number(U_34) ),
inference(clausify,[status(thm)],[f_18_2]) ).
cnf(f_18_4,plain,
( ord_less(U_34,U_36,ti(U_34,U_35))
| ~ ord_less(U_34,U_36,U_35)
| ~ linorder(U_34)
| ~ number(U_34) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [B_1,B_2,X_a] :
( ( ( ord_less_eq(X_a,ti(X_a,B_1),B_2)
| ~ ord_less_eq(X_a,B_1,B_2) )
& ( ord_less_eq(X_a,B_1,B_2)
| ~ ord_less_eq(X_a,ti(X_a,B_1),B_2) ) )
| ~ linorder(X_a)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Orderings_Oord__class_Oless__eq_arg1]) ).
fof(f_19_2,plain,
! [U_39,U_38,U_37] :
( ( ( ord_less_eq(U_37,ti(U_37,U_39),U_38)
| ~ ord_less_eq(U_37,U_39,U_38) )
& ( ord_less_eq(U_37,U_39,U_38)
| ~ ord_less_eq(U_37,ti(U_37,U_39),U_38) ) )
| ~ linorder(U_37)
| ~ number(U_37) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( ord_less_eq(U_37,U_39,U_38)
| ~ ord_less_eq(U_37,ti(U_37,U_39),U_38)
| ~ linorder(U_37)
| ~ number(U_37) ),
inference(clausify,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( ord_less_eq(U_37,ti(U_37,U_39),U_38)
| ~ ord_less_eq(U_37,U_39,U_38)
| ~ linorder(U_37)
| ~ number(U_37) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [B_1,B_2,X_a] :
( ( ( ord_less_eq(X_a,B_1,ti(X_a,B_2))
| ~ ord_less_eq(X_a,B_1,B_2) )
& ( ord_less_eq(X_a,B_1,B_2)
| ~ ord_less_eq(X_a,B_1,ti(X_a,B_2)) ) )
| ~ linorder(X_a)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Orderings_Oord__class_Oless__eq_arg2]) ).
fof(f_20_2,plain,
! [U_42,U_41,U_40] :
( ( ( ord_less_eq(U_40,U_42,ti(U_40,U_41))
| ~ ord_less_eq(U_40,U_42,U_41) )
& ( ord_less_eq(U_40,U_42,U_41)
| ~ ord_less_eq(U_40,U_42,ti(U_40,U_41)) ) )
| ~ linorder(U_40)
| ~ number(U_40) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( ord_less_eq(U_40,U_42,U_41)
| ~ ord_less_eq(U_40,U_42,ti(U_40,U_41))
| ~ linorder(U_40)
| ~ number(U_40) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( ord_less_eq(U_40,U_42,ti(U_40,U_41))
| ~ ord_less_eq(U_40,U_42,U_41)
| ~ linorder(U_40)
| ~ number(U_40) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [B_1,B_2,X_a] :
( power_power(X_a,ti(X_a,B_1),B_2) = power_power(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Power_Opower__class_Opower_arg1]) ).
fof(f_21_2,plain,
! [U_45,U_44,U_43] :
( power_power(U_43,ti(U_43,U_45),U_44) = power_power(U_43,U_45,U_44)
| ~ monoid_mult(U_43) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( power_power(U_43,ti(U_43,U_45),U_44) = power_power(U_43,U_45,U_44)
| ~ monoid_mult(U_43) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [B_1,B_2,X_a] :
( power_power(X_a,B_1,ti(nat,B_2)) = power_power(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Power_Opower__class_Opower_arg2]) ).
fof(f_22_2,plain,
! [U_48,U_47,U_46] :
( power_power(U_46,U_48,ti(nat,U_47)) = power_power(U_46,U_48,U_47)
| ~ monoid_mult(U_46) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( power_power(U_46,U_48,ti(nat,U_47)) = power_power(U_46,U_48,U_47)
| ~ monoid_mult(U_46) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [B_1,B_2,X_a] :
( ti(X_a,power_power(X_a,B_1,B_2)) = power_power(X_a,B_1,B_2)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[tsy_c_Power_Opower__class_Opower_res]) ).
fof(f_23_2,plain,
! [U_51,U_50,U_49] :
( ti(U_49,power_power(U_49,U_51,U_50)) = power_power(U_49,U_51,U_50)
| ~ monoid_mult(U_49) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( ti(U_49,power_power(U_49,U_51,U_50)) = power_power(U_49,U_51,U_50)
| ~ monoid_mult(U_49) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [B_1] :
( ( twoSqu33214720sum2sq(ti(int,B_1))
| ~ twoSqu33214720sum2sq(B_1) )
& ( twoSqu33214720sum2sq(B_1)
| ~ twoSqu33214720sum2sq(ti(int,B_1)) ) ),
inference(fof_nnf,[status(thm)],[tsy_c_TwoSquares__Mirabelle__vsgmegnqdl_Ois__sum2sq_arg1]) ).
fof(f_24_2,plain,
! [U_52] :
( ( twoSqu33214720sum2sq(ti(int,U_52))
| ~ twoSqu33214720sum2sq(U_52) )
& ( twoSqu33214720sum2sq(U_52)
| ~ twoSqu33214720sum2sq(ti(int,U_52)) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_54] :
( twoSqu33214720sum2sq(ti(int,U_54))
| ~ twoSqu33214720sum2sq(U_54) )
& ! [U_53] :
( twoSqu33214720sum2sq(U_53)
| ~ twoSqu33214720sum2sq(ti(int,U_53)) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
cnf(f_24_4,plain,
( twoSqu33214720sum2sq(U_53)
| ~ twoSqu33214720sum2sq(ti(int,U_53)) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( twoSqu33214720sum2sq(ti(int,U_54))
| ~ twoSqu33214720sum2sq(U_54) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
ti(int,m) = m,
inference(fof_nnf,[status(thm)],[tsy_v_m_res]) ).
cnf(f_25_2,plain,
ti(int,m) = m,
inference(clausify,[status(thm)],[f_25_1]) ).
fof(f_26_1,plain,
ti(int,s) = s,
inference(fof_nnf,[status(thm)],[tsy_v_s_____res]) ).
cnf(f_26_2,plain,
ti(int,s) = s,
inference(clausify,[status(thm)],[f_26_1]) ).
fof(f_27_1,plain,
ti(int,t) = t,
inference(fof_nnf,[status(thm)],[tsy_v_t_____res]) ).
cnf(f_27_2,plain,
ti(int,t) = t,
inference(clausify,[status(thm)],[f_27_1]) ).
fof(f_28_1,plain,
ord_less_eq(int,one_one(int),t),
inference(fof_nnf,[status(thm)],[fact_0_tpos]) ).
cnf(f_28_2,plain,
ord_less_eq(int,one_one(int),t),
inference(clausify,[status(thm)],[f_28_1]) ).
fof(f_29_1,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| t != one_one(int) ),
inference(fof_nnf,[status(thm)],[fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(f_29_2,plain,
( ? [U_56,U_55] : plus_plus(int,power_power(int,U_56,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_55,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| t != one_one(int) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ? [U_55] : plus_plus(int,power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_55,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| t != one_one(int) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_56,sK1)],[f_29_2]) ).
fof(f_29_4,plain,
( plus_plus(int,power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK2,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| t != one_one(int) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_55,sK2)],[f_29_3]) ).
cnf(f_29_5,plain,
( plus_plus(int,power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK2,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| t != one_one(int) ),
inference(clausify,[status(thm)],[f_29_4]) ).
fof(f_30_1,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(fof_nnf,[status(thm)],[fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(f_30_2,plain,
( ? [U_58,U_57] : plus_plus(int,power_power(int,U_58,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_57,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
( ? [U_57] : plus_plus(int,power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_57,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_58,sK3)],[f_30_2]) ).
fof(f_30_4,plain,
( plus_plus(int,power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK4,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_57,sK4)],[f_30_3]) ).
cnf(f_30_5,plain,
( plus_plus(int,power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK4,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(clausify,[status(thm)],[f_30_4]) ).
fof(f_31_1,plain,
ord_less(int,t,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
inference(fof_nnf,[status(thm)],[fact_3_t__l__p]) ).
cnf(f_31_2,plain,
ord_less(int,t,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
inference(clausify,[status(thm)],[f_31_1]) ).
fof(f_32_1,plain,
zprime(plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
inference(fof_nnf,[status(thm)],[fact_4_p]) ).
cnf(f_32_2,plain,
zprime(plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))),
inference(clausify,[status(thm)],[f_32_1]) ).
fof(f_33_1,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
inference(fof_nnf,[status(thm)],[fact_5_t]) ).
cnf(f_33_2,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
inference(clausify,[status(thm)],[f_33_1]) ).
fof(f_34_1,plain,
twoSqu33214720sum2sq(times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t)),
inference(fof_nnf,[status(thm)],[fact_6_qf1pt]) ).
cnf(f_34_2,plain,
twoSqu33214720sum2sq(times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t)),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
! [A_1,B] : power_power(int,plus_plus(int,A_1,B),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,plus_plus(int,power_power(int,A_1,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),A_1),B)),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))),
inference(fof_nnf,[status(thm)],[fact_7_zadd__power2]) ).
fof(f_35_2,plain,
! [U_60,U_59] : power_power(int,plus_plus(int,U_60,U_59),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,plus_plus(int,power_power(int,U_60,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),U_60),U_59)),power_power(int,U_59,number_number_of(nat,bit0(bit1(pls))))),
inference(variable_rename,[status(thm)],[f_35_1]) ).
cnf(f_35_3,plain,
power_power(int,plus_plus(int,U_60,U_59),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,plus_plus(int,power_power(int,U_60,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),U_60),U_59)),power_power(int,U_59,number_number_of(nat,bit0(bit1(pls))))),
inference(clausify,[status(thm)],[f_35_2]) ).
fof(f_36_1,plain,
! [A_1,B] : power_power(int,plus_plus(int,A_1,B),number_number_of(nat,bit1(bit1(pls)))) = plus_plus(int,plus_plus(int,plus_plus(int,power_power(int,A_1,number_number_of(nat,bit1(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),power_power(int,A_1,number_number_of(nat,bit0(bit1(pls))))),B)),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),A_1),power_power(int,B,number_number_of(nat,bit0(bit1(pls)))))),power_power(int,B,number_number_of(nat,bit1(bit1(pls))))),
inference(fof_nnf,[status(thm)],[fact_8_zadd__power3]) ).
fof(f_36_2,plain,
! [U_62,U_61] : power_power(int,plus_plus(int,U_62,U_61),number_number_of(nat,bit1(bit1(pls)))) = plus_plus(int,plus_plus(int,plus_plus(int,power_power(int,U_62,number_number_of(nat,bit1(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),power_power(int,U_62,number_number_of(nat,bit0(bit1(pls))))),U_61)),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),U_62),power_power(int,U_61,number_number_of(nat,bit0(bit1(pls)))))),power_power(int,U_61,number_number_of(nat,bit1(bit1(pls))))),
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
power_power(int,plus_plus(int,U_62,U_61),number_number_of(nat,bit1(bit1(pls)))) = plus_plus(int,plus_plus(int,plus_plus(int,power_power(int,U_62,number_number_of(nat,bit1(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),power_power(int,U_62,number_number_of(nat,bit0(bit1(pls))))),U_61)),times_times(int,times_times(int,number_number_of(int,bit1(bit1(pls))),U_62),power_power(int,U_61,number_number_of(nat,bit0(bit1(pls)))))),power_power(int,U_61,number_number_of(nat,bit1(bit1(pls))))),
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [X_a] :
( ! [X_1,Y_1] : power_power(X_a,plus_plus(X_a,X_1,Y_1),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(X_a,plus_plus(X_a,power_power(X_a,X_1,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Y_1,number_number_of(nat,bit0(bit1(pls))))),times_times(X_a,times_times(X_a,number_number_of(X_a,bit0(bit1(pls))),X_1),Y_1))
| ~ number_semiring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_9_power2__sum]) ).
fof(f_37_2,plain,
! [U_65] :
( ! [U_64,U_63] : power_power(U_65,plus_plus(U_65,U_64,U_63),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(U_65,plus_plus(U_65,power_power(U_65,U_64,number_number_of(nat,bit0(bit1(pls)))),power_power(U_65,U_63,number_number_of(nat,bit0(bit1(pls))))),times_times(U_65,times_times(U_65,number_number_of(U_65,bit0(bit1(pls))),U_64),U_63))
| ~ number_semiring(U_65) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
( power_power(U_65,plus_plus(U_65,U_64,U_63),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(U_65,plus_plus(U_65,power_power(U_65,U_64,number_number_of(nat,bit0(bit1(pls)))),power_power(U_65,U_63,number_number_of(nat,bit0(bit1(pls))))),times_times(U_65,times_times(U_65,number_number_of(U_65,bit0(bit1(pls))),U_64),U_63))
| ~ number_semiring(U_65) ),
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_38_1,plain,
! [X_b] :
( ! [W] : power_power(X_b,number_number_of(X_b,W),number_number_of(nat,bit0(bit1(pls)))) = times_times(X_b,number_number_of(X_b,W),number_number_of(X_b,W))
| ~ number(X_b)
| ~ monoid_mult(X_b) ),
inference(fof_nnf,[status(thm)],[fact_10_power2__eq__square__number__of]) ).
fof(f_38_2,plain,
! [U_67] :
( ! [U_66] : power_power(U_67,number_number_of(U_67,U_66),number_number_of(nat,bit0(bit1(pls)))) = times_times(U_67,number_number_of(U_67,U_66),number_number_of(U_67,U_66))
| ~ number(U_67)
| ~ monoid_mult(U_67) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
( power_power(U_67,number_number_of(U_67,U_66),number_number_of(nat,bit0(bit1(pls)))) = times_times(U_67,number_number_of(U_67,U_66),number_number_of(U_67,U_66))
| ~ number(U_67)
| ~ monoid_mult(U_67) ),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
! [A_1] : times_times(int,A_1,power_power(int,A_1,number_number_of(nat,bit0(bit1(pls))))) = power_power(int,A_1,number_number_of(nat,bit1(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_11_cube__square]) ).
fof(f_39_2,plain,
! [U_68] : times_times(int,U_68,power_power(int,U_68,number_number_of(nat,bit0(bit1(pls))))) = power_power(int,U_68,number_number_of(nat,bit1(bit1(pls)))),
inference(variable_rename,[status(thm)],[f_39_1]) ).
cnf(f_39_3,plain,
times_times(int,U_68,power_power(int,U_68,number_number_of(nat,bit0(bit1(pls))))) = power_power(int,U_68,number_number_of(nat,bit1(bit1(pls)))),
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_40_1,plain,
! [X_a] :
( power_power(X_a,one_one(X_a),number_number_of(nat,bit0(bit1(pls)))) = one_one(X_a)
| ~ semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_12_one__power2]) ).
fof(f_40_2,plain,
! [U_69] :
( power_power(U_69,one_one(U_69),number_number_of(nat,bit0(bit1(pls)))) = one_one(U_69)
| ~ semiring_1(U_69) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( power_power(U_69,one_one(U_69),number_number_of(nat,bit0(bit1(pls)))) = one_one(U_69)
| ~ semiring_1(U_69) ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_41_1,plain,
! [X_a] :
( ! [X_1] : times_times(X_a,X_1,X_1) = power_power(X_a,X_1,number_number_of(nat,bit0(bit1(pls))))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_13_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J]) ).
fof(f_41_2,plain,
! [U_71] :
( ! [U_70] : times_times(U_71,U_70,U_70) = power_power(U_71,U_70,number_number_of(nat,bit0(bit1(pls))))
| ~ comm_semiring_1(U_71) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
cnf(f_41_3,plain,
( times_times(U_71,U_70,U_70) = power_power(U_71,U_70,number_number_of(nat,bit0(bit1(pls))))
| ~ comm_semiring_1(U_71) ),
inference(clausify,[status(thm)],[f_41_2]) ).
fof(f_42_1,plain,
! [X_a] :
( ! [A_1] : power_power(X_a,A_1,number_number_of(nat,bit0(bit1(pls)))) = times_times(X_a,A_1,A_1)
| ~ monoid_mult(X_a) ),
inference(fof_nnf,[status(thm)],[fact_14_power2__eq__square]) ).
fof(f_42_2,plain,
! [U_73] :
( ! [U_72] : power_power(U_73,U_72,number_number_of(nat,bit0(bit1(pls)))) = times_times(U_73,U_72,U_72)
| ~ monoid_mult(U_73) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
( power_power(U_73,U_72,number_number_of(nat,bit0(bit1(pls)))) = times_times(U_73,U_72,U_72)
| ~ monoid_mult(U_73) ),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
! [X_a] :
( ! [X_1,N] : power_power(X_a,X_1,times_times(nat,number_number_of(nat,bit0(bit1(pls))),N)) = times_times(X_a,power_power(X_a,X_1,N),power_power(X_a,X_1,N))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_15_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J]) ).
fof(f_43_2,plain,
! [U_76] :
( ! [U_75,U_74] : power_power(U_76,U_75,times_times(nat,number_number_of(nat,bit0(bit1(pls))),U_74)) = times_times(U_76,power_power(U_76,U_75,U_74),power_power(U_76,U_75,U_74))
| ~ comm_semiring_1(U_76) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
( power_power(U_76,U_75,times_times(nat,number_number_of(nat,bit0(bit1(pls))),U_74)) = times_times(U_76,power_power(U_76,U_75,U_74),power_power(U_76,U_75,U_74))
| ~ comm_semiring_1(U_76) ),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_44_1,plain,
! [X_a] :
( ! [W] : plus_plus(X_a,one_one(X_a),number_number_of(X_a,W)) = number_number_of(X_a,plus_plus(int,bit1(pls),W))
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_16_add__special_I2_J]) ).
fof(f_44_2,plain,
! [U_78] :
( ! [U_77] : plus_plus(U_78,one_one(U_78),number_number_of(U_78,U_77)) = number_number_of(U_78,plus_plus(int,bit1(pls),U_77))
| ~ number_ring(U_78) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
( plus_plus(U_78,one_one(U_78),number_number_of(U_78,U_77)) = number_number_of(U_78,plus_plus(int,bit1(pls),U_77))
| ~ number_ring(U_78) ),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_1,plain,
! [X_a] :
( ! [V] : plus_plus(X_a,number_number_of(X_a,V),one_one(X_a)) = number_number_of(X_a,plus_plus(int,V,bit1(pls)))
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_17_add__special_I3_J]) ).
fof(f_45_2,plain,
! [U_80] :
( ! [U_79] : plus_plus(U_80,number_number_of(U_80,U_79),one_one(U_80)) = number_number_of(U_80,plus_plus(int,U_79,bit1(pls)))
| ~ number_ring(U_80) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
cnf(f_45_3,plain,
( plus_plus(U_80,number_number_of(U_80,U_79),one_one(U_80)) = number_number_of(U_80,plus_plus(int,U_79,bit1(pls)))
| ~ number_ring(U_80) ),
inference(clausify,[status(thm)],[f_45_2]) ).
fof(f_46_1,plain,
! [X_a] :
( plus_plus(X_a,one_one(X_a),one_one(X_a)) = number_number_of(X_a,bit0(bit1(pls)))
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_18_one__add__one__is__two]) ).
fof(f_46_2,plain,
! [U_81] :
( plus_plus(U_81,one_one(U_81),one_one(U_81)) = number_number_of(U_81,bit0(bit1(pls)))
| ~ number_ring(U_81) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
cnf(f_46_3,plain,
( plus_plus(U_81,one_one(U_81),one_one(U_81)) = number_number_of(U_81,bit0(bit1(pls)))
| ~ number_ring(U_81) ),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_47_1,plain,
? [T_1] : plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),T_1),
inference(fof_nnf,[status(thm)],[fact_19__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_]) ).
fof(f_47_2,plain,
? [U_82] : plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),U_82),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),sK5),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_82,sK5)],[f_47_2]) ).
cnf(f_47_4,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),sK5),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [W] : ord_less_eq(int,W,W),
inference(fof_nnf,[status(thm)],[fact_20_zle__refl]) ).
fof(f_48_2,plain,
! [U_83] : ord_less_eq(int,U_83,U_83),
inference(variable_rename,[status(thm)],[f_48_1]) ).
cnf(f_48_3,plain,
ord_less_eq(int,U_83,U_83),
inference(clausify,[status(thm)],[f_48_2]) ).
fof(f_49_1,plain,
! [Z,W] :
( ord_less_eq(int,W,Z)
| ord_less_eq(int,Z,W) ),
inference(fof_nnf,[status(thm)],[fact_21_zle__linear]) ).
fof(f_49_2,plain,
! [U_85,U_84] :
( ord_less_eq(int,U_84,U_85)
| ord_less_eq(int,U_85,U_84) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
cnf(f_49_3,plain,
( ord_less_eq(int,U_84,U_85)
| ord_less_eq(int,U_85,U_84) ),
inference(clausify,[status(thm)],[f_49_2]) ).
fof(f_50_1,plain,
! [Z_1,W_1] :
( ( ord_less(int,Z_1,W_1)
| Z_1 = W_1
| ~ ord_less_eq(int,Z_1,W_1) )
& ( ( Z_1 != W_1
& ord_less_eq(int,Z_1,W_1) )
| ~ ord_less(int,Z_1,W_1) ) ),
inference(fof_nnf,[status(thm)],[fact_22_zless__le]) ).
fof(f_50_2,plain,
! [U_87,U_86] :
( ( ord_less(int,U_87,U_86)
| U_87 = U_86
| ~ ord_less_eq(int,U_87,U_86) )
& ( ( U_87 != U_86
& ord_less_eq(int,U_87,U_86) )
| ~ ord_less(int,U_87,U_86) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_91,U_89] :
( ord_less(int,U_91,U_89)
| U_91 = U_89
| ~ ord_less_eq(int,U_91,U_89) )
& ! [U_90,U_88] :
( ( U_90 != U_88
& ord_less_eq(int,U_90,U_88) )
| ~ ord_less(int,U_90,U_88) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( ord_less_eq(int,U_90,U_88)
| ~ ord_less(int,U_90,U_88) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_5,plain,
( U_90 != U_88
| ~ ord_less(int,U_90,U_88) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_6,plain,
( ord_less(int,U_91,U_89)
| U_91 = U_89
| ~ ord_less_eq(int,U_91,U_89) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_1,plain,
! [X_1,Y_1] :
( ord_less(int,Y_1,X_1)
| X_1 = Y_1
| ord_less(int,X_1,Y_1) ),
inference(fof_nnf,[status(thm)],[fact_23_zless__linear]) ).
fof(f_51_2,plain,
! [U_93,U_92] :
( ord_less(int,U_92,U_93)
| U_93 = U_92
| ord_less(int,U_93,U_92) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
cnf(f_51_3,plain,
( ord_less(int,U_92,U_93)
| U_93 = U_92
| ord_less(int,U_93,U_92) ),
inference(clausify,[status(thm)],[f_51_2]) ).
fof(f_52_1,plain,
! [K_1,I,J] :
( ord_less_eq(int,I,K_1)
| ~ ord_less_eq(int,J,K_1)
| ~ ord_less_eq(int,I,J) ),
inference(fof_nnf,[status(thm)],[fact_24_zle__trans]) ).
fof(f_52_2,plain,
! [U_96,U_95,U_94] :
( ord_less_eq(int,U_95,U_96)
| ~ ord_less_eq(int,U_94,U_96)
| ~ ord_less_eq(int,U_95,U_94) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
cnf(f_52_3,plain,
( ord_less_eq(int,U_95,U_96)
| ~ ord_less_eq(int,U_94,U_96)
| ~ ord_less_eq(int,U_95,U_94) ),
inference(clausify,[status(thm)],[f_52_2]) ).
fof(f_53_1,plain,
! [Z,W] :
( Z = W
| ~ ord_less_eq(int,W,Z)
| ~ ord_less_eq(int,Z,W) ),
inference(fof_nnf,[status(thm)],[fact_25_zle__antisym]) ).
fof(f_53_2,plain,
! [U_98,U_97] :
( U_98 = U_97
| ~ ord_less_eq(int,U_97,U_98)
| ~ ord_less_eq(int,U_98,U_97) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
cnf(f_53_3,plain,
( U_98 = U_97
| ~ ord_less_eq(int,U_97,U_98)
| ~ ord_less_eq(int,U_98,U_97) ),
inference(clausify,[status(thm)],[f_53_2]) ).
fof(f_54_1,plain,
! [X_a] :
( ! [X_1,P,Q] : power_power(X_a,power_power(X_a,X_1,P),Q) = power_power(X_a,X_1,times_times(nat,P,Q))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_26_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J]) ).
fof(f_54_2,plain,
! [U_102] :
( ! [U_101,U_100,U_99] : power_power(U_102,power_power(U_102,U_101,U_100),U_99) = power_power(U_102,U_101,times_times(nat,U_100,U_99))
| ~ comm_semiring_1(U_102) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
cnf(f_54_3,plain,
( power_power(U_102,power_power(U_102,U_101,U_100),U_99) = power_power(U_102,U_101,times_times(nat,U_100,U_99))
| ~ comm_semiring_1(U_102) ),
inference(clausify,[status(thm)],[f_54_2]) ).
fof(f_55_1,plain,
! [X_a] :
( ! [X_1] : power_power(X_a,X_1,one_one(nat)) = ti(X_a,X_1)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_27_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J]) ).
fof(f_55_2,plain,
! [U_104] :
( ! [U_103] : power_power(U_104,U_103,one_one(nat)) = ti(U_104,U_103)
| ~ comm_semiring_1(U_104) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
cnf(f_55_3,plain,
( power_power(U_104,U_103,one_one(nat)) = ti(U_104,U_103)
| ~ comm_semiring_1(U_104) ),
inference(clausify,[status(thm)],[f_55_2]) ).
fof(f_56_1,plain,
! [X_1,Y_1,Z] : power_power(int,power_power(int,X_1,Y_1),Z) = power_power(int,X_1,times_times(nat,Y_1,Z)),
inference(fof_nnf,[status(thm)],[fact_28_zpower__zpower]) ).
fof(f_56_2,plain,
! [U_107,U_106,U_105] : power_power(int,power_power(int,U_107,U_106),U_105) = power_power(int,U_107,times_times(nat,U_106,U_105)),
inference(variable_rename,[status(thm)],[f_56_1]) ).
cnf(f_56_3,plain,
power_power(int,power_power(int,U_107,U_106),U_105) = power_power(int,U_107,times_times(nat,U_106,U_105)),
inference(clausify,[status(thm)],[f_56_2]) ).
fof(f_57_1,plain,
! [X_a] :
( ! [V_2,W_1] :
( ( ord_less_eq(X_a,number_number_of(X_a,V_2),number_number_of(X_a,W_1))
| ord_less(X_a,number_number_of(X_a,W_1),number_number_of(X_a,V_2)) )
& ( ~ ord_less(X_a,number_number_of(X_a,W_1),number_number_of(X_a,V_2))
| ~ ord_less_eq(X_a,number_number_of(X_a,V_2),number_number_of(X_a,W_1)) ) )
| ~ linorder(X_a)
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[fact_29_le__number__of__eq__not__less]) ).
fof(f_57_2,plain,
! [U_110] :
( ! [U_109,U_108] :
( ( ord_less_eq(U_110,number_number_of(U_110,U_109),number_number_of(U_110,U_108))
| ord_less(U_110,number_number_of(U_110,U_108),number_number_of(U_110,U_109)) )
& ( ~ ord_less(U_110,number_number_of(U_110,U_108),number_number_of(U_110,U_109))
| ~ ord_less_eq(U_110,number_number_of(U_110,U_109),number_number_of(U_110,U_108)) ) )
| ~ linorder(U_110)
| ~ number(U_110) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
! [U_110] :
( ( ! [U_114,U_112] :
( ord_less_eq(U_110,number_number_of(U_110,U_114),number_number_of(U_110,U_112))
| ord_less(U_110,number_number_of(U_110,U_112),number_number_of(U_110,U_114)) )
& ! [U_113,U_111] :
( ~ ord_less(U_110,number_number_of(U_110,U_111),number_number_of(U_110,U_113))
| ~ ord_less_eq(U_110,number_number_of(U_110,U_113),number_number_of(U_110,U_111)) ) )
| ~ linorder(U_110)
| ~ number(U_110) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( ~ ord_less(U_110,number_number_of(U_110,U_111),number_number_of(U_110,U_113))
| ~ ord_less_eq(U_110,number_number_of(U_110,U_113),number_number_of(U_110,U_111))
| ~ linorder(U_110)
| ~ number(U_110) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( ord_less_eq(U_110,number_number_of(U_110,U_114),number_number_of(U_110,U_112))
| ord_less(U_110,number_number_of(U_110,U_112),number_number_of(U_110,U_114))
| ~ linorder(U_110)
| ~ number(U_110) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [X_a] :
( ! [X_2,Y_2] :
( ( ord_less(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2))
| ~ ord_less(int,X_2,Y_2) )
& ( ord_less(int,X_2,Y_2)
| ~ ord_less(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2)) ) )
| ~ linordered_idom(X_a)
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_30_less__number__of]) ).
fof(f_58_2,plain,
! [U_117] :
( ! [U_116,U_115] :
( ( ord_less(U_117,number_number_of(U_117,U_116),number_number_of(U_117,U_115))
| ~ ord_less(int,U_116,U_115) )
& ( ord_less(int,U_116,U_115)
| ~ ord_less(U_117,number_number_of(U_117,U_116),number_number_of(U_117,U_115)) ) )
| ~ linordered_idom(U_117)
| ~ number_ring(U_117) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
! [U_117] :
( ( ! [U_121,U_119] :
( ord_less(U_117,number_number_of(U_117,U_121),number_number_of(U_117,U_119))
| ~ ord_less(int,U_121,U_119) )
& ! [U_120,U_118] :
( ord_less(int,U_120,U_118)
| ~ ord_less(U_117,number_number_of(U_117,U_120),number_number_of(U_117,U_118)) ) )
| ~ linordered_idom(U_117)
| ~ number_ring(U_117) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( ord_less(int,U_120,U_118)
| ~ ord_less(U_117,number_number_of(U_117,U_120),number_number_of(U_117,U_118))
| ~ linordered_idom(U_117)
| ~ number_ring(U_117) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( ord_less(U_117,number_number_of(U_117,U_121),number_number_of(U_117,U_119))
| ~ ord_less(int,U_121,U_119)
| ~ linordered_idom(U_117)
| ~ number_ring(U_117) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [X_a] :
( ! [X_2,Y_2] :
( ( ord_less_eq(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2))
| ~ ord_less_eq(int,X_2,Y_2) )
& ( ord_less_eq(int,X_2,Y_2)
| ~ ord_less_eq(X_a,number_number_of(X_a,X_2),number_number_of(X_a,Y_2)) ) )
| ~ linordered_idom(X_a)
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_31_le__number__of]) ).
fof(f_59_2,plain,
! [U_124] :
( ! [U_123,U_122] :
( ( ord_less_eq(U_124,number_number_of(U_124,U_123),number_number_of(U_124,U_122))
| ~ ord_less_eq(int,U_123,U_122) )
& ( ord_less_eq(int,U_123,U_122)
| ~ ord_less_eq(U_124,number_number_of(U_124,U_123),number_number_of(U_124,U_122)) ) )
| ~ linordered_idom(U_124)
| ~ number_ring(U_124) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
! [U_124] :
( ( ! [U_128,U_126] :
( ord_less_eq(U_124,number_number_of(U_124,U_128),number_number_of(U_124,U_126))
| ~ ord_less_eq(int,U_128,U_126) )
& ! [U_127,U_125] :
( ord_less_eq(int,U_127,U_125)
| ~ ord_less_eq(U_124,number_number_of(U_124,U_127),number_number_of(U_124,U_125)) ) )
| ~ linordered_idom(U_124)
| ~ number_ring(U_124) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
cnf(f_59_4,plain,
( ord_less_eq(int,U_127,U_125)
| ~ ord_less_eq(U_124,number_number_of(U_124,U_127),number_number_of(U_124,U_125))
| ~ linordered_idom(U_124)
| ~ number_ring(U_124) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_5,plain,
( ord_less_eq(U_124,number_number_of(U_124,U_128),number_number_of(U_124,U_126))
| ~ ord_less_eq(int,U_128,U_126)
| ~ linordered_idom(U_124)
| ~ number_ring(U_124) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_1,plain,
! [Z_2,Z,W_2,W] :
( ord_less(int,plus_plus(int,W_2,Z_2),plus_plus(int,W,Z))
| ~ ord_less_eq(int,Z_2,Z)
| ~ ord_less(int,W_2,W) ),
inference(fof_nnf,[status(thm)],[fact_32_zadd__zless__mono]) ).
fof(f_60_2,plain,
! [U_132,U_131,U_130,U_129] :
( ord_less(int,plus_plus(int,U_130,U_132),plus_plus(int,U_129,U_131))
| ~ ord_less_eq(int,U_132,U_131)
| ~ ord_less(int,U_130,U_129) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
cnf(f_60_3,plain,
( ord_less(int,plus_plus(int,U_130,U_132),plus_plus(int,U_129,U_131))
| ~ ord_less_eq(int,U_132,U_131)
| ~ ord_less(int,U_130,U_129) ),
inference(clausify,[status(thm)],[f_60_2]) ).
fof(f_61_1,plain,
! [X_a] :
( ! [X_1,P,Q] : times_times(X_a,power_power(X_a,X_1,P),power_power(X_a,X_1,Q)) = power_power(X_a,X_1,plus_plus(nat,P,Q))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J]) ).
fof(f_61_2,plain,
! [U_136] :
( ! [U_135,U_134,U_133] : times_times(U_136,power_power(U_136,U_135,U_134),power_power(U_136,U_135,U_133)) = power_power(U_136,U_135,plus_plus(nat,U_134,U_133))
| ~ comm_semiring_1(U_136) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
cnf(f_61_3,plain,
( times_times(U_136,power_power(U_136,U_135,U_134),power_power(U_136,U_135,U_133)) = power_power(U_136,U_135,plus_plus(nat,U_134,U_133))
| ~ comm_semiring_1(U_136) ),
inference(clausify,[status(thm)],[f_61_2]) ).
fof(f_62_1,plain,
! [X_1,Y_1,Z] : power_power(int,X_1,plus_plus(nat,Y_1,Z)) = times_times(int,power_power(int,X_1,Y_1),power_power(int,X_1,Z)),
inference(fof_nnf,[status(thm)],[fact_34_zpower__zadd__distrib]) ).
fof(f_62_2,plain,
! [U_139,U_138,U_137] : power_power(int,U_139,plus_plus(nat,U_138,U_137)) = times_times(int,power_power(int,U_139,U_138),power_power(int,U_139,U_137)),
inference(variable_rename,[status(thm)],[f_62_1]) ).
cnf(f_62_3,plain,
power_power(int,U_139,plus_plus(nat,U_138,U_137)) = times_times(int,power_power(int,U_139,U_138),power_power(int,U_139,U_137)),
inference(clausify,[status(thm)],[f_62_2]) ).
fof(f_63_1,plain,
! [Z] : times_times(nat,number_number_of(nat,bit0(bit1(pls))),Z) = plus_plus(nat,Z,Z),
inference(fof_nnf,[status(thm)],[fact_35_nat__mult__2]) ).
fof(f_63_2,plain,
! [U_140] : times_times(nat,number_number_of(nat,bit0(bit1(pls))),U_140) = plus_plus(nat,U_140,U_140),
inference(variable_rename,[status(thm)],[f_63_1]) ).
cnf(f_63_3,plain,
times_times(nat,number_number_of(nat,bit0(bit1(pls))),U_140) = plus_plus(nat,U_140,U_140),
inference(clausify,[status(thm)],[f_63_2]) ).
fof(f_64_1,plain,
! [Z] : times_times(nat,Z,number_number_of(nat,bit0(bit1(pls)))) = plus_plus(nat,Z,Z),
inference(fof_nnf,[status(thm)],[fact_36_nat__mult__2__right]) ).
fof(f_64_2,plain,
! [U_141] : times_times(nat,U_141,number_number_of(nat,bit0(bit1(pls)))) = plus_plus(nat,U_141,U_141),
inference(variable_rename,[status(thm)],[f_64_1]) ).
cnf(f_64_3,plain,
times_times(nat,U_141,number_number_of(nat,bit0(bit1(pls)))) = plus_plus(nat,U_141,U_141),
inference(clausify,[status(thm)],[f_64_2]) ).
fof(f_65_1,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_37_nat__1__add__1]) ).
cnf(f_65_2,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_1,plain,
! [K1,K2] :
( ( ord_less(int,bit1(K1),bit1(K2))
| ~ ord_less(int,K1,K2) )
& ( ord_less(int,K1,K2)
| ~ ord_less(int,bit1(K1),bit1(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_38_less__int__code_I16_J]) ).
fof(f_66_2,plain,
! [U_143,U_142] :
( ( ord_less(int,bit1(U_143),bit1(U_142))
| ~ ord_less(int,U_143,U_142) )
& ( ord_less(int,U_143,U_142)
| ~ ord_less(int,bit1(U_143),bit1(U_142)) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_147,U_145] :
( ord_less(int,bit1(U_147),bit1(U_145))
| ~ ord_less(int,U_147,U_145) )
& ! [U_146,U_144] :
( ord_less(int,U_146,U_144)
| ~ ord_less(int,bit1(U_146),bit1(U_144)) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( ord_less(int,U_146,U_144)
| ~ ord_less(int,bit1(U_146),bit1(U_144)) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( ord_less(int,bit1(U_147),bit1(U_145))
| ~ ord_less(int,U_147,U_145) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [K,L] :
( ( ord_less(int,bit1(K),bit1(L))
| ~ ord_less(int,K,L) )
& ( ord_less(int,K,L)
| ~ ord_less(int,bit1(K),bit1(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_39_rel__simps_I17_J]) ).
fof(f_67_2,plain,
! [U_149,U_148] :
( ( ord_less(int,bit1(U_149),bit1(U_148))
| ~ ord_less(int,U_149,U_148) )
& ( ord_less(int,U_149,U_148)
| ~ ord_less(int,bit1(U_149),bit1(U_148)) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_153,U_151] :
( ord_less(int,bit1(U_153),bit1(U_151))
| ~ ord_less(int,U_153,U_151) )
& ! [U_152,U_150] :
( ord_less(int,U_152,U_150)
| ~ ord_less(int,bit1(U_152),bit1(U_150)) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
cnf(f_67_4,plain,
( ord_less(int,U_152,U_150)
| ~ ord_less(int,bit1(U_152),bit1(U_150)) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_5,plain,
( ord_less(int,bit1(U_153),bit1(U_151))
| ~ ord_less(int,U_153,U_151) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_68_1,plain,
! [K1,K2] :
( ( ord_less_eq(int,bit1(K1),bit1(K2))
| ~ ord_less_eq(int,K1,K2) )
& ( ord_less_eq(int,K1,K2)
| ~ ord_less_eq(int,bit1(K1),bit1(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_40_less__eq__int__code_I16_J]) ).
fof(f_68_2,plain,
! [U_155,U_154] :
( ( ord_less_eq(int,bit1(U_155),bit1(U_154))
| ~ ord_less_eq(int,U_155,U_154) )
& ( ord_less_eq(int,U_155,U_154)
| ~ ord_less_eq(int,bit1(U_155),bit1(U_154)) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_159,U_157] :
( ord_less_eq(int,bit1(U_159),bit1(U_157))
| ~ ord_less_eq(int,U_159,U_157) )
& ! [U_158,U_156] :
( ord_less_eq(int,U_158,U_156)
| ~ ord_less_eq(int,bit1(U_158),bit1(U_156)) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ord_less_eq(int,U_158,U_156)
| ~ ord_less_eq(int,bit1(U_158),bit1(U_156)) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( ord_less_eq(int,bit1(U_159),bit1(U_157))
| ~ ord_less_eq(int,U_159,U_157) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
! [K,L] :
( ( ord_less_eq(int,bit1(K),bit1(L))
| ~ ord_less_eq(int,K,L) )
& ( ord_less_eq(int,K,L)
| ~ ord_less_eq(int,bit1(K),bit1(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_41_rel__simps_I34_J]) ).
fof(f_69_2,plain,
! [U_161,U_160] :
( ( ord_less_eq(int,bit1(U_161),bit1(U_160))
| ~ ord_less_eq(int,U_161,U_160) )
& ( ord_less_eq(int,U_161,U_160)
| ~ ord_less_eq(int,bit1(U_161),bit1(U_160)) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_165,U_163] :
( ord_less_eq(int,bit1(U_165),bit1(U_163))
| ~ ord_less_eq(int,U_165,U_163) )
& ! [U_164,U_162] :
( ord_less_eq(int,U_164,U_162)
| ~ ord_less_eq(int,bit1(U_164),bit1(U_162)) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
cnf(f_69_4,plain,
( ord_less_eq(int,U_164,U_162)
| ~ ord_less_eq(int,bit1(U_164),bit1(U_162)) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(f_69_5,plain,
( ord_less_eq(int,bit1(U_165),bit1(U_163))
| ~ ord_less_eq(int,U_165,U_163) ),
inference(clausify,[status(thm)],[f_69_3]) ).
fof(f_70_1,plain,
~ ord_less(int,pls,pls),
inference(fof_nnf,[status(thm)],[fact_42_rel__simps_I2_J]) ).
cnf(f_70_2,plain,
~ ord_less(int,pls,pls),
inference(clausify,[status(thm)],[f_70_1]) ).
fof(f_71_1,plain,
! [K1,K2] :
( ( ord_less(int,bit0(K1),bit0(K2))
| ~ ord_less(int,K1,K2) )
& ( ord_less(int,K1,K2)
| ~ ord_less(int,bit0(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_43_less__int__code_I13_J]) ).
fof(f_71_2,plain,
! [U_167,U_166] :
( ( ord_less(int,bit0(U_167),bit0(U_166))
| ~ ord_less(int,U_167,U_166) )
& ( ord_less(int,U_167,U_166)
| ~ ord_less(int,bit0(U_167),bit0(U_166)) ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_171,U_169] :
( ord_less(int,bit0(U_171),bit0(U_169))
| ~ ord_less(int,U_171,U_169) )
& ! [U_170,U_168] :
( ord_less(int,U_170,U_168)
| ~ ord_less(int,bit0(U_170),bit0(U_168)) ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( ord_less(int,U_170,U_168)
| ~ ord_less(int,bit0(U_170),bit0(U_168)) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( ord_less(int,bit0(U_171),bit0(U_169))
| ~ ord_less(int,U_171,U_169) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_1,plain,
! [K,L] :
( ( ord_less(int,bit0(K),bit0(L))
| ~ ord_less(int,K,L) )
& ( ord_less(int,K,L)
| ~ ord_less(int,bit0(K),bit0(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_44_rel__simps_I14_J]) ).
fof(f_72_2,plain,
! [U_173,U_172] :
( ( ord_less(int,bit0(U_173),bit0(U_172))
| ~ ord_less(int,U_173,U_172) )
& ( ord_less(int,U_173,U_172)
| ~ ord_less(int,bit0(U_173),bit0(U_172)) ) ),
inference(variable_rename,[status(thm)],[f_72_1]) ).
fof(f_72_3,plain,
( ! [U_177,U_175] :
( ord_less(int,bit0(U_177),bit0(U_175))
| ~ ord_less(int,U_177,U_175) )
& ! [U_176,U_174] :
( ord_less(int,U_176,U_174)
| ~ ord_less(int,bit0(U_176),bit0(U_174)) ) ),
inference(miniscope,[status(thm)],[f_72_2]) ).
cnf(f_72_4,plain,
( ord_less(int,U_176,U_174)
| ~ ord_less(int,bit0(U_176),bit0(U_174)) ),
inference(clausify,[status(thm)],[f_72_3]) ).
cnf(f_72_5,plain,
( ord_less(int,bit0(U_177),bit0(U_175))
| ~ ord_less(int,U_177,U_175) ),
inference(clausify,[status(thm)],[f_72_3]) ).
fof(f_73_1,plain,
ord_less_eq(int,pls,pls),
inference(fof_nnf,[status(thm)],[fact_45_rel__simps_I19_J]) ).
cnf(f_73_2,plain,
ord_less_eq(int,pls,pls),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
! [K1,K2] :
( ( ord_less_eq(int,bit0(K1),bit0(K2))
| ~ ord_less_eq(int,K1,K2) )
& ( ord_less_eq(int,K1,K2)
| ~ ord_less_eq(int,bit0(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_46_less__eq__int__code_I13_J]) ).
fof(f_74_2,plain,
! [U_179,U_178] :
( ( ord_less_eq(int,bit0(U_179),bit0(U_178))
| ~ ord_less_eq(int,U_179,U_178) )
& ( ord_less_eq(int,U_179,U_178)
| ~ ord_less_eq(int,bit0(U_179),bit0(U_178)) ) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
fof(f_74_3,plain,
( ! [U_183,U_181] :
( ord_less_eq(int,bit0(U_183),bit0(U_181))
| ~ ord_less_eq(int,U_183,U_181) )
& ! [U_182,U_180] :
( ord_less_eq(int,U_182,U_180)
| ~ ord_less_eq(int,bit0(U_182),bit0(U_180)) ) ),
inference(miniscope,[status(thm)],[f_74_2]) ).
cnf(f_74_4,plain,
( ord_less_eq(int,U_182,U_180)
| ~ ord_less_eq(int,bit0(U_182),bit0(U_180)) ),
inference(clausify,[status(thm)],[f_74_3]) ).
cnf(f_74_5,plain,
( ord_less_eq(int,bit0(U_183),bit0(U_181))
| ~ ord_less_eq(int,U_183,U_181) ),
inference(clausify,[status(thm)],[f_74_3]) ).
fof(f_75_1,plain,
! [K,L] :
( ( ord_less_eq(int,bit0(K),bit0(L))
| ~ ord_less_eq(int,K,L) )
& ( ord_less_eq(int,K,L)
| ~ ord_less_eq(int,bit0(K),bit0(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_47_rel__simps_I31_J]) ).
fof(f_75_2,plain,
! [U_185,U_184] :
( ( ord_less_eq(int,bit0(U_185),bit0(U_184))
| ~ ord_less_eq(int,U_185,U_184) )
& ( ord_less_eq(int,U_185,U_184)
| ~ ord_less_eq(int,bit0(U_185),bit0(U_184)) ) ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
fof(f_75_3,plain,
( ! [U_189,U_187] :
( ord_less_eq(int,bit0(U_189),bit0(U_187))
| ~ ord_less_eq(int,U_189,U_187) )
& ! [U_188,U_186] :
( ord_less_eq(int,U_188,U_186)
| ~ ord_less_eq(int,bit0(U_188),bit0(U_186)) ) ),
inference(miniscope,[status(thm)],[f_75_2]) ).
cnf(f_75_4,plain,
( ord_less_eq(int,U_188,U_186)
| ~ ord_less_eq(int,bit0(U_188),bit0(U_186)) ),
inference(clausify,[status(thm)],[f_75_3]) ).
cnf(f_75_5,plain,
( ord_less_eq(int,bit0(U_189),bit0(U_187))
| ~ ord_less_eq(int,U_189,U_187) ),
inference(clausify,[status(thm)],[f_75_3]) ).
fof(f_76_1,plain,
! [K,L] :
( ( ord_less(int,number_number_of(int,K),number_number_of(int,L))
| ~ ord_less(int,K,L) )
& ( ord_less(int,K,L)
| ~ ord_less(int,number_number_of(int,K),number_number_of(int,L)) ) ),
inference(fof_nnf,[status(thm)],[fact_48_less__number__of__int__code]) ).
fof(f_76_2,plain,
! [U_191,U_190] :
( ( ord_less(int,number_number_of(int,U_191),number_number_of(int,U_190))
| ~ ord_less(int,U_191,U_190) )
& ( ord_less(int,U_191,U_190)
| ~ ord_less(int,number_number_of(int,U_191),number_number_of(int,U_190)) ) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
fof(f_76_3,plain,
( ! [U_195,U_193] :
( ord_less(int,number_number_of(int,U_195),number_number_of(int,U_193))
| ~ ord_less(int,U_195,U_193) )
& ! [U_194,U_192] :
( ord_less(int,U_194,U_192)
| ~ ord_less(int,number_number_of(int,U_194),number_number_of(int,U_192)) ) ),
inference(miniscope,[status(thm)],[f_76_2]) ).
cnf(f_76_4,plain,
( ord_less(int,U_194,U_192)
| ~ ord_less(int,number_number_of(int,U_194),number_number_of(int,U_192)) ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_5,plain,
( ord_less(int,number_number_of(int,U_195),number_number_of(int,U_193))
| ~ ord_less(int,U_195,U_193) ),
inference(clausify,[status(thm)],[f_76_3]) ).
fof(f_77_1,plain,
! [K,L] :
( ( ord_less_eq(int,number_number_of(int,K),number_number_of(int,L))
| ~ ord_less_eq(int,K,L) )
& ( ord_less_eq(int,K,L)
| ~ ord_less_eq(int,number_number_of(int,K),number_number_of(int,L)) ) ),
inference(fof_nnf,[status(thm)],[fact_49_less__eq__number__of__int__code]) ).
fof(f_77_2,plain,
! [U_197,U_196] :
( ( ord_less_eq(int,number_number_of(int,U_197),number_number_of(int,U_196))
| ~ ord_less_eq(int,U_197,U_196) )
& ( ord_less_eq(int,U_197,U_196)
| ~ ord_less_eq(int,number_number_of(int,U_197),number_number_of(int,U_196)) ) ),
inference(variable_rename,[status(thm)],[f_77_1]) ).
fof(f_77_3,plain,
( ! [U_201,U_199] :
( ord_less_eq(int,number_number_of(int,U_201),number_number_of(int,U_199))
| ~ ord_less_eq(int,U_201,U_199) )
& ! [U_200,U_198] :
( ord_less_eq(int,U_200,U_198)
| ~ ord_less_eq(int,number_number_of(int,U_200),number_number_of(int,U_198)) ) ),
inference(miniscope,[status(thm)],[f_77_2]) ).
cnf(f_77_4,plain,
( ord_less_eq(int,U_200,U_198)
| ~ ord_less_eq(int,number_number_of(int,U_200),number_number_of(int,U_198)) ),
inference(clausify,[status(thm)],[f_77_3]) ).
cnf(f_77_5,plain,
( ord_less_eq(int,number_number_of(int,U_201),number_number_of(int,U_199))
| ~ ord_less_eq(int,U_201,U_199) ),
inference(clausify,[status(thm)],[f_77_3]) ).
fof(f_78_1,plain,
! [K_1,I,J] :
( ord_less(int,plus_plus(int,I,K_1),plus_plus(int,J,K_1))
| ~ ord_less(int,I,J) ),
inference(fof_nnf,[status(thm)],[fact_50_zadd__strict__right__mono]) ).
fof(f_78_2,plain,
! [U_204,U_203,U_202] :
( ord_less(int,plus_plus(int,U_203,U_204),plus_plus(int,U_202,U_204))
| ~ ord_less(int,U_203,U_202) ),
inference(variable_rename,[status(thm)],[f_78_1]) ).
cnf(f_78_3,plain,
( ord_less(int,plus_plus(int,U_203,U_204),plus_plus(int,U_202,U_204))
| ~ ord_less(int,U_203,U_202) ),
inference(clausify,[status(thm)],[f_78_2]) ).
fof(f_79_1,plain,
! [K_1,I,J] :
( ord_less_eq(int,plus_plus(int,K_1,I),plus_plus(int,K_1,J))
| ~ ord_less_eq(int,I,J) ),
inference(fof_nnf,[status(thm)],[fact_51_zadd__left__mono]) ).
fof(f_79_2,plain,
! [U_207,U_206,U_205] :
( ord_less_eq(int,plus_plus(int,U_207,U_206),plus_plus(int,U_207,U_205))
| ~ ord_less_eq(int,U_206,U_205) ),
inference(variable_rename,[status(thm)],[f_79_1]) ).
cnf(f_79_3,plain,
( ord_less_eq(int,plus_plus(int,U_207,U_206),plus_plus(int,U_207,U_205))
| ~ ord_less_eq(int,U_206,U_205) ),
inference(clausify,[status(thm)],[f_79_2]) ).
fof(f_80_1,plain,
! [V_1,V] :
( ( ( ( plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,plus_plus(int,V,V_1))
| ord_less(int,V_1,pls) )
& ( plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,V)
| ~ ord_less(int,V_1,pls) ) )
| ord_less(int,V,pls) )
& ( plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1)) = number_number_of(nat,V_1)
| ~ ord_less(int,V,pls) ) ),
inference(fof_nnf,[status(thm)],[fact_52_add__nat__number__of]) ).
fof(f_80_2,plain,
! [U_209,U_208] :
( ( ( ( plus_plus(nat,number_number_of(nat,U_208),number_number_of(nat,U_209)) = number_number_of(nat,plus_plus(int,U_208,U_209))
| ord_less(int,U_209,pls) )
& ( plus_plus(nat,number_number_of(nat,U_208),number_number_of(nat,U_209)) = number_number_of(nat,U_208)
| ~ ord_less(int,U_209,pls) ) )
| ord_less(int,U_208,pls) )
& ( plus_plus(nat,number_number_of(nat,U_208),number_number_of(nat,U_209)) = number_number_of(nat,U_209)
| ~ ord_less(int,U_208,pls) ) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
fof(f_80_3,plain,
( ! [U_213,U_211] :
( ( ( plus_plus(nat,number_number_of(nat,U_211),number_number_of(nat,U_213)) = number_number_of(nat,plus_plus(int,U_211,U_213))
| ord_less(int,U_213,pls) )
& ( plus_plus(nat,number_number_of(nat,U_211),number_number_of(nat,U_213)) = number_number_of(nat,U_211)
| ~ ord_less(int,U_213,pls) ) )
| ord_less(int,U_211,pls) )
& ! [U_212,U_210] :
( plus_plus(nat,number_number_of(nat,U_210),number_number_of(nat,U_212)) = number_number_of(nat,U_212)
| ~ ord_less(int,U_210,pls) ) ),
inference(miniscope,[status(thm)],[f_80_2]) ).
cnf(f_80_4,plain,
( plus_plus(nat,number_number_of(nat,U_210),number_number_of(nat,U_212)) = number_number_of(nat,U_212)
| ~ ord_less(int,U_210,pls) ),
inference(clausify,[status(thm)],[f_80_3]) ).
cnf(f_80_5,plain,
( plus_plus(nat,number_number_of(nat,U_211),number_number_of(nat,U_213)) = number_number_of(nat,U_211)
| ~ ord_less(int,U_213,pls)
| ord_less(int,U_211,pls) ),
inference(clausify,[status(thm)],[f_80_3]) ).
cnf(f_80_6,plain,
( plus_plus(nat,number_number_of(nat,U_211),number_number_of(nat,U_213)) = number_number_of(nat,plus_plus(int,U_211,U_213))
| ord_less(int,U_213,pls)
| ord_less(int,U_211,pls) ),
inference(clausify,[status(thm)],[f_80_3]) ).
fof(f_81_1,plain,
number_number_of(nat,bit1(pls)) = one_one(nat),
inference(fof_nnf,[status(thm)],[fact_53_nat__numeral__1__eq__1]) ).
cnf(f_81_2,plain,
number_number_of(nat,bit1(pls)) = one_one(nat),
inference(clausify,[status(thm)],[f_81_1]) ).
fof(f_82_1,plain,
one_one(nat) = number_number_of(nat,bit1(pls)),
inference(fof_nnf,[status(thm)],[fact_54_Numeral1__eq1__nat]) ).
cnf(f_82_2,plain,
one_one(nat) = number_number_of(nat,bit1(pls)),
inference(clausify,[status(thm)],[f_82_1]) ).
fof(f_83_1,plain,
! [K] :
( ( ord_less_eq(int,bit1(K),pls)
| ~ ord_less(int,K,pls) )
& ( ord_less(int,K,pls)
| ~ ord_less_eq(int,bit1(K),pls) ) ),
inference(fof_nnf,[status(thm)],[fact_55_rel__simps_I29_J]) ).
fof(f_83_2,plain,
! [U_214] :
( ( ord_less_eq(int,bit1(U_214),pls)
| ~ ord_less(int,U_214,pls) )
& ( ord_less(int,U_214,pls)
| ~ ord_less_eq(int,bit1(U_214),pls) ) ),
inference(variable_rename,[status(thm)],[f_83_1]) ).
fof(f_83_3,plain,
( ! [U_216] :
( ord_less_eq(int,bit1(U_216),pls)
| ~ ord_less(int,U_216,pls) )
& ! [U_215] :
( ord_less(int,U_215,pls)
| ~ ord_less_eq(int,bit1(U_215),pls) ) ),
inference(miniscope,[status(thm)],[f_83_2]) ).
cnf(f_83_4,plain,
( ord_less(int,U_215,pls)
| ~ ord_less_eq(int,bit1(U_215),pls) ),
inference(clausify,[status(thm)],[f_83_3]) ).
cnf(f_83_5,plain,
( ord_less_eq(int,bit1(U_216),pls)
| ~ ord_less(int,U_216,pls) ),
inference(clausify,[status(thm)],[f_83_3]) ).
fof(f_84_1,plain,
! [K] :
( ( ord_less(int,pls,bit1(K))
| ~ ord_less_eq(int,pls,K) )
& ( ord_less_eq(int,pls,K)
| ~ ord_less(int,pls,bit1(K)) ) ),
inference(fof_nnf,[status(thm)],[fact_56_rel__simps_I5_J]) ).
fof(f_84_2,plain,
! [U_217] :
( ( ord_less(int,pls,bit1(U_217))
| ~ ord_less_eq(int,pls,U_217) )
& ( ord_less_eq(int,pls,U_217)
| ~ ord_less(int,pls,bit1(U_217)) ) ),
inference(variable_rename,[status(thm)],[f_84_1]) ).
fof(f_84_3,plain,
( ! [U_219] :
( ord_less(int,pls,bit1(U_219))
| ~ ord_less_eq(int,pls,U_219) )
& ! [U_218] :
( ord_less_eq(int,pls,U_218)
| ~ ord_less(int,pls,bit1(U_218)) ) ),
inference(miniscope,[status(thm)],[f_84_2]) ).
cnf(f_84_4,plain,
( ord_less_eq(int,pls,U_218)
| ~ ord_less(int,pls,bit1(U_218)) ),
inference(clausify,[status(thm)],[f_84_3]) ).
cnf(f_84_5,plain,
( ord_less(int,pls,bit1(U_219))
| ~ ord_less_eq(int,pls,U_219) ),
inference(clausify,[status(thm)],[f_84_3]) ).
fof(f_85_1,plain,
! [K1,K2] :
( ( ord_less_eq(int,bit1(K1),bit0(K2))
| ~ ord_less(int,K1,K2) )
& ( ord_less(int,K1,K2)
| ~ ord_less_eq(int,bit1(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_57_less__eq__int__code_I15_J]) ).
fof(f_85_2,plain,
! [U_221,U_220] :
( ( ord_less_eq(int,bit1(U_221),bit0(U_220))
| ~ ord_less(int,U_221,U_220) )
& ( ord_less(int,U_221,U_220)
| ~ ord_less_eq(int,bit1(U_221),bit0(U_220)) ) ),
inference(variable_rename,[status(thm)],[f_85_1]) ).
fof(f_85_3,plain,
( ! [U_225,U_223] :
( ord_less_eq(int,bit1(U_225),bit0(U_223))
| ~ ord_less(int,U_225,U_223) )
& ! [U_224,U_222] :
( ord_less(int,U_224,U_222)
| ~ ord_less_eq(int,bit1(U_224),bit0(U_222)) ) ),
inference(miniscope,[status(thm)],[f_85_2]) ).
cnf(f_85_4,plain,
( ord_less(int,U_224,U_222)
| ~ ord_less_eq(int,bit1(U_224),bit0(U_222)) ),
inference(clausify,[status(thm)],[f_85_3]) ).
cnf(f_85_5,plain,
( ord_less_eq(int,bit1(U_225),bit0(U_223))
| ~ ord_less(int,U_225,U_223) ),
inference(clausify,[status(thm)],[f_85_3]) ).
fof(f_86_1,plain,
! [K,L] :
( ( ord_less_eq(int,bit1(K),bit0(L))
| ~ ord_less(int,K,L) )
& ( ord_less(int,K,L)
| ~ ord_less_eq(int,bit1(K),bit0(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_58_rel__simps_I33_J]) ).
fof(f_86_2,plain,
! [U_227,U_226] :
( ( ord_less_eq(int,bit1(U_227),bit0(U_226))
| ~ ord_less(int,U_227,U_226) )
& ( ord_less(int,U_227,U_226)
| ~ ord_less_eq(int,bit1(U_227),bit0(U_226)) ) ),
inference(variable_rename,[status(thm)],[f_86_1]) ).
fof(f_86_3,plain,
( ! [U_231,U_229] :
( ord_less_eq(int,bit1(U_231),bit0(U_229))
| ~ ord_less(int,U_231,U_229) )
& ! [U_230,U_228] :
( ord_less(int,U_230,U_228)
| ~ ord_less_eq(int,bit1(U_230),bit0(U_228)) ) ),
inference(miniscope,[status(thm)],[f_86_2]) ).
cnf(f_86_4,plain,
( ord_less(int,U_230,U_228)
| ~ ord_less_eq(int,bit1(U_230),bit0(U_228)) ),
inference(clausify,[status(thm)],[f_86_3]) ).
cnf(f_86_5,plain,
( ord_less_eq(int,bit1(U_231),bit0(U_229))
| ~ ord_less(int,U_231,U_229) ),
inference(clausify,[status(thm)],[f_86_3]) ).
fof(f_87_1,plain,
! [K1,K2] :
( ( ord_less(int,bit0(K1),bit1(K2))
| ~ ord_less_eq(int,K1,K2) )
& ( ord_less_eq(int,K1,K2)
| ~ ord_less(int,bit0(K1),bit1(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_59_less__int__code_I14_J]) ).
fof(f_87_2,plain,
! [U_233,U_232] :
( ( ord_less(int,bit0(U_233),bit1(U_232))
| ~ ord_less_eq(int,U_233,U_232) )
& ( ord_less_eq(int,U_233,U_232)
| ~ ord_less(int,bit0(U_233),bit1(U_232)) ) ),
inference(variable_rename,[status(thm)],[f_87_1]) ).
fof(f_87_3,plain,
( ! [U_237,U_235] :
( ord_less(int,bit0(U_237),bit1(U_235))
| ~ ord_less_eq(int,U_237,U_235) )
& ! [U_236,U_234] :
( ord_less_eq(int,U_236,U_234)
| ~ ord_less(int,bit0(U_236),bit1(U_234)) ) ),
inference(miniscope,[status(thm)],[f_87_2]) ).
cnf(f_87_4,plain,
( ord_less_eq(int,U_236,U_234)
| ~ ord_less(int,bit0(U_236),bit1(U_234)) ),
inference(clausify,[status(thm)],[f_87_3]) ).
cnf(f_87_5,plain,
( ord_less(int,bit0(U_237),bit1(U_235))
| ~ ord_less_eq(int,U_237,U_235) ),
inference(clausify,[status(thm)],[f_87_3]) ).
fof(f_88_1,plain,
! [K,L] :
( ( ord_less(int,bit0(K),bit1(L))
| ~ ord_less_eq(int,K,L) )
& ( ord_less_eq(int,K,L)
| ~ ord_less(int,bit0(K),bit1(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_60_rel__simps_I15_J]) ).
fof(f_88_2,plain,
! [U_239,U_238] :
( ( ord_less(int,bit0(U_239),bit1(U_238))
| ~ ord_less_eq(int,U_239,U_238) )
& ( ord_less_eq(int,U_239,U_238)
| ~ ord_less(int,bit0(U_239),bit1(U_238)) ) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
fof(f_88_3,plain,
( ! [U_243,U_241] :
( ord_less(int,bit0(U_243),bit1(U_241))
| ~ ord_less_eq(int,U_243,U_241) )
& ! [U_242,U_240] :
( ord_less_eq(int,U_242,U_240)
| ~ ord_less(int,bit0(U_242),bit1(U_240)) ) ),
inference(miniscope,[status(thm)],[f_88_2]) ).
cnf(f_88_4,plain,
( ord_less_eq(int,U_242,U_240)
| ~ ord_less(int,bit0(U_242),bit1(U_240)) ),
inference(clausify,[status(thm)],[f_88_3]) ).
cnf(f_88_5,plain,
( ord_less(int,bit0(U_243),bit1(U_241))
| ~ ord_less_eq(int,U_243,U_241) ),
inference(clausify,[status(thm)],[f_88_3]) ).
fof(f_89_1,plain,
! [W,Z] :
( ord_less_eq(int,plus_plus(int,W,one_one(int)),Z)
| ~ ord_less(int,W,Z) ),
inference(fof_nnf,[status(thm)],[fact_61_zless__imp__add1__zle]) ).
fof(f_89_2,plain,
! [U_245,U_244] :
( ord_less_eq(int,plus_plus(int,U_245,one_one(int)),U_244)
| ~ ord_less(int,U_245,U_244) ),
inference(variable_rename,[status(thm)],[f_89_1]) ).
cnf(f_89_3,plain,
( ord_less_eq(int,plus_plus(int,U_245,one_one(int)),U_244)
| ~ ord_less(int,U_245,U_244) ),
inference(clausify,[status(thm)],[f_89_2]) ).
fof(f_90_1,plain,
! [W_1,Z_1] :
( ( ord_less_eq(int,plus_plus(int,W_1,one_one(int)),Z_1)
| ~ ord_less(int,W_1,Z_1) )
& ( ord_less(int,W_1,Z_1)
| ~ ord_less_eq(int,plus_plus(int,W_1,one_one(int)),Z_1) ) ),
inference(fof_nnf,[status(thm)],[fact_62_add1__zle__eq]) ).
fof(f_90_2,plain,
! [U_247,U_246] :
( ( ord_less_eq(int,plus_plus(int,U_247,one_one(int)),U_246)
| ~ ord_less(int,U_247,U_246) )
& ( ord_less(int,U_247,U_246)
| ~ ord_less_eq(int,plus_plus(int,U_247,one_one(int)),U_246) ) ),
inference(variable_rename,[status(thm)],[f_90_1]) ).
fof(f_90_3,plain,
( ! [U_251,U_249] :
( ord_less_eq(int,plus_plus(int,U_251,one_one(int)),U_249)
| ~ ord_less(int,U_251,U_249) )
& ! [U_250,U_248] :
( ord_less(int,U_250,U_248)
| ~ ord_less_eq(int,plus_plus(int,U_250,one_one(int)),U_248) ) ),
inference(miniscope,[status(thm)],[f_90_2]) ).
cnf(f_90_4,plain,
( ord_less(int,U_250,U_248)
| ~ ord_less_eq(int,plus_plus(int,U_250,one_one(int)),U_248) ),
inference(clausify,[status(thm)],[f_90_3]) ).
cnf(f_90_5,plain,
( ord_less_eq(int,plus_plus(int,U_251,one_one(int)),U_249)
| ~ ord_less(int,U_251,U_249) ),
inference(clausify,[status(thm)],[f_90_3]) ).
fof(f_91_1,plain,
! [W_1,Z_1] :
( ( ord_less(int,W_1,plus_plus(int,Z_1,one_one(int)))
| ~ ord_less_eq(int,W_1,Z_1) )
& ( ord_less_eq(int,W_1,Z_1)
| ~ ord_less(int,W_1,plus_plus(int,Z_1,one_one(int))) ) ),
inference(fof_nnf,[status(thm)],[fact_63_zle__add1__eq__le]) ).
fof(f_91_2,plain,
! [U_253,U_252] :
( ( ord_less(int,U_253,plus_plus(int,U_252,one_one(int)))
| ~ ord_less_eq(int,U_253,U_252) )
& ( ord_less_eq(int,U_253,U_252)
| ~ ord_less(int,U_253,plus_plus(int,U_252,one_one(int))) ) ),
inference(variable_rename,[status(thm)],[f_91_1]) ).
fof(f_91_3,plain,
( ! [U_257,U_255] :
( ord_less(int,U_257,plus_plus(int,U_255,one_one(int)))
| ~ ord_less_eq(int,U_257,U_255) )
& ! [U_256,U_254] :
( ord_less_eq(int,U_256,U_254)
| ~ ord_less(int,U_256,plus_plus(int,U_254,one_one(int))) ) ),
inference(miniscope,[status(thm)],[f_91_2]) ).
cnf(f_91_4,plain,
( ord_less_eq(int,U_256,U_254)
| ~ ord_less(int,U_256,plus_plus(int,U_254,one_one(int))) ),
inference(clausify,[status(thm)],[f_91_3]) ).
cnf(f_91_5,plain,
( ord_less(int,U_257,plus_plus(int,U_255,one_one(int)))
| ~ ord_less_eq(int,U_257,U_255) ),
inference(clausify,[status(thm)],[f_91_3]) ).
fof(f_92_1,plain,
zprime(number_number_of(int,bit0(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_64_zprime__2]) ).
cnf(f_92_2,plain,
zprime(number_number_of(int,bit0(bit1(pls)))),
inference(clausify,[status(thm)],[f_92_1]) ).
fof(f_93_1,plain,
! [Y_1,X_1] :
( twoSqu33214720sum2sq(times_times(int,X_1,Y_1))
| ~ twoSqu33214720sum2sq(Y_1)
| ~ twoSqu33214720sum2sq(X_1) ),
inference(fof_nnf,[status(thm)],[fact_65_is__mult__sum2sq]) ).
fof(f_93_2,plain,
! [U_259,U_258] :
( twoSqu33214720sum2sq(times_times(int,U_258,U_259))
| ~ twoSqu33214720sum2sq(U_259)
| ~ twoSqu33214720sum2sq(U_258) ),
inference(variable_rename,[status(thm)],[f_93_1]) ).
cnf(f_93_3,plain,
( twoSqu33214720sum2sq(times_times(int,U_258,U_259))
| ~ twoSqu33214720sum2sq(U_259)
| ~ twoSqu33214720sum2sq(U_258) ),
inference(clausify,[status(thm)],[f_93_2]) ).
fof(f_94_1,plain,
! [X_a] :
( ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,times_times(X_a,Lx,Rx),times_times(X_a,Ly,Ry))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_66_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J]) ).
fof(f_94_2,plain,
! [U_264] :
( ! [U_263,U_262,U_261,U_260] : times_times(U_264,times_times(U_264,U_263,U_262),times_times(U_264,U_261,U_260)) = times_times(U_264,times_times(U_264,U_263,U_261),times_times(U_264,U_262,U_260))
| ~ comm_semiring_1(U_264) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
cnf(f_94_3,plain,
( times_times(U_264,times_times(U_264,U_263,U_262),times_times(U_264,U_261,U_260)) = times_times(U_264,times_times(U_264,U_263,U_261),times_times(U_264,U_262,U_260))
| ~ comm_semiring_1(U_264) ),
inference(clausify,[status(thm)],[f_94_2]) ).
fof(f_95_1,plain,
! [X_a] :
( ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,Rx,times_times(X_a,times_times(X_a,Lx,Ly),Ry))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_67_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J]) ).
fof(f_95_2,plain,
! [U_269] :
( ! [U_268,U_267,U_266,U_265] : times_times(U_269,times_times(U_269,U_268,U_267),times_times(U_269,U_266,U_265)) = times_times(U_269,U_266,times_times(U_269,times_times(U_269,U_268,U_267),U_265))
| ~ comm_semiring_1(U_269) ),
inference(variable_rename,[status(thm)],[f_95_1]) ).
cnf(f_95_3,plain,
( times_times(U_269,times_times(U_269,U_268,U_267),times_times(U_269,U_266,U_265)) = times_times(U_269,U_266,times_times(U_269,times_times(U_269,U_268,U_267),U_265))
| ~ comm_semiring_1(U_269) ),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_96_1,plain,
! [X_a] :
( ! [Lx,Ly,Rx,Ry] : times_times(X_a,times_times(X_a,Lx,Ly),times_times(X_a,Rx,Ry)) = times_times(X_a,Lx,times_times(X_a,Ly,times_times(X_a,Rx,Ry)))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_68_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J]) ).
fof(f_96_2,plain,
! [U_274] :
( ! [U_273,U_272,U_271,U_270] : times_times(U_274,times_times(U_274,U_273,U_272),times_times(U_274,U_271,U_270)) = times_times(U_274,U_273,times_times(U_274,U_272,times_times(U_274,U_271,U_270)))
| ~ comm_semiring_1(U_274) ),
inference(variable_rename,[status(thm)],[f_96_1]) ).
cnf(f_96_3,plain,
( times_times(U_274,times_times(U_274,U_273,U_272),times_times(U_274,U_271,U_270)) = times_times(U_274,U_273,times_times(U_274,U_272,times_times(U_274,U_271,U_270)))
| ~ comm_semiring_1(U_274) ),
inference(clausify,[status(thm)],[f_96_2]) ).
fof(f_97_1,plain,
! [X_a] :
( ! [Lx,Ly,Rx] : times_times(X_a,times_times(X_a,Lx,Ly),Rx) = times_times(X_a,times_times(X_a,Lx,Rx),Ly)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_69_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J]) ).
fof(f_97_2,plain,
! [U_278] :
( ! [U_277,U_276,U_275] : times_times(U_278,times_times(U_278,U_277,U_276),U_275) = times_times(U_278,times_times(U_278,U_277,U_275),U_276)
| ~ comm_semiring_1(U_278) ),
inference(variable_rename,[status(thm)],[f_97_1]) ).
cnf(f_97_3,plain,
( times_times(U_278,times_times(U_278,U_277,U_276),U_275) = times_times(U_278,times_times(U_278,U_277,U_275),U_276)
| ~ comm_semiring_1(U_278) ),
inference(clausify,[status(thm)],[f_97_2]) ).
fof(f_98_1,plain,
! [X_a] :
( ! [Lx,Ly,Rx] : times_times(X_a,times_times(X_a,Lx,Ly),Rx) = times_times(X_a,Lx,times_times(X_a,Ly,Rx))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_70_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J]) ).
fof(f_98_2,plain,
! [U_282] :
( ! [U_281,U_280,U_279] : times_times(U_282,times_times(U_282,U_281,U_280),U_279) = times_times(U_282,U_281,times_times(U_282,U_280,U_279))
| ~ comm_semiring_1(U_282) ),
inference(variable_rename,[status(thm)],[f_98_1]) ).
cnf(f_98_3,plain,
( times_times(U_282,times_times(U_282,U_281,U_280),U_279) = times_times(U_282,U_281,times_times(U_282,U_280,U_279))
| ~ comm_semiring_1(U_282) ),
inference(clausify,[status(thm)],[f_98_2]) ).
fof(f_99_1,plain,
! [X_a] :
( ! [Lx,Rx,Ry] : times_times(X_a,Lx,times_times(X_a,Rx,Ry)) = times_times(X_a,times_times(X_a,Lx,Rx),Ry)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_71_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J]) ).
fof(f_99_2,plain,
! [U_286] :
( ! [U_285,U_284,U_283] : times_times(U_286,U_285,times_times(U_286,U_284,U_283)) = times_times(U_286,times_times(U_286,U_285,U_284),U_283)
| ~ comm_semiring_1(U_286) ),
inference(variable_rename,[status(thm)],[f_99_1]) ).
cnf(f_99_3,plain,
( times_times(U_286,U_285,times_times(U_286,U_284,U_283)) = times_times(U_286,times_times(U_286,U_285,U_284),U_283)
| ~ comm_semiring_1(U_286) ),
inference(clausify,[status(thm)],[f_99_2]) ).
fof(f_100_1,plain,
! [X_a] :
( ! [Lx,Rx,Ry] : times_times(X_a,Lx,times_times(X_a,Rx,Ry)) = times_times(X_a,Rx,times_times(X_a,Lx,Ry))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_72_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J]) ).
fof(f_100_2,plain,
! [U_290] :
( ! [U_289,U_288,U_287] : times_times(U_290,U_289,times_times(U_290,U_288,U_287)) = times_times(U_290,U_288,times_times(U_290,U_289,U_287))
| ~ comm_semiring_1(U_290) ),
inference(variable_rename,[status(thm)],[f_100_1]) ).
cnf(f_100_3,plain,
( times_times(U_290,U_289,times_times(U_290,U_288,U_287)) = times_times(U_290,U_288,times_times(U_290,U_289,U_287))
| ~ comm_semiring_1(U_290) ),
inference(clausify,[status(thm)],[f_100_2]) ).
fof(f_101_1,plain,
! [X_a] :
( ! [A_1,B] : times_times(X_a,A_1,B) = times_times(X_a,B,A_1)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_73_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J]) ).
fof(f_101_2,plain,
! [U_293] :
( ! [U_292,U_291] : times_times(U_293,U_292,U_291) = times_times(U_293,U_291,U_292)
| ~ comm_semiring_1(U_293) ),
inference(variable_rename,[status(thm)],[f_101_1]) ).
cnf(f_101_3,plain,
( times_times(U_293,U_292,U_291) = times_times(U_293,U_291,U_292)
| ~ comm_semiring_1(U_293) ),
inference(clausify,[status(thm)],[f_101_2]) ).
fof(f_102_1,plain,
! [X_a] :
( ! [A_1,B,C,D] : plus_plus(X_a,plus_plus(X_a,A_1,B),plus_plus(X_a,C,D)) = plus_plus(X_a,plus_plus(X_a,A_1,C),plus_plus(X_a,B,D))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_74_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J]) ).
fof(f_102_2,plain,
! [U_298] :
( ! [U_297,U_296,U_295,U_294] : plus_plus(U_298,plus_plus(U_298,U_297,U_296),plus_plus(U_298,U_295,U_294)) = plus_plus(U_298,plus_plus(U_298,U_297,U_295),plus_plus(U_298,U_296,U_294))
| ~ comm_semiring_1(U_298) ),
inference(variable_rename,[status(thm)],[f_102_1]) ).
cnf(f_102_3,plain,
( plus_plus(U_298,plus_plus(U_298,U_297,U_296),plus_plus(U_298,U_295,U_294)) = plus_plus(U_298,plus_plus(U_298,U_297,U_295),plus_plus(U_298,U_296,U_294))
| ~ comm_semiring_1(U_298) ),
inference(clausify,[status(thm)],[f_102_2]) ).
fof(f_103_1,plain,
! [X_a] :
( ! [A_1,B,C] : plus_plus(X_a,plus_plus(X_a,A_1,B),C) = plus_plus(X_a,plus_plus(X_a,A_1,C),B)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_75_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J]) ).
fof(f_103_2,plain,
! [U_302] :
( ! [U_301,U_300,U_299] : plus_plus(U_302,plus_plus(U_302,U_301,U_300),U_299) = plus_plus(U_302,plus_plus(U_302,U_301,U_299),U_300)
| ~ comm_semiring_1(U_302) ),
inference(variable_rename,[status(thm)],[f_103_1]) ).
cnf(f_103_3,plain,
( plus_plus(U_302,plus_plus(U_302,U_301,U_300),U_299) = plus_plus(U_302,plus_plus(U_302,U_301,U_299),U_300)
| ~ comm_semiring_1(U_302) ),
inference(clausify,[status(thm)],[f_103_2]) ).
fof(f_104_1,plain,
! [X_a] :
( ! [A_1,B,C] : plus_plus(X_a,plus_plus(X_a,A_1,B),C) = plus_plus(X_a,A_1,plus_plus(X_a,B,C))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J]) ).
fof(f_104_2,plain,
! [U_306] :
( ! [U_305,U_304,U_303] : plus_plus(U_306,plus_plus(U_306,U_305,U_304),U_303) = plus_plus(U_306,U_305,plus_plus(U_306,U_304,U_303))
| ~ comm_semiring_1(U_306) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
cnf(f_104_3,plain,
( plus_plus(U_306,plus_plus(U_306,U_305,U_304),U_303) = plus_plus(U_306,U_305,plus_plus(U_306,U_304,U_303))
| ~ comm_semiring_1(U_306) ),
inference(clausify,[status(thm)],[f_104_2]) ).
fof(f_105_1,plain,
! [X_a] :
( ! [A_1,C,D] : plus_plus(X_a,A_1,plus_plus(X_a,C,D)) = plus_plus(X_a,plus_plus(X_a,A_1,C),D)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J]) ).
fof(f_105_2,plain,
! [U_310] :
( ! [U_309,U_308,U_307] : plus_plus(U_310,U_309,plus_plus(U_310,U_308,U_307)) = plus_plus(U_310,plus_plus(U_310,U_309,U_308),U_307)
| ~ comm_semiring_1(U_310) ),
inference(variable_rename,[status(thm)],[f_105_1]) ).
cnf(f_105_3,plain,
( plus_plus(U_310,U_309,plus_plus(U_310,U_308,U_307)) = plus_plus(U_310,plus_plus(U_310,U_309,U_308),U_307)
| ~ comm_semiring_1(U_310) ),
inference(clausify,[status(thm)],[f_105_2]) ).
fof(f_106_1,plain,
! [X_a] :
( ! [A_1,C,D] : plus_plus(X_a,A_1,plus_plus(X_a,C,D)) = plus_plus(X_a,C,plus_plus(X_a,A_1,D))
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J]) ).
fof(f_106_2,plain,
! [U_314] :
( ! [U_313,U_312,U_311] : plus_plus(U_314,U_313,plus_plus(U_314,U_312,U_311)) = plus_plus(U_314,U_312,plus_plus(U_314,U_313,U_311))
| ~ comm_semiring_1(U_314) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
cnf(f_106_3,plain,
( plus_plus(U_314,U_313,plus_plus(U_314,U_312,U_311)) = plus_plus(U_314,U_312,plus_plus(U_314,U_313,U_311))
| ~ comm_semiring_1(U_314) ),
inference(clausify,[status(thm)],[f_106_2]) ).
fof(f_107_1,plain,
! [X_a] :
( ! [A_1,C] : plus_plus(X_a,A_1,C) = plus_plus(X_a,C,A_1)
| ~ comm_semiring_1(X_a) ),
inference(fof_nnf,[status(thm)],[fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J]) ).
fof(f_107_2,plain,
! [U_317] :
( ! [U_316,U_315] : plus_plus(U_317,U_316,U_315) = plus_plus(U_317,U_315,U_316)
| ~ comm_semiring_1(U_317) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
cnf(f_107_3,plain,
( plus_plus(U_317,U_316,U_315) = plus_plus(U_317,U_315,U_316)
| ~ comm_semiring_1(U_317) ),
inference(clausify,[status(thm)],[f_107_2]) ).
fof(f_108_1,plain,
! [X_a] :
( ! [X_2,Y_2] :
( ( number_number_of(X_a,X_2) = number_number_of(X_a,Y_2)
| X_2 != Y_2 )
& ( X_2 = Y_2
| number_number_of(X_a,X_2) != number_number_of(X_a,Y_2) ) )
| ~ ring_char_0(X_a)
| ~ number_ring(X_a) ),
inference(fof_nnf,[status(thm)],[fact_80_eq__number__of]) ).
fof(f_108_2,plain,
! [U_320] :
( ! [U_319,U_318] :
( ( number_number_of(U_320,U_319) = number_number_of(U_320,U_318)
| U_319 != U_318 )
& ( U_319 = U_318
| number_number_of(U_320,U_319) != number_number_of(U_320,U_318) ) )
| ~ ring_char_0(U_320)
| ~ number_ring(U_320) ),
inference(variable_rename,[status(thm)],[f_108_1]) ).
fof(f_108_3,plain,
! [U_320] :
( ( ! [U_324,U_322] :
( number_number_of(U_320,U_324) = number_number_of(U_320,U_322)
| U_324 != U_322 )
& ! [U_323,U_321] :
( U_323 = U_321
| number_number_of(U_320,U_323) != number_number_of(U_320,U_321) ) )
| ~ ring_char_0(U_320)
| ~ number_ring(U_320) ),
inference(miniscope,[status(thm)],[f_108_2]) ).
cnf(f_108_4,plain,
( U_323 = U_321
| number_number_of(U_320,U_323) != number_number_of(U_320,U_321)
| ~ ring_char_0(U_320)
| ~ number_ring(U_320) ),
inference(clausify,[status(thm)],[f_108_3]) ).
cnf(f_108_5,plain,
( number_number_of(U_320,U_324) = number_number_of(U_320,U_322)
| U_324 != U_322
| ~ ring_char_0(U_320)
| ~ number_ring(U_320) ),
inference(clausify,[status(thm)],[f_108_3]) ).
fof(f_109_1,plain,
! [X_a] :
( ! [W_1,X_2] :
( ( number_number_of(X_a,W_1) = ti(X_a,X_2)
| ti(X_a,X_2) != number_number_of(X_a,W_1) )
& ( ti(X_a,X_2) = number_number_of(X_a,W_1)
| number_number_of(X_a,W_1) != ti(X_a,X_2) ) )
| ~ number(X_a) ),
inference(fof_nnf,[status(thm)],[fact_81_number__of__reorient]) ).
fof(f_109_2,plain,
! [U_327] :
( ! [U_326,U_325] :
( ( number_number_of(U_327,U_326) = ti(U_327,U_325)
| ti(U_327,U_325) != number_number_of(U_327,U_326) )
& ( ti(U_327,U_325) = number_number_of(U_327,U_326)
| number_number_of(U_327,U_326) != ti(U_327,U_325) ) )
| ~ number(U_327) ),
inference(variable_rename,[status(thm)],[f_109_1]) ).
fof(f_109_3,plain,
! [U_327] :
( ( ! [U_331,U_329] :
( number_number_of(U_327,U_331) = ti(U_327,U_329)
| ti(U_327,U_329) != number_number_of(U_327,U_331) )
& ! [U_330,U_328] :
( ti(U_327,U_328) = number_number_of(U_327,U_330)
| number_number_of(U_327,U_330) != ti(U_327,U_328) ) )
| ~ number(U_327) ),
inference(miniscope,[status(thm)],[f_109_2]) ).
cnf(f_109_4,plain,
( ti(U_327,U_328) = number_number_of(U_327,U_330)
| number_number_of(U_327,U_330) != ti(U_327,U_328)
| ~ number(U_327) ),
inference(clausify,[status(thm)],[f_109_3]) ).
cnf(f_109_5,plain,
( number_number_of(U_327,U_331) = ti(U_327,U_329)
| ti(U_327,U_329) != number_number_of(U_327,U_331)
| ~ number(U_327) ),
inference(clausify,[status(thm)],[f_109_3]) ).
fof(f_110_1,plain,
! [K,L] :
( ( bit1(K) = bit1(L)
| K != L )
& ( K = L
| bit1(K) != bit1(L) ) ),
inference(fof_nnf,[status(thm)],[fact_82_rel__simps_I51_J]) ).
fof(f_110_2,plain,
! [U_333,U_332] :
( ( bit1(U_333) = bit1(U_332)
| U_333 != U_332 )
& ( U_333 = U_332
| bit1(U_333) != bit1(U_332) ) ),
inference(variable_rename,[status(thm)],[f_110_1]) ).
fof(f_110_3,plain,
( ! [U_337,U_335] :
( bit1(U_337) = bit1(U_335)
| U_337 != U_335 )
& ! [U_336,U_334] :
( U_336 = U_334
| bit1(U_336) != bit1(U_334) ) ),
inference(miniscope,[status(thm)],[f_110_2]) ).
cnf(f_110_4,plain,
( U_336 = U_334
| bit1(U_336) != bit1(U_334) ),
inference(clausify,[status(thm)],[f_110_3]) ).
cnf(f_110_5,plain,
( bit1(U_337) = bit1(U_335)
| U_337 != U_335 ),
inference(clausify,[status(thm)],[f_110_3]) ).
fof(f_111_1,plain,
! [K,L] :
( ( bit0(K) = bit0(L)
| K != L )
& ( K = L
| bit0(K) != bit0(L) ) ),
inference(fof_nnf,[status(thm)],[fact_83_rel__simps_I48_J]) ).
fof(f_111_2,plain,
! [U_339,U_338] :
( ( bit0(U_339) = bit0(U_338)
| U_339 != U_338 )
& ( U_339 = U_338
| bit0(U_339) != bit0(U_338) ) ),
inference(variable_rename,[status(thm)],[f_111_1]) ).
fof(f_111_3,plain,
( ! [U_343,U_341] :
( bit0(U_343) = bit0(U_341)
| U_343 != U_341 )
& ! [U_342,U_340] :
( U_342 = U_340
| bit0(U_342) != bit0(U_340) ) ),
inference(miniscope,[status(thm)],[f_111_2]) ).
cnf(f_111_4,plain,
( U_342 = U_340
| bit0(U_342) != bit0(U_340) ),
inference(clausify,[status(thm)],[f_111_3]) ).
cnf(f_111_5,plain,
( bit0(U_343) = bit0(U_341)
| U_343 != U_341 ),
inference(clausify,[status(thm)],[f_111_3]) ).
fof(f_112_1,plain,
! [Z1,Z2,Z3] : times_times(int,times_times(int,Z1,Z2),Z3) = times_times(int,Z1,times_times(int,Z2,Z3)),
inference(fof_nnf,[status(thm)],[fact_84_zmult__assoc]) ).
fof(f_112_2,plain,
! [U_346,U_345,U_344] : times_times(int,times_times(int,U_346,U_345),U_344) = times_times(int,U_346,times_times(int,U_345,U_344)),
inference(variable_rename,[status(thm)],[f_112_1]) ).
cnf(f_112_3,plain,
times_times(int,times_times(int,U_346,U_345),U_344) = times_times(int,U_346,times_times(int,U_345,U_344)),
inference(clausify,[status(thm)],[f_112_2]) ).
fof(f_113_1,plain,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
inference(fof_nnf,[status(thm)],[fact_85_zmult__commute]) ).
fof(f_113_2,plain,
! [U_348,U_347] : times_times(int,U_348,U_347) = times_times(int,U_347,U_348),
inference(variable_rename,[status(thm)],[f_113_1]) ).
cnf(f_113_3,plain,
times_times(int,U_348,U_347) = times_times(int,U_347,U_348),
inference(clausify,[status(thm)],[f_113_2]) ).
fof(f_114_1,plain,
! [K_1] : number_number_of(int,K_1) = K_1,
inference(fof_nnf,[status(thm)],[fact_86_number__of__is__id]) ).
fof(f_114_2,plain,
! [U_349] : number_number_of(int,U_349) = U_349,
inference(variable_rename,[status(thm)],[f_114_1]) ).
cnf(f_114_3,plain,
number_number_of(int,U_349) = U_349,
inference(clausify,[status(thm)],[f_114_2]) ).
fof(f_115_1,plain,
! [Z1,Z2,Z3] : plus_plus(int,plus_plus(int,Z1,Z2),Z3) = plus_plus(int,Z1,plus_plus(int,Z2,Z3)),
inference(fof_nnf,[status(thm)],[fact_87_zadd__assoc]) ).
fof(f_115_2,plain,
! [U_352,U_351,U_350] : plus_plus(int,plus_plus(int,U_352,U_351),U_350) = plus_plus(int,U_352,plus_plus(int,U_351,U_350)),
inference(variable_rename,[status(thm)],[f_115_1]) ).
cnf(f_115_3,plain,
plus_plus(int,plus_plus(int,U_352,U_351),U_350) = plus_plus(int,U_352,plus_plus(int,U_351,U_350)),
inference(clausify,[status(thm)],[f_115_2]) ).
fof(f_116_1,plain,
! [X_1,Y_1,Z] : plus_plus(int,X_1,plus_plus(int,Y_1,Z)) = plus_plus(int,Y_1,plus_plus(int,X_1,Z)),
inference(fof_nnf,[status(thm)],[fact_88_zadd__left__commute]) ).
fof(f_116_2,plain,
! [U_355,U_354,U_353] : plus_plus(int,U_355,plus_plus(int,U_354,U_353)) = plus_plus(int,U_354,plus_plus(int,U_355,U_353)),
inference(variable_rename,[status(thm)],[f_116_1]) ).
cnf(f_116_3,plain,
plus_plus(int,U_355,plus_plus(int,U_354,U_353)) = plus_plus(int,U_354,plus_plus(int,U_355,U_353)),
inference(clausify,[status(thm)],[f_116_2]) ).
fof(f_117_1,plain,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
inference(fof_nnf,[status(thm)],[fact_89_zadd__commute]) ).
fof(f_117_2,plain,
! [U_357,U_356] : plus_plus(int,U_357,U_356) = plus_plus(int,U_356,U_357),
inference(variable_rename,[status(thm)],[f_117_1]) ).
cnf(f_117_3,plain,
plus_plus(int,U_357,U_356) = plus_plus(int,U_356,U_357),
inference(clausify,[status(thm)],[f_117_2]) ).
fof(f_118_1,plain,
! [K] :
( ( ord_less(int,bit1(K),pls)
| ~ ord_less(int,K,pls) )
& ( ord_less(int,K,pls)
| ~ ord_less(int,bit1(K),pls) ) ),
inference(fof_nnf,[status(thm)],[fact_90_rel__simps_I12_J]) ).
fof(f_118_2,plain,
! [U_358] :
( ( ord_less(int,bit1(U_358),pls)
| ~ ord_less(int,U_358,pls) )
& ( ord_less(int,U_358,pls)
| ~ ord_less(int,bit1(U_358),pls) ) ),
inference(variable_rename,[status(thm)],[f_118_1]) ).
fof(f_118_3,plain,
( ! [U_360] :
( ord_less(int,bit1(U_360),pls)
| ~ ord_less(int,U_360,pls) )
& ! [U_359] :
( ord_less(int,U_359,pls)
| ~ ord_less(int,bit1(U_359),pls) ) ),
inference(miniscope,[status(thm)],[f_118_2]) ).
cnf(f_118_4,plain,
( ord_less(int,U_359,pls)
| ~ ord_less(int,bit1(U_359),pls) ),
inference(clausify,[status(thm)],[f_118_3]) ).
cnf(f_118_5,plain,
( ord_less(int,bit1(U_360),pls)
| ~ ord_less(int,U_360,pls) ),
inference(clausify,[status(thm)],[f_118_3]) ).
fof(f_119_1,plain,
! [K1,K2] :
( ( ord_less(int,bit1(K1),bit0(K2))
| ~ ord_less(int,K1,K2) )
& ( ord_less(int,K1,K2)
| ~ ord_less(int,bit1(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_91_less__int__code_I15_J]) ).
fof(f_119_2,plain,
! [U_362,U_361] :
( ( ord_less(int,bit1(U_362),bit0(U_361))
| ~ ord_less(int,U_362,U_361) )
& ( ord_less(int,U_362,U_361)
| ~ ord_less(int,bit1(U_362),bit0(U_361)) ) ),
inference(variable_rename,[status(thm)],[f_119_1]) ).
fof(f_119_3,plain,
( ! [U_366,U_364] :
( ord_less(int,bit1(U_366),bit0(U_364))
| ~ ord_less(int,U_366,U_364) )
& ! [U_365,U_363] :
( ord_less(int,U_365,U_363)
| ~ ord_less(int,bit1(U_365),bit0(U_363)) ) ),
inference(miniscope,[status(thm)],[f_119_2]) ).
cnf(f_119_4,plain,
( ord_less(int,U_365,U_363)
| ~ ord_less(int,bit1(U_365),bit0(U_363)) ),
inference(clausify,[status(thm)],[f_119_3]) ).
cnf(f_119_5,plain,
( ord_less(int,bit1(U_366),bit0(U_364))
| ~ ord_less(int,U_366,U_364) ),
inference(clausify,[status(thm)],[f_119_3]) ).
fof(f_120_1,plain,
! [K,L] :
( ( ord_less(int,bit1(K),bit0(L))
| ~ ord_less(int,K,L) )
& ( ord_less(int,K,L)
| ~ ord_less(int,bit1(K),bit0(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_92_rel__simps_I16_J]) ).
fof(f_120_2,plain,
! [U_368,U_367] :
( ( ord_less(int,bit1(U_368),bit0(U_367))
| ~ ord_less(int,U_368,U_367) )
& ( ord_less(int,U_368,U_367)
| ~ ord_less(int,bit1(U_368),bit0(U_367)) ) ),
inference(variable_rename,[status(thm)],[f_120_1]) ).
fof(f_120_3,plain,
( ! [U_372,U_370] :
( ord_less(int,bit1(U_372),bit0(U_370))
| ~ ord_less(int,U_372,U_370) )
& ! [U_371,U_369] :
( ord_less(int,U_371,U_369)
| ~ ord_less(int,bit1(U_371),bit0(U_369)) ) ),
inference(miniscope,[status(thm)],[f_120_2]) ).
cnf(f_120_4,plain,
( ord_less(int,U_371,U_369)
| ~ ord_less(int,bit1(U_371),bit0(U_369)) ),
inference(clausify,[status(thm)],[f_120_3]) ).
cnf(f_120_5,plain,
( ord_less(int,bit1(U_372),bit0(U_370))
| ~ ord_less(int,U_372,U_370) ),
inference(clausify,[status(thm)],[f_120_3]) ).
fof(f_121_1,plain,
! [K] :
( ( ord_less(int,bit0(K),pls)
| ~ ord_less(int,K,pls) )
& ( ord_less(int,K,pls)
| ~ ord_less(int,bit0(K),pls) ) ),
inference(fof_nnf,[status(thm)],[fact_93_rel__simps_I10_J]) ).
fof(f_121_2,plain,
! [U_373] :
( ( ord_less(int,bit0(U_373),pls)
| ~ ord_less(int,U_373,pls) )
& ( ord_less(int,U_373,pls)
| ~ ord_less(int,bit0(U_373),pls) ) ),
inference(variable_rename,[status(thm)],[f_121_1]) ).
fof(f_121_3,plain,
( ! [U_375] :
( ord_less(int,bit0(U_375),pls)
| ~ ord_less(int,U_375,pls) )
& ! [U_374] :
( ord_less(int,U_374,pls)
| ~ ord_less(int,bit0(U_374),pls) ) ),
inference(miniscope,[status(thm)],[f_121_2]) ).
cnf(f_121_4,plain,
( ord_less(int,U_374,pls)
| ~ ord_less(int,bit0(U_374),pls) ),
inference(clausify,[status(thm)],[f_121_3]) ).
cnf(f_121_5,plain,
( ord_less(int,bit0(U_375),pls)
| ~ ord_less(int,U_375,pls) ),
inference(clausify,[status(thm)],[f_121_3]) ).
fof(f_122_1,plain,
! [K] :
( ( ord_less(int,pls,bit0(K))
| ~ ord_less(int,pls,K) )
& ( ord_less(int,pls,K)
| ~ ord_less(int,pls,bit0(K)) ) ),
inference(fof_nnf,[status(thm)],[fact_94_rel__simps_I4_J]) ).
fof(f_122_2,plain,
! [U_376] :
( ( ord_less(int,pls,bit0(U_376))
| ~ ord_less(int,pls,U_376) )
& ( ord_less(int,pls,U_376)
| ~ ord_less(int,pls,bit0(U_376)) ) ),
inference(variable_rename,[status(thm)],[f_122_1]) ).
fof(f_122_3,plain,
( ! [U_378] :
( ord_less(int,pls,bit0(U_378))
| ~ ord_less(int,pls,U_378) )
& ! [U_377] :
( ord_less(int,pls,U_377)
| ~ ord_less(int,pls,bit0(U_377)) ) ),
inference(miniscope,[status(thm)],[f_122_2]) ).
cnf(f_122_4,plain,
( ord_less(int,pls,U_377)
| ~ ord_less(int,pls,bit0(U_377)) ),
inference(clausify,[status(thm)],[f_122_3]) ).
cnf(f_122_5,plain,
( ord_less(int,pls,bit0(U_378))
| ~ ord_less(int,pls,U_378) ),
inference(clausify,[status(thm)],[f_122_3]) ).
fof(f_123_1,plain,
! [K] :
( ( ord_less_eq(int,pls,bit1(K))
| ~ ord_less_eq(int,pls,K) )
& ( ord_less_eq(int,pls,K)
| ~ ord_less_eq(int,pls,bit1(K)) ) ),
inference(fof_nnf,[status(thm)],[fact_95_rel__simps_I22_J]) ).
fof(f_123_2,plain,
! [U_379] :
( ( ord_less_eq(int,pls,bit1(U_379))
| ~ ord_less_eq(int,pls,U_379) )
& ( ord_less_eq(int,pls,U_379)
| ~ ord_less_eq(int,pls,bit1(U_379)) ) ),
inference(variable_rename,[status(thm)],[f_123_1]) ).
fof(f_123_3,plain,
( ! [U_381] :
( ord_less_eq(int,pls,bit1(U_381))
| ~ ord_less_eq(int,pls,U_381) )
& ! [U_380] :
( ord_less_eq(int,pls,U_380)
| ~ ord_less_eq(int,pls,bit1(U_380)) ) ),
inference(miniscope,[status(thm)],[f_123_2]) ).
cnf(f_123_4,plain,
( ord_less_eq(int,pls,U_380)
| ~ ord_less_eq(int,pls,bit1(U_380)) ),
inference(clausify,[status(thm)],[f_123_3]) ).
cnf(f_123_5,plain,
( ord_less_eq(int,pls,bit1(U_381))
| ~ ord_less_eq(int,pls,U_381) ),
inference(clausify,[status(thm)],[f_123_3]) ).
fof(f_124_1,plain,
! [K1,K2] :
( ( ord_less_eq(int,bit0(K1),bit1(K2))
| ~ ord_less_eq(int,K1,K2) )
& ( ord_less_eq(int,K1,K2)
| ~ ord_less_eq(int,bit0(K1),bit1(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_96_less__eq__int__code_I14_J]) ).
fof(f_124_2,plain,
! [U_383,U_382] :
( ( ord_less_eq(int,bit0(U_383),bit1(U_382))
| ~ ord_less_eq(int,U_383,U_382) )
& ( ord_less_eq(int,U_383,U_382)
| ~ ord_less_eq(int,bit0(U_383),bit1(U_382)) ) ),
inference(variable_rename,[status(thm)],[f_124_1]) ).
fof(f_124_3,plain,
( ! [U_387,U_385] :
( ord_less_eq(int,bit0(U_387),bit1(U_385))
| ~ ord_less_eq(int,U_387,U_385) )
& ! [U_386,U_384] :
( ord_less_eq(int,U_386,U_384)
| ~ ord_less_eq(int,bit0(U_386),bit1(U_384)) ) ),
inference(miniscope,[status(thm)],[f_124_2]) ).
cnf(f_124_4,plain,
( ord_less_eq(int,U_386,U_384)
| ~ ord_less_eq(int,bit0(U_386),bit1(U_384)) ),
inference(clausify,[status(thm)],[f_124_3]) ).
cnf(f_124_5,plain,
( ord_less_eq(int,bit0(U_387),bit1(U_385))
| ~ ord_less_eq(int,U_387,U_385) ),
inference(clausify,[status(thm)],[f_124_3]) ).
fof(f_125_1,plain,
! [K,L] :
( ( ord_less_eq(int,bit0(K),bit1(L))
| ~ ord_less_eq(int,K,L) )
& ( ord_less_eq(int,K,L)
| ~ ord_less_eq(int,bit0(K),bit1(L)) ) ),
inference(fof_nnf,[status(thm)],[fact_97_rel__simps_I32_J]) ).
fof(f_125_2,plain,
! [U_389,U_388] :
( ( ord_less_eq(int,bit0(U_389),bit1(U_388))
| ~ ord_less_eq(int,U_389,U_388) )
& ( ord_less_eq(int,U_389,U_388)
| ~ ord_less_eq(int,bit0(U_389),bit1(U_388)) ) ),
inference(variable_rename,[status(thm)],[f_125_1]) ).
fof(f_125_3,plain,
( ! [U_393,U_391] :
( ord_less_eq(int,bit0(U_393),bit1(U_391))
| ~ ord_less_eq(int,U_393,U_391) )
& ! [U_392,U_390] :
( ord_less_eq(int,U_392,U_390)
| ~ ord_less_eq(int,bit0(U_392),bit1(U_390)) ) ),
inference(miniscope,[status(thm)],[f_125_2]) ).
cnf(f_125_4,plain,
( ord_less_eq(int,U_392,U_390)
| ~ ord_less_eq(int,bit0(U_392),bit1(U_390)) ),
inference(clausify,[status(thm)],[f_125_3]) ).
cnf(f_125_5,plain,
( ord_less_eq(int,bit0(U_393),bit1(U_391))
| ~ ord_less_eq(int,U_393,U_391) ),
inference(clausify,[status(thm)],[f_125_3]) ).
fof(f_126_1,plain,
linordered_idom(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Rings_Olinordered__idom]) ).
cnf(f_126_2,plain,
linordered_idom(int),
inference(clausify,[status(thm)],[f_126_1]) ).
fof(f_127_1,plain,
comm_semiring_1(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Rings_Ocomm__semiring__1]) ).
cnf(f_127_2,plain,
comm_semiring_1(int),
inference(clausify,[status(thm)],[f_127_1]) ).
fof(f_128_1,plain,
number_semiring(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Int_Onumber__semiring]) ).
cnf(f_128_2,plain,
number_semiring(int),
inference(clausify,[status(thm)],[f_128_1]) ).
fof(f_129_1,plain,
linorder(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Orderings_Olinorder]) ).
cnf(f_129_2,plain,
linorder(int),
inference(clausify,[status(thm)],[f_129_1]) ).
fof(f_130_1,plain,
monoid_mult(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Groups_Omonoid__mult]) ).
cnf(f_130_2,plain,
monoid_mult(int),
inference(clausify,[status(thm)],[f_130_1]) ).
fof(f_131_1,plain,
semiring_1(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Rings_Osemiring__1]) ).
cnf(f_131_2,plain,
semiring_1(int),
inference(clausify,[status(thm)],[f_131_1]) ).
fof(f_132_1,plain,
ring_char_0(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Int_Oring__char__0]) ).
cnf(f_132_2,plain,
ring_char_0(int),
inference(clausify,[status(thm)],[f_132_1]) ).
fof(f_133_1,plain,
number_ring(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Int_Onumber__ring]) ).
cnf(f_133_2,plain,
number_ring(int),
inference(clausify,[status(thm)],[f_133_1]) ).
fof(f_134_1,plain,
number(int),
inference(fof_nnf,[status(thm)],[arity_Int_Oint___Int_Onumber]) ).
cnf(f_134_2,plain,
number(int),
inference(clausify,[status(thm)],[f_134_1]) ).
fof(f_135_1,plain,
comm_semiring_1(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Rings_Ocomm__semiring__1]) ).
cnf(f_135_2,plain,
comm_semiring_1(nat),
inference(clausify,[status(thm)],[f_135_1]) ).
fof(f_136_1,plain,
number_semiring(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Int_Onumber__semiring]) ).
cnf(f_136_2,plain,
number_semiring(nat),
inference(clausify,[status(thm)],[f_136_1]) ).
fof(f_137_1,plain,
linorder(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Orderings_Olinorder]) ).
cnf(f_137_2,plain,
linorder(nat),
inference(clausify,[status(thm)],[f_137_1]) ).
fof(f_138_1,plain,
monoid_mult(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Groups_Omonoid__mult]) ).
cnf(f_138_2,plain,
monoid_mult(nat),
inference(clausify,[status(thm)],[f_138_1]) ).
fof(f_139_1,plain,
semiring_1(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Rings_Osemiring__1]) ).
cnf(f_139_2,plain,
semiring_1(nat),
inference(clausify,[status(thm)],[f_139_1]) ).
fof(f_140_1,plain,
number(nat),
inference(fof_nnf,[status(thm)],[arity_Nat_Onat___Int_Onumber]) ).
cnf(f_140_2,plain,
number(nat),
inference(clausify,[status(thm)],[f_140_1]) ).
fof(f_141_1,plain,
! [T,A] : ti(T,ti(T,A)) = ti(T,A),
inference(fof_nnf,[status(thm)],[help_ti_idem]) ).
fof(f_141_2,plain,
! [U_395,U_394] : ti(U_395,ti(U_395,U_394)) = ti(U_395,U_394),
inference(variable_rename,[status(thm)],[f_141_1]) ).
cnf(f_141_3,plain,
ti(U_395,ti(U_395,U_394)) = ti(U_395,U_394),
inference(clausify,[status(thm)],[f_141_2]) ).
fof(f_142_1,negated_conjecture,
~ ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(negate,[status(cth)],[conj_0]) ).
fof(f_142_2,negated_conjecture,
! [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(fof_nnf,[status(thm)],[f_142_1]) ).
fof(f_142_3,negated_conjecture,
! [U_397,U_396] : plus_plus(int,power_power(int,U_397,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_396,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(variable_rename,[status(thm)],[f_142_2]) ).
fof(f_142_4,negated_conjecture,
! [U_397,U_396] : plus_plus(int,power_power(int,U_397,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_396,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(definitional_conversion,[status(esa)],[f_142_3]) ).
cnf(f_142_5,negated_conjecture,
plus_plus(int,power_power(int,U_397,number_number_of(nat,bit0(bit1(pls)))),power_power(int,U_396,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(clausify,[status(thm)],[f_142_4]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( one_one(Eq_x_0) = one_one(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( ti(Eq_x_0,Eq_x_1) = ti(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( plus_plus(Eq_x_0,Eq_x_1,Eq_x_2) = plus_plus(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( times_times(Eq_x_0,Eq_x_1,Eq_x_2) = times_times(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( undefined(Eq_x_0) = undefined(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( bit0(Eq_x_0) = bit0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( bit1(Eq_x_0) = bit1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( number_number_of(Eq_x_0,Eq_x_1) = number_number_of(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( power_power(Eq_x_0,Eq_x_1,Eq_x_2) = power_power(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( semiring_1(Eq_y_0)
| ~ semiring_1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( comm_semiring_1(Eq_y_0)
| ~ comm_semiring_1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( monoid_mult(Eq_y_0)
| ~ monoid_mult(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( zprime(Eq_y_0)
| ~ zprime(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( number(Eq_y_0)
| ~ number(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( linorder(Eq_y_0)
| ~ linorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( ord_less(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ord_less(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( ord_less_eq(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ ord_less_eq(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( twoSqu33214720sum2sq(Eq_y_0)
| ~ twoSqu33214720sum2sq(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( number_semiring(Eq_y_0)
| ~ number_semiring(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( number_ring(Eq_y_0)
| ~ number_ring(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( linordered_idom(Eq_y_0)
| ~ linordered_idom(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( ring_char_0(Eq_y_0)
| ~ ring_char_0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 19:24:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.89/1.17 % SZS status Theorem for theBenchmark
% 0.89/1.17 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------