%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM926+1 : 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 : n006.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:36 AM UTC 2026
% Result : Theorem 0.93s 6.25s
% Output : Proof 0.93s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
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,
twoSqu526106917sum2sq(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_8,B_4] : power_power_int(plus_plus_int(A_8,B_4),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(A_8,number_number_of_nat(bit0(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),A_8),B_4)),power_power_int(B_4,number_number_of_nat(bit0(bit1(pls))))),
file('theBenchmark.p',fact_7_zadd__power2) ).
fof(fact_8_zadd__power3,axiom,
! [A_8,B_4] : power_power_int(plus_plus_int(A_8,B_4),number_number_of_nat(bit1(bit1(pls)))) = plus_plus_int(plus_plus_int(plus_plus_int(power_power_int(A_8,number_number_of_nat(bit1(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),power_power_int(A_8,number_number_of_nat(bit0(bit1(pls))))),B_4)),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),A_8),power_power_int(B_4,number_number_of_nat(bit0(bit1(pls)))))),power_power_int(B_4,number_number_of_nat(bit1(bit1(pls))))),
file('theBenchmark.p',fact_8_zadd__power3) ).
fof(fact_9_power2__sum,axiom,
! [X_2,Y_2] : power_power_nat(plus_plus_nat(X_2,Y_2),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(plus_plus_nat(power_power_nat(X_2,number_number_of_nat(bit0(bit1(pls)))),power_power_nat(Y_2,number_number_of_nat(bit0(bit1(pls))))),times_times_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))),X_2),Y_2)),
file('theBenchmark.p',fact_9_power2__sum) ).
fof(fact_10_power2__sum,axiom,
! [X_2,Y_2] : power_power_int(plus_plus_int(X_2,Y_2),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(X_2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_2,number_number_of_nat(bit0(bit1(pls))))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),X_2),Y_2)),
file('theBenchmark.p',fact_10_power2__sum) ).
fof(fact_11_power2__eq__square__number__of,axiom,
! [W_4] : power_power_int(number_number_of_int(W_4),number_number_of_nat(bit0(bit1(pls)))) = times_times_int(number_number_of_int(W_4),number_number_of_int(W_4)),
file('theBenchmark.p',fact_11_power2__eq__square__number__of) ).
fof(fact_12_power2__eq__square__number__of,axiom,
! [W_4] : power_power_nat(number_number_of_nat(W_4),number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(number_number_of_nat(W_4),number_number_of_nat(W_4)),
file('theBenchmark.p',fact_12_power2__eq__square__number__of) ).
fof(fact_13_cube__square,axiom,
! [A_8] : times_times_int(A_8,power_power_int(A_8,number_number_of_nat(bit0(bit1(pls))))) = power_power_int(A_8,number_number_of_nat(bit1(bit1(pls)))),
file('theBenchmark.p',fact_13_cube__square) ).
fof(fact_14_one__power2,axiom,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
file('theBenchmark.p',fact_14_one__power2) ).
fof(fact_15_one__power2,axiom,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
file('theBenchmark.p',fact_15_one__power2) ).
fof(fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
! [X_7] : times_times_int(X_7,X_7) = power_power_int(X_7,number_number_of_nat(bit0(bit1(pls)))),
file('theBenchmark.p',fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
fof(fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
! [X_7] : times_times_nat(X_7,X_7) = power_power_nat(X_7,number_number_of_nat(bit0(bit1(pls)))),
file('theBenchmark.p',fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
fof(fact_18_power2__eq__square,axiom,
! [A_7] : power_power_int(A_7,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(A_7,A_7),
file('theBenchmark.p',fact_18_power2__eq__square) ).
fof(fact_19_power2__eq__square,axiom,
! [A_7] : power_power_nat(A_7,number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(A_7,A_7),
file('theBenchmark.p',fact_19_power2__eq__square) ).
fof(fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
! [X_6,N] : power_power_int(X_6,times_times_nat(number_number_of_nat(bit0(bit1(pls))),N)) = times_times_int(power_power_int(X_6,N),power_power_int(X_6,N)),
file('theBenchmark.p',fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J) ).
fof(fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,axiom,
! [X_6,N] : power_power_nat(X_6,times_times_nat(number_number_of_nat(bit0(bit1(pls))),N)) = times_times_nat(power_power_nat(X_6,N),power_power_nat(X_6,N)),
file('theBenchmark.p',fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J) ).
fof(fact_22_add__special_I2_J,axiom,
! [W_3] : plus_plus_int(one_one_int,number_number_of_int(W_3)) = number_number_of_int(plus_plus_int(bit1(pls),W_3)),
file('theBenchmark.p',fact_22_add__special_I2_J) ).
fof(fact_23_add__special_I3_J,axiom,
! [V_3] : plus_plus_int(number_number_of_int(V_3),one_one_int) = number_number_of_int(plus_plus_int(V_3,bit1(pls))),
file('theBenchmark.p',fact_23_add__special_I3_J) ).
fof(fact_24_one__add__one__is__two,axiom,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
file('theBenchmark.p',fact_24_one__add__one__is__two) ).
fof(fact_25__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] : 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_25__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_26_zle__refl,axiom,
! [W] : ord_less_eq_int(W,W),
file('theBenchmark.p',fact_26_zle__refl) ).
fof(fact_27_zle__linear,axiom,
! [Z,W] :
( ord_less_eq_int(W,Z)
| ord_less_eq_int(Z,W) ),
file('theBenchmark.p',fact_27_zle__linear) ).
fof(fact_28_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_28_zless__le) ).
fof(fact_29_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_29_zless__linear) ).
fof(fact_30_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_30_zle__trans) ).
fof(fact_31_zle__antisym,axiom,
! [Z,W] :
( ord_less_eq_int(Z,W)
=> ( ord_less_eq_int(W,Z)
=> Z = W ) ),
file('theBenchmark.p',fact_31_zle__antisym) ).
fof(fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
! [X_5,P_1,Q_1] : power_power_int(power_power_int(X_5,P_1),Q_1) = power_power_int(X_5,times_times_nat(P_1,Q_1)),
file('theBenchmark.p',fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J) ).
fof(fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,axiom,
! [X_5,P_1,Q_1] : power_power_nat(power_power_nat(X_5,P_1),Q_1) = power_power_nat(X_5,times_times_nat(P_1,Q_1)),
file('theBenchmark.p',fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J) ).
fof(fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
! [X_4] : power_power_int(X_4,one_one_nat) = X_4,
file('theBenchmark.p',fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J) ).
fof(fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,axiom,
! [X_4] : power_power_nat(X_4,one_one_nat) = X_4,
file('theBenchmark.p',fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J) ).
fof(fact_36_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_36_zpower__zpower) ).
fof(fact_37_le__number__of__eq__not__less,axiom,
! [V_2,W_1] :
( ord_less_eq_nat(number_number_of_nat(V_2),number_number_of_nat(W_1))
<=> ~ ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_2)) ),
file('theBenchmark.p',fact_37_le__number__of__eq__not__less) ).
fof(fact_38_le__number__of__eq__not__less,axiom,
! [V_2,W_1] :
( ord_less_eq_int(number_number_of_int(V_2),number_number_of_int(W_1))
<=> ~ ord_less_int(number_number_of_int(W_1),number_number_of_int(V_2)) ),
file('theBenchmark.p',fact_38_le__number__of__eq__not__less) ).
fof(fact_39_less__number__of,axiom,
! [X_2,Y_2] :
( ord_less_int(number_number_of_int(X_2),number_number_of_int(Y_2))
<=> ord_less_int(X_2,Y_2) ),
file('theBenchmark.p',fact_39_less__number__of) ).
fof(fact_40_le__number__of,axiom,
! [X_2,Y_2] :
( ord_less_eq_int(number_number_of_int(X_2),number_number_of_int(Y_2))
<=> ord_less_eq_int(X_2,Y_2) ),
file('theBenchmark.p',fact_40_le__number__of) ).
fof(fact_41_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_41_zadd__zless__mono) ).
fof(fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
! [X_3,P,Q] : times_times_int(power_power_int(X_3,P),power_power_int(X_3,Q)) = power_power_int(X_3,plus_plus_nat(P,Q)),
file('theBenchmark.p',fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J) ).
fof(fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,axiom,
! [X_3,P,Q] : times_times_nat(power_power_nat(X_3,P),power_power_nat(X_3,Q)) = power_power_nat(X_3,plus_plus_nat(P,Q)),
file('theBenchmark.p',fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J) ).
fof(fact_44_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_44_zpower__zadd__distrib) ).
fof(fact_45_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_45_nat__mult__2) ).
fof(fact_46_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_46_nat__mult__2__right) ).
fof(fact_47_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_47_nat__1__add__1) ).
fof(fact_48_less__int__code_I16_J,axiom,
! [K1,K2] :
( ord_less_int(bit1(K1),bit1(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_48_less__int__code_I16_J) ).
fof(fact_49_rel__simps_I17_J,axiom,
! [K,L] :
( ord_less_int(bit1(K),bit1(L))
<=> ord_less_int(K,L) ),
file('theBenchmark.p',fact_49_rel__simps_I17_J) ).
fof(fact_50_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_50_less__eq__int__code_I16_J) ).
fof(fact_51_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_51_rel__simps_I34_J) ).
fof(fact_52_rel__simps_I2_J,axiom,
~ ord_less_int(pls,pls),
file('theBenchmark.p',fact_52_rel__simps_I2_J) ).
fof(fact_53_less__int__code_I13_J,axiom,
! [K1,K2] :
( ord_less_int(bit0(K1),bit0(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_53_less__int__code_I13_J) ).
fof(fact_54_rel__simps_I14_J,axiom,
! [K,L] :
( ord_less_int(bit0(K),bit0(L))
<=> ord_less_int(K,L) ),
file('theBenchmark.p',fact_54_rel__simps_I14_J) ).
fof(fact_55_rel__simps_I19_J,axiom,
ord_less_eq_int(pls,pls),
file('theBenchmark.p',fact_55_rel__simps_I19_J) ).
fof(fact_56_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_56_less__eq__int__code_I13_J) ).
fof(fact_57_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_57_rel__simps_I31_J) ).
fof(fact_58_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_58_less__number__of__int__code) ).
fof(fact_59_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_59_less__eq__number__of__int__code) ).
fof(fact_60_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_60_zadd__strict__right__mono) ).
fof(fact_61_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_61_zadd__left__mono) ).
fof(fact_62_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_62_add__nat__number__of) ).
fof(fact_63_nat__numeral__1__eq__1,axiom,
number_number_of_nat(bit1(pls)) = one_one_nat,
file('theBenchmark.p',fact_63_nat__numeral__1__eq__1) ).
fof(fact_64_Numeral1__eq1__nat,axiom,
one_one_nat = number_number_of_nat(bit1(pls)),
file('theBenchmark.p',fact_64_Numeral1__eq1__nat) ).
fof(fact_65_rel__simps_I29_J,axiom,
! [K] :
( ord_less_eq_int(bit1(K),pls)
<=> ord_less_int(K,pls) ),
file('theBenchmark.p',fact_65_rel__simps_I29_J) ).
fof(fact_66_rel__simps_I5_J,axiom,
! [K] :
( ord_less_int(pls,bit1(K))
<=> ord_less_eq_int(pls,K) ),
file('theBenchmark.p',fact_66_rel__simps_I5_J) ).
fof(fact_67_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_67_less__eq__int__code_I15_J) ).
fof(fact_68_rel__simps_I33_J,axiom,
! [K,L] :
( ord_less_eq_int(bit1(K),bit0(L))
<=> ord_less_int(K,L) ),
file('theBenchmark.p',fact_68_rel__simps_I33_J) ).
fof(fact_69_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_69_less__int__code_I14_J) ).
fof(fact_70_rel__simps_I15_J,axiom,
! [K,L] :
( ord_less_int(bit0(K),bit1(L))
<=> ord_less_eq_int(K,L) ),
file('theBenchmark.p',fact_70_rel__simps_I15_J) ).
fof(fact_71_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_71_zless__imp__add1__zle) ).
fof(fact_72_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_72_add1__zle__eq) ).
fof(fact_73_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_73_zle__add1__eq__le) ).
fof(fact_74_zprime__2,axiom,
zprime(number_number_of_int(bit0(bit1(pls)))),
file('theBenchmark.p',fact_74_zprime__2) ).
fof(fact_75_is__mult__sum2sq,axiom,
! [Y_1,X_1] :
( twoSqu526106917sum2sq(X_1)
=> ( twoSqu526106917sum2sq(Y_1)
=> twoSqu526106917sum2sq(times_times_int(X_1,Y_1)) ) ),
file('theBenchmark.p',fact_75_is__mult__sum2sq) ).
fof(fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
! [Lx_6,Ly_4,Rx_6,Ry_4] : times_times_int(times_times_int(Lx_6,Ly_4),times_times_int(Rx_6,Ry_4)) = times_times_int(times_times_int(Lx_6,Rx_6),times_times_int(Ly_4,Ry_4)),
file('theBenchmark.p',fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J) ).
fof(fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,axiom,
! [Lx_6,Ly_4,Rx_6,Ry_4] : times_times_nat(times_times_nat(Lx_6,Ly_4),times_times_nat(Rx_6,Ry_4)) = times_times_nat(times_times_nat(Lx_6,Rx_6),times_times_nat(Ly_4,Ry_4)),
file('theBenchmark.p',fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J) ).
fof(fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
! [Lx_5,Ly_3,Rx_5,Ry_3] : times_times_int(times_times_int(Lx_5,Ly_3),times_times_int(Rx_5,Ry_3)) = times_times_int(Rx_5,times_times_int(times_times_int(Lx_5,Ly_3),Ry_3)),
file('theBenchmark.p',fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J) ).
fof(fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,axiom,
! [Lx_5,Ly_3,Rx_5,Ry_3] : times_times_nat(times_times_nat(Lx_5,Ly_3),times_times_nat(Rx_5,Ry_3)) = times_times_nat(Rx_5,times_times_nat(times_times_nat(Lx_5,Ly_3),Ry_3)),
file('theBenchmark.p',fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J) ).
fof(fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
! [Lx_4,Ly_2,Rx_4,Ry_2] : times_times_int(times_times_int(Lx_4,Ly_2),times_times_int(Rx_4,Ry_2)) = times_times_int(Lx_4,times_times_int(Ly_2,times_times_int(Rx_4,Ry_2))),
file('theBenchmark.p',fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J) ).
fof(fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,axiom,
! [Lx_4,Ly_2,Rx_4,Ry_2] : times_times_nat(times_times_nat(Lx_4,Ly_2),times_times_nat(Rx_4,Ry_2)) = times_times_nat(Lx_4,times_times_nat(Ly_2,times_times_nat(Rx_4,Ry_2))),
file('theBenchmark.p',fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J) ).
fof(fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
! [Lx_3,Ly_1,Rx_3] : times_times_int(times_times_int(Lx_3,Ly_1),Rx_3) = times_times_int(times_times_int(Lx_3,Rx_3),Ly_1),
file('theBenchmark.p',fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J) ).
fof(fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,axiom,
! [Lx_3,Ly_1,Rx_3] : times_times_nat(times_times_nat(Lx_3,Ly_1),Rx_3) = times_times_nat(times_times_nat(Lx_3,Rx_3),Ly_1),
file('theBenchmark.p',fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J) ).
fof(fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
! [Lx_2,Ly,Rx_2] : times_times_int(times_times_int(Lx_2,Ly),Rx_2) = times_times_int(Lx_2,times_times_int(Ly,Rx_2)),
file('theBenchmark.p',fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
fof(fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,axiom,
! [Lx_2,Ly,Rx_2] : times_times_nat(times_times_nat(Lx_2,Ly),Rx_2) = times_times_nat(Lx_2,times_times_nat(Ly,Rx_2)),
file('theBenchmark.p',fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
fof(fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
! [Lx_1,Rx_1,Ry_1] : times_times_int(Lx_1,times_times_int(Rx_1,Ry_1)) = times_times_int(times_times_int(Lx_1,Rx_1),Ry_1),
file('theBenchmark.p',fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J) ).
fof(fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,axiom,
! [Lx_1,Rx_1,Ry_1] : times_times_nat(Lx_1,times_times_nat(Rx_1,Ry_1)) = times_times_nat(times_times_nat(Lx_1,Rx_1),Ry_1),
file('theBenchmark.p',fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J) ).
fof(fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
! [Lx,Rx,Ry] : times_times_int(Lx,times_times_int(Rx,Ry)) = times_times_int(Rx,times_times_int(Lx,Ry)),
file('theBenchmark.p',fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
! [Lx,Rx,Ry] : times_times_nat(Lx,times_times_nat(Rx,Ry)) = times_times_nat(Rx,times_times_nat(Lx,Ry)),
file('theBenchmark.p',fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
! [A_6,B_3] : times_times_int(A_6,B_3) = times_times_int(B_3,A_6),
file('theBenchmark.p',fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,axiom,
! [A_6,B_3] : times_times_nat(A_6,B_3) = times_times_nat(B_3,A_6),
file('theBenchmark.p',fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
fof(fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
! [A_5,B_2,C_5,D_2] : plus_plus_int(plus_plus_int(A_5,B_2),plus_plus_int(C_5,D_2)) = plus_plus_int(plus_plus_int(A_5,C_5),plus_plus_int(B_2,D_2)),
file('theBenchmark.p',fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J) ).
fof(fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,axiom,
! [A_5,B_2,C_5,D_2] : plus_plus_nat(plus_plus_nat(A_5,B_2),plus_plus_nat(C_5,D_2)) = plus_plus_nat(plus_plus_nat(A_5,C_5),plus_plus_nat(B_2,D_2)),
file('theBenchmark.p',fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J) ).
fof(fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
! [A_4,B_1,C_4] : plus_plus_int(plus_plus_int(A_4,B_1),C_4) = plus_plus_int(plus_plus_int(A_4,C_4),B_1),
file('theBenchmark.p',fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J) ).
fof(fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,axiom,
! [A_4,B_1,C_4] : plus_plus_nat(plus_plus_nat(A_4,B_1),C_4) = plus_plus_nat(plus_plus_nat(A_4,C_4),B_1),
file('theBenchmark.p',fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J) ).
fof(fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
! [A_3,B,C_3] : plus_plus_int(plus_plus_int(A_3,B),C_3) = plus_plus_int(A_3,plus_plus_int(B,C_3)),
file('theBenchmark.p',fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
fof(fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,axiom,
! [A_3,B,C_3] : plus_plus_nat(plus_plus_nat(A_3,B),C_3) = plus_plus_nat(A_3,plus_plus_nat(B,C_3)),
file('theBenchmark.p',fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
fof(fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
! [A_2,C_2,D_1] : plus_plus_int(A_2,plus_plus_int(C_2,D_1)) = plus_plus_int(plus_plus_int(A_2,C_2),D_1),
file('theBenchmark.p',fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
fof(fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,axiom,
! [A_2,C_2,D_1] : plus_plus_nat(A_2,plus_plus_nat(C_2,D_1)) = plus_plus_nat(plus_plus_nat(A_2,C_2),D_1),
file('theBenchmark.p',fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
fof(fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
! [A_1,C_1,D] : plus_plus_int(A_1,plus_plus_int(C_1,D)) = plus_plus_int(C_1,plus_plus_int(A_1,D)),
file('theBenchmark.p',fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,axiom,
! [A_1,C_1,D] : plus_plus_nat(A_1,plus_plus_nat(C_1,D)) = plus_plus_nat(C_1,plus_plus_nat(A_1,D)),
file('theBenchmark.p',fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
! [A,C] : plus_plus_int(A,C) = plus_plus_int(C,A),
file('theBenchmark.p',fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,axiom,
! [A,C] : plus_plus_nat(A,C) = plus_plus_nat(C,A),
file('theBenchmark.p',fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(fact_104_eq__number__of,axiom,
! [X_2,Y_2] :
( number_number_of_int(X_2) = number_number_of_int(Y_2)
<=> X_2 = Y_2 ),
file('theBenchmark.p',fact_104_eq__number__of) ).
fof(fact_105_number__of__reorient,axiom,
! [W_1,X_2] :
( number_number_of_nat(W_1) = X_2
<=> X_2 = number_number_of_nat(W_1) ),
file('theBenchmark.p',fact_105_number__of__reorient) ).
fof(fact_106_number__of__reorient,axiom,
! [W_1,X_2] :
( number_number_of_int(W_1) = X_2
<=> X_2 = number_number_of_int(W_1) ),
file('theBenchmark.p',fact_106_number__of__reorient) ).
fof(fact_107_rel__simps_I51_J,axiom,
! [K,L] :
( bit1(K) = bit1(L)
<=> K = L ),
file('theBenchmark.p',fact_107_rel__simps_I51_J) ).
fof(fact_108_rel__simps_I48_J,axiom,
! [K,L] :
( bit0(K) = bit0(L)
<=> K = L ),
file('theBenchmark.p',fact_108_rel__simps_I48_J) ).
fof(fact_109_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_109_zmult__assoc) ).
fof(fact_110_zmult__commute,axiom,
! [Z,W] : times_times_int(Z,W) = times_times_int(W,Z),
file('theBenchmark.p',fact_110_zmult__commute) ).
fof(fact_111_number__of__is__id,axiom,
! [K_1] : number_number_of_int(K_1) = K_1,
file('theBenchmark.p',fact_111_number__of__is__id) ).
fof(fact_112_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_112_zadd__assoc) ).
fof(fact_113_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_113_zadd__left__commute) ).
fof(fact_114_zadd__commute,axiom,
! [Z,W] : plus_plus_int(Z,W) = plus_plus_int(W,Z),
file('theBenchmark.p',fact_114_zadd__commute) ).
fof(fact_115_rel__simps_I12_J,axiom,
! [K] :
( ord_less_int(bit1(K),pls)
<=> ord_less_int(K,pls) ),
file('theBenchmark.p',fact_115_rel__simps_I12_J) ).
fof(fact_116_less__int__code_I15_J,axiom,
! [K1,K2] :
( ord_less_int(bit1(K1),bit0(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_116_less__int__code_I15_J) ).
fof(fact_117_rel__simps_I16_J,axiom,
! [K,L] :
( ord_less_int(bit1(K),bit0(L))
<=> ord_less_int(K,L) ),
file('theBenchmark.p',fact_117_rel__simps_I16_J) ).
fof(fact_118_rel__simps_I10_J,axiom,
! [K] :
( ord_less_int(bit0(K),pls)
<=> ord_less_int(K,pls) ),
file('theBenchmark.p',fact_118_rel__simps_I10_J) ).
fof(fact_119_rel__simps_I4_J,axiom,
! [K] :
( ord_less_int(pls,bit0(K))
<=> ord_less_int(pls,K) ),
file('theBenchmark.p',fact_119_rel__simps_I4_J) ).
fof(fact_120_rel__simps_I22_J,axiom,
! [K] :
( ord_less_eq_int(pls,bit1(K))
<=> ord_less_eq_int(pls,K) ),
file('theBenchmark.p',fact_120_rel__simps_I22_J) ).
fof(fact_121_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_121_less__eq__int__code_I14_J) ).
fof(fact_122_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_122_rel__simps_I32_J) ).
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,
ord_less_eq_int(one_one_int,t),
inference(fof_nnf,[status(thm)],[fact_0_tpos]) ).
cnf(f_1_2,plain,
ord_less_eq_int(one_one_int,t),
inference(clausify,[status(thm)],[f_1_1]) ).
fof(f_2_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_2_2,plain,
( ? [U_1,U_0] : plus_plus_int(power_power_int(U_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_0,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_2_1]) ).
fof(f_2_3,plain,
( ? [U_0] : plus_plus_int(power_power_int(sK1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_0,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_1,sK1)],[f_2_2]) ).
fof(f_2_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_0,sK2)],[f_2_3]) ).
cnf(f_2_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_2_4]) ).
fof(f_3_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_3_2,plain,
( ? [U_3,U_2] : plus_plus_int(power_power_int(U_3,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_2,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_3_1]) ).
fof(f_3_3,plain,
( ? [U_2] : plus_plus_int(power_power_int(sK3,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_2,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_3,sK3)],[f_3_2]) ).
fof(f_3_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_2,sK4)],[f_3_3]) ).
cnf(f_3_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_3_4]) ).
fof(f_4_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_4_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_4_1]) ).
fof(f_5_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_5_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_5_1]) ).
fof(f_6_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_6_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_6_1]) ).
fof(f_7_1,plain,
twoSqu526106917sum2sq(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_7_2,plain,
twoSqu526106917sum2sq(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_7_1]) ).
fof(f_8_1,plain,
! [A_8,B_4] : power_power_int(plus_plus_int(A_8,B_4),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(A_8,number_number_of_nat(bit0(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),A_8),B_4)),power_power_int(B_4,number_number_of_nat(bit0(bit1(pls))))),
inference(fof_nnf,[status(thm)],[fact_7_zadd__power2]) ).
fof(f_8_2,plain,
! [U_5,U_4] : power_power_int(plus_plus_int(U_5,U_4),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(U_5,number_number_of_nat(bit0(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),U_5),U_4)),power_power_int(U_4,number_number_of_nat(bit0(bit1(pls))))),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
power_power_int(plus_plus_int(U_5,U_4),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(U_5,number_number_of_nat(bit0(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),U_5),U_4)),power_power_int(U_4,number_number_of_nat(bit0(bit1(pls))))),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [A_8,B_4] : power_power_int(plus_plus_int(A_8,B_4),number_number_of_nat(bit1(bit1(pls)))) = plus_plus_int(plus_plus_int(plus_plus_int(power_power_int(A_8,number_number_of_nat(bit1(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),power_power_int(A_8,number_number_of_nat(bit0(bit1(pls))))),B_4)),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),A_8),power_power_int(B_4,number_number_of_nat(bit0(bit1(pls)))))),power_power_int(B_4,number_number_of_nat(bit1(bit1(pls))))),
inference(fof_nnf,[status(thm)],[fact_8_zadd__power3]) ).
fof(f_9_2,plain,
! [U_7,U_6] : power_power_int(plus_plus_int(U_7,U_6),number_number_of_nat(bit1(bit1(pls)))) = plus_plus_int(plus_plus_int(plus_plus_int(power_power_int(U_7,number_number_of_nat(bit1(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),power_power_int(U_7,number_number_of_nat(bit0(bit1(pls))))),U_6)),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),U_7),power_power_int(U_6,number_number_of_nat(bit0(bit1(pls)))))),power_power_int(U_6,number_number_of_nat(bit1(bit1(pls))))),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
power_power_int(plus_plus_int(U_7,U_6),number_number_of_nat(bit1(bit1(pls)))) = plus_plus_int(plus_plus_int(plus_plus_int(power_power_int(U_7,number_number_of_nat(bit1(bit1(pls)))),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),power_power_int(U_7,number_number_of_nat(bit0(bit1(pls))))),U_6)),times_times_int(times_times_int(number_number_of_int(bit1(bit1(pls))),U_7),power_power_int(U_6,number_number_of_nat(bit0(bit1(pls)))))),power_power_int(U_6,number_number_of_nat(bit1(bit1(pls))))),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [X_2,Y_2] : power_power_nat(plus_plus_nat(X_2,Y_2),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(plus_plus_nat(power_power_nat(X_2,number_number_of_nat(bit0(bit1(pls)))),power_power_nat(Y_2,number_number_of_nat(bit0(bit1(pls))))),times_times_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))),X_2),Y_2)),
inference(fof_nnf,[status(thm)],[fact_9_power2__sum]) ).
fof(f_10_2,plain,
! [U_9,U_8] : power_power_nat(plus_plus_nat(U_9,U_8),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(plus_plus_nat(power_power_nat(U_9,number_number_of_nat(bit0(bit1(pls)))),power_power_nat(U_8,number_number_of_nat(bit0(bit1(pls))))),times_times_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_9),U_8)),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
power_power_nat(plus_plus_nat(U_9,U_8),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(plus_plus_nat(power_power_nat(U_9,number_number_of_nat(bit0(bit1(pls)))),power_power_nat(U_8,number_number_of_nat(bit0(bit1(pls))))),times_times_nat(times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_9),U_8)),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X_2,Y_2] : power_power_int(plus_plus_int(X_2,Y_2),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(X_2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_2,number_number_of_nat(bit0(bit1(pls))))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),X_2),Y_2)),
inference(fof_nnf,[status(thm)],[fact_10_power2__sum]) ).
fof(f_11_2,plain,
! [U_11,U_10] : power_power_int(plus_plus_int(U_11,U_10),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(U_11,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_10,number_number_of_nat(bit0(bit1(pls))))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),U_11),U_10)),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
power_power_int(plus_plus_int(U_11,U_10),number_number_of_nat(bit0(bit1(pls)))) = plus_plus_int(plus_plus_int(power_power_int(U_11,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_10,number_number_of_nat(bit0(bit1(pls))))),times_times_int(times_times_int(number_number_of_int(bit0(bit1(pls))),U_11),U_10)),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [W_4] : power_power_int(number_number_of_int(W_4),number_number_of_nat(bit0(bit1(pls)))) = times_times_int(number_number_of_int(W_4),number_number_of_int(W_4)),
inference(fof_nnf,[status(thm)],[fact_11_power2__eq__square__number__of]) ).
fof(f_12_2,plain,
! [U_12] : power_power_int(number_number_of_int(U_12),number_number_of_nat(bit0(bit1(pls)))) = times_times_int(number_number_of_int(U_12),number_number_of_int(U_12)),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
power_power_int(number_number_of_int(U_12),number_number_of_nat(bit0(bit1(pls)))) = times_times_int(number_number_of_int(U_12),number_number_of_int(U_12)),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [W_4] : power_power_nat(number_number_of_nat(W_4),number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(number_number_of_nat(W_4),number_number_of_nat(W_4)),
inference(fof_nnf,[status(thm)],[fact_12_power2__eq__square__number__of]) ).
fof(f_13_2,plain,
! [U_13] : power_power_nat(number_number_of_nat(U_13),number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(number_number_of_nat(U_13),number_number_of_nat(U_13)),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
power_power_nat(number_number_of_nat(U_13),number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(number_number_of_nat(U_13),number_number_of_nat(U_13)),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
! [A_8] : times_times_int(A_8,power_power_int(A_8,number_number_of_nat(bit0(bit1(pls))))) = power_power_int(A_8,number_number_of_nat(bit1(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_13_cube__square]) ).
fof(f_14_2,plain,
! [U_14] : times_times_int(U_14,power_power_int(U_14,number_number_of_nat(bit0(bit1(pls))))) = power_power_int(U_14,number_number_of_nat(bit1(bit1(pls)))),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
times_times_int(U_14,power_power_int(U_14,number_number_of_nat(bit0(bit1(pls))))) = power_power_int(U_14,number_number_of_nat(bit1(bit1(pls)))),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
inference(fof_nnf,[status(thm)],[fact_14_one__power2]) ).
cnf(f_15_2,plain,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
inference(clausify,[status(thm)],[f_15_1]) ).
fof(f_16_1,plain,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
inference(fof_nnf,[status(thm)],[fact_15_one__power2]) ).
cnf(f_16_2,plain,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
inference(clausify,[status(thm)],[f_16_1]) ).
fof(f_17_1,plain,
! [X_7] : times_times_int(X_7,X_7) = power_power_int(X_7,number_number_of_nat(bit0(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_16_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J]) ).
fof(f_17_2,plain,
! [U_15] : times_times_int(U_15,U_15) = power_power_int(U_15,number_number_of_nat(bit0(bit1(pls)))),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
times_times_int(U_15,U_15) = power_power_int(U_15,number_number_of_nat(bit0(bit1(pls)))),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X_7] : times_times_nat(X_7,X_7) = power_power_nat(X_7,number_number_of_nat(bit0(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_17_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J]) ).
fof(f_18_2,plain,
! [U_16] : times_times_nat(U_16,U_16) = power_power_nat(U_16,number_number_of_nat(bit0(bit1(pls)))),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
times_times_nat(U_16,U_16) = power_power_nat(U_16,number_number_of_nat(bit0(bit1(pls)))),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [A_7] : power_power_int(A_7,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(A_7,A_7),
inference(fof_nnf,[status(thm)],[fact_18_power2__eq__square]) ).
fof(f_19_2,plain,
! [U_17] : power_power_int(U_17,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(U_17,U_17),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
power_power_int(U_17,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(U_17,U_17),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [A_7] : power_power_nat(A_7,number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(A_7,A_7),
inference(fof_nnf,[status(thm)],[fact_19_power2__eq__square]) ).
fof(f_20_2,plain,
! [U_18] : power_power_nat(U_18,number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(U_18,U_18),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
power_power_nat(U_18,number_number_of_nat(bit0(bit1(pls)))) = times_times_nat(U_18,U_18),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X_6,N] : power_power_int(X_6,times_times_nat(number_number_of_nat(bit0(bit1(pls))),N)) = times_times_int(power_power_int(X_6,N),power_power_int(X_6,N)),
inference(fof_nnf,[status(thm)],[fact_20_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J]) ).
fof(f_21_2,plain,
! [U_20,U_19] : power_power_int(U_20,times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_19)) = times_times_int(power_power_int(U_20,U_19),power_power_int(U_20,U_19)),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
power_power_int(U_20,times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_19)) = times_times_int(power_power_int(U_20,U_19),power_power_int(U_20,U_19)),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X_6,N] : power_power_nat(X_6,times_times_nat(number_number_of_nat(bit0(bit1(pls))),N)) = times_times_nat(power_power_nat(X_6,N),power_power_nat(X_6,N)),
inference(fof_nnf,[status(thm)],[fact_21_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J]) ).
fof(f_22_2,plain,
! [U_22,U_21] : power_power_nat(U_22,times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_21)) = times_times_nat(power_power_nat(U_22,U_21),power_power_nat(U_22,U_21)),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
power_power_nat(U_22,times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_21)) = times_times_nat(power_power_nat(U_22,U_21),power_power_nat(U_22,U_21)),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [W_3] : plus_plus_int(one_one_int,number_number_of_int(W_3)) = number_number_of_int(plus_plus_int(bit1(pls),W_3)),
inference(fof_nnf,[status(thm)],[fact_22_add__special_I2_J]) ).
fof(f_23_2,plain,
! [U_23] : plus_plus_int(one_one_int,number_number_of_int(U_23)) = number_number_of_int(plus_plus_int(bit1(pls),U_23)),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
plus_plus_int(one_one_int,number_number_of_int(U_23)) = number_number_of_int(plus_plus_int(bit1(pls),U_23)),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [V_3] : plus_plus_int(number_number_of_int(V_3),one_one_int) = number_number_of_int(plus_plus_int(V_3,bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_23_add__special_I3_J]) ).
fof(f_24_2,plain,
! [U_24] : plus_plus_int(number_number_of_int(U_24),one_one_int) = number_number_of_int(plus_plus_int(U_24,bit1(pls))),
inference(variable_rename,[status(thm)],[f_24_1]) ).
cnf(f_24_3,plain,
plus_plus_int(number_number_of_int(U_24),one_one_int) = number_number_of_int(plus_plus_int(U_24,bit1(pls))),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_24_one__add__one__is__two]) ).
cnf(f_25_2,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_25_1]) ).
fof(f_26_1,plain,
? [T] : 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_25__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_26_2,plain,
? [U_25] : 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_25),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_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_25,sK5)],[f_26_2]) ).
cnf(f_26_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_26_3]) ).
fof(f_27_1,plain,
! [W] : ord_less_eq_int(W,W),
inference(fof_nnf,[status(thm)],[fact_26_zle__refl]) ).
fof(f_27_2,plain,
! [U_26] : ord_less_eq_int(U_26,U_26),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
ord_less_eq_int(U_26,U_26),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
! [Z,W] :
( ord_less_eq_int(W,Z)
| ord_less_eq_int(Z,W) ),
inference(fof_nnf,[status(thm)],[fact_27_zle__linear]) ).
fof(f_28_2,plain,
! [U_28,U_27] :
( ord_less_eq_int(U_27,U_28)
| ord_less_eq_int(U_28,U_27) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
cnf(f_28_3,plain,
( ord_less_eq_int(U_27,U_28)
| ord_less_eq_int(U_28,U_27) ),
inference(clausify,[status(thm)],[f_28_2]) ).
fof(f_29_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_28_zless__le]) ).
fof(f_29_2,plain,
! [U_30,U_29] :
( ( ord_less_int(U_30,U_29)
| U_30 = U_29
| ~ ord_less_eq_int(U_30,U_29) )
& ( ( U_30 != U_29
& ord_less_eq_int(U_30,U_29) )
| ~ ord_less_int(U_30,U_29) ) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
( ! [U_34,U_32] :
( ord_less_int(U_34,U_32)
| U_34 = U_32
| ~ ord_less_eq_int(U_34,U_32) )
& ! [U_33,U_31] :
( ( U_33 != U_31
& ord_less_eq_int(U_33,U_31) )
| ~ ord_less_int(U_33,U_31) ) ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( ord_less_eq_int(U_33,U_31)
| ~ ord_less_int(U_33,U_31) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_5,plain,
( U_33 != U_31
| ~ ord_less_int(U_33,U_31) ),
inference(clausify,[status(thm)],[f_29_3]) ).
cnf(f_29_6,plain,
( ord_less_int(U_34,U_32)
| U_34 = U_32
| ~ ord_less_eq_int(U_34,U_32) ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_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_29_zless__linear]) ).
fof(f_30_2,plain,
! [U_36,U_35] :
( ord_less_int(U_35,U_36)
| U_36 = U_35
| ord_less_int(U_36,U_35) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
cnf(f_30_3,plain,
( ord_less_int(U_35,U_36)
| U_36 = U_35
| ord_less_int(U_36,U_35) ),
inference(clausify,[status(thm)],[f_30_2]) ).
fof(f_31_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_30_zle__trans]) ).
fof(f_31_2,plain,
! [U_39,U_38,U_37] :
( ord_less_eq_int(U_38,U_39)
| ~ ord_less_eq_int(U_37,U_39)
| ~ ord_less_eq_int(U_38,U_37) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
cnf(f_31_3,plain,
( ord_less_eq_int(U_38,U_39)
| ~ ord_less_eq_int(U_37,U_39)
| ~ ord_less_eq_int(U_38,U_37) ),
inference(clausify,[status(thm)],[f_31_2]) ).
fof(f_32_1,plain,
! [Z,W] :
( Z = W
| ~ ord_less_eq_int(W,Z)
| ~ ord_less_eq_int(Z,W) ),
inference(fof_nnf,[status(thm)],[fact_31_zle__antisym]) ).
fof(f_32_2,plain,
! [U_41,U_40] :
( U_41 = U_40
| ~ ord_less_eq_int(U_40,U_41)
| ~ ord_less_eq_int(U_41,U_40) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
cnf(f_32_3,plain,
( U_41 = U_40
| ~ ord_less_eq_int(U_40,U_41)
| ~ ord_less_eq_int(U_41,U_40) ),
inference(clausify,[status(thm)],[f_32_2]) ).
fof(f_33_1,plain,
! [X_5,P_1,Q_1] : power_power_int(power_power_int(X_5,P_1),Q_1) = power_power_int(X_5,times_times_nat(P_1,Q_1)),
inference(fof_nnf,[status(thm)],[fact_32_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J]) ).
fof(f_33_2,plain,
! [U_44,U_43,U_42] : power_power_int(power_power_int(U_44,U_43),U_42) = power_power_int(U_44,times_times_nat(U_43,U_42)),
inference(variable_rename,[status(thm)],[f_33_1]) ).
cnf(f_33_3,plain,
power_power_int(power_power_int(U_44,U_43),U_42) = power_power_int(U_44,times_times_nat(U_43,U_42)),
inference(clausify,[status(thm)],[f_33_2]) ).
fof(f_34_1,plain,
! [X_5,P_1,Q_1] : power_power_nat(power_power_nat(X_5,P_1),Q_1) = power_power_nat(X_5,times_times_nat(P_1,Q_1)),
inference(fof_nnf,[status(thm)],[fact_33_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J]) ).
fof(f_34_2,plain,
! [U_47,U_46,U_45] : power_power_nat(power_power_nat(U_47,U_46),U_45) = power_power_nat(U_47,times_times_nat(U_46,U_45)),
inference(variable_rename,[status(thm)],[f_34_1]) ).
cnf(f_34_3,plain,
power_power_nat(power_power_nat(U_47,U_46),U_45) = power_power_nat(U_47,times_times_nat(U_46,U_45)),
inference(clausify,[status(thm)],[f_34_2]) ).
fof(f_35_1,plain,
! [X_4] : power_power_int(X_4,one_one_nat) = X_4,
inference(fof_nnf,[status(thm)],[fact_34_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J]) ).
fof(f_35_2,plain,
! [U_48] : power_power_int(U_48,one_one_nat) = U_48,
inference(variable_rename,[status(thm)],[f_35_1]) ).
cnf(f_35_3,plain,
power_power_int(U_48,one_one_nat) = U_48,
inference(clausify,[status(thm)],[f_35_2]) ).
fof(f_36_1,plain,
! [X_4] : power_power_nat(X_4,one_one_nat) = X_4,
inference(fof_nnf,[status(thm)],[fact_35_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J]) ).
fof(f_36_2,plain,
! [U_49] : power_power_nat(U_49,one_one_nat) = U_49,
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
power_power_nat(U_49,one_one_nat) = U_49,
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_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_36_zpower__zpower]) ).
fof(f_37_2,plain,
! [U_52,U_51,U_50] : power_power_int(power_power_int(U_52,U_51),U_50) = power_power_int(U_52,times_times_nat(U_51,U_50)),
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
power_power_int(power_power_int(U_52,U_51),U_50) = power_power_int(U_52,times_times_nat(U_51,U_50)),
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_38_1,plain,
! [V_2,W_1] :
( ( ord_less_eq_nat(number_number_of_nat(V_2),number_number_of_nat(W_1))
| ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_2)) )
& ( ~ ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_2))
| ~ ord_less_eq_nat(number_number_of_nat(V_2),number_number_of_nat(W_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_37_le__number__of__eq__not__less]) ).
fof(f_38_2,plain,
! [U_54,U_53] :
( ( ord_less_eq_nat(number_number_of_nat(U_54),number_number_of_nat(U_53))
| ord_less_nat(number_number_of_nat(U_53),number_number_of_nat(U_54)) )
& ( ~ ord_less_nat(number_number_of_nat(U_53),number_number_of_nat(U_54))
| ~ ord_less_eq_nat(number_number_of_nat(U_54),number_number_of_nat(U_53)) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_58,U_56] :
( ord_less_eq_nat(number_number_of_nat(U_58),number_number_of_nat(U_56))
| ord_less_nat(number_number_of_nat(U_56),number_number_of_nat(U_58)) )
& ! [U_57,U_55] :
( ~ ord_less_nat(number_number_of_nat(U_55),number_number_of_nat(U_57))
| ~ ord_less_eq_nat(number_number_of_nat(U_57),number_number_of_nat(U_55)) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
cnf(f_38_4,plain,
( ~ ord_less_nat(number_number_of_nat(U_55),number_number_of_nat(U_57))
| ~ ord_less_eq_nat(number_number_of_nat(U_57),number_number_of_nat(U_55)) ),
inference(clausify,[status(thm)],[f_38_3]) ).
cnf(f_38_5,plain,
( ord_less_eq_nat(number_number_of_nat(U_58),number_number_of_nat(U_56))
| ord_less_nat(number_number_of_nat(U_56),number_number_of_nat(U_58)) ),
inference(clausify,[status(thm)],[f_38_3]) ).
fof(f_39_1,plain,
! [V_2,W_1] :
( ( ord_less_eq_int(number_number_of_int(V_2),number_number_of_int(W_1))
| ord_less_int(number_number_of_int(W_1),number_number_of_int(V_2)) )
& ( ~ ord_less_int(number_number_of_int(W_1),number_number_of_int(V_2))
| ~ ord_less_eq_int(number_number_of_int(V_2),number_number_of_int(W_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_38_le__number__of__eq__not__less]) ).
fof(f_39_2,plain,
! [U_60,U_59] :
( ( ord_less_eq_int(number_number_of_int(U_60),number_number_of_int(U_59))
| ord_less_int(number_number_of_int(U_59),number_number_of_int(U_60)) )
& ( ~ ord_less_int(number_number_of_int(U_59),number_number_of_int(U_60))
| ~ ord_less_eq_int(number_number_of_int(U_60),number_number_of_int(U_59)) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_64,U_62] :
( ord_less_eq_int(number_number_of_int(U_64),number_number_of_int(U_62))
| ord_less_int(number_number_of_int(U_62),number_number_of_int(U_64)) )
& ! [U_63,U_61] :
( ~ ord_less_int(number_number_of_int(U_61),number_number_of_int(U_63))
| ~ ord_less_eq_int(number_number_of_int(U_63),number_number_of_int(U_61)) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( ~ ord_less_int(number_number_of_int(U_61),number_number_of_int(U_63))
| ~ ord_less_eq_int(number_number_of_int(U_63),number_number_of_int(U_61)) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( ord_less_eq_int(number_number_of_int(U_64),number_number_of_int(U_62))
| ord_less_int(number_number_of_int(U_62),number_number_of_int(U_64)) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X_2,Y_2] :
( ( ord_less_int(number_number_of_int(X_2),number_number_of_int(Y_2))
| ~ ord_less_int(X_2,Y_2) )
& ( ord_less_int(X_2,Y_2)
| ~ ord_less_int(number_number_of_int(X_2),number_number_of_int(Y_2)) ) ),
inference(fof_nnf,[status(thm)],[fact_39_less__number__of]) ).
fof(f_40_2,plain,
! [U_66,U_65] :
( ( ord_less_int(number_number_of_int(U_66),number_number_of_int(U_65))
| ~ ord_less_int(U_66,U_65) )
& ( ord_less_int(U_66,U_65)
| ~ ord_less_int(number_number_of_int(U_66),number_number_of_int(U_65)) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_70,U_68] :
( ord_less_int(number_number_of_int(U_70),number_number_of_int(U_68))
| ~ ord_less_int(U_70,U_68) )
& ! [U_69,U_67] :
( ord_less_int(U_69,U_67)
| ~ ord_less_int(number_number_of_int(U_69),number_number_of_int(U_67)) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( ord_less_int(U_69,U_67)
| ~ ord_less_int(number_number_of_int(U_69),number_number_of_int(U_67)) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_5,plain,
( ord_less_int(number_number_of_int(U_70),number_number_of_int(U_68))
| ~ ord_less_int(U_70,U_68) ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [X_2,Y_2] :
( ( ord_less_eq_int(number_number_of_int(X_2),number_number_of_int(Y_2))
| ~ ord_less_eq_int(X_2,Y_2) )
& ( ord_less_eq_int(X_2,Y_2)
| ~ ord_less_eq_int(number_number_of_int(X_2),number_number_of_int(Y_2)) ) ),
inference(fof_nnf,[status(thm)],[fact_40_le__number__of]) ).
fof(f_41_2,plain,
! [U_72,U_71] :
( ( ord_less_eq_int(number_number_of_int(U_72),number_number_of_int(U_71))
| ~ ord_less_eq_int(U_72,U_71) )
& ( ord_less_eq_int(U_72,U_71)
| ~ ord_less_eq_int(number_number_of_int(U_72),number_number_of_int(U_71)) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_76,U_74] :
( ord_less_eq_int(number_number_of_int(U_76),number_number_of_int(U_74))
| ~ ord_less_eq_int(U_76,U_74) )
& ! [U_75,U_73] :
( ord_less_eq_int(U_75,U_73)
| ~ ord_less_eq_int(number_number_of_int(U_75),number_number_of_int(U_73)) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( ord_less_eq_int(U_75,U_73)
| ~ ord_less_eq_int(number_number_of_int(U_75),number_number_of_int(U_73)) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_5,plain,
( ord_less_eq_int(number_number_of_int(U_76),number_number_of_int(U_74))
| ~ ord_less_eq_int(U_76,U_74) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_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_41_zadd__zless__mono]) ).
fof(f_42_2,plain,
! [U_80,U_79,U_78,U_77] :
( ord_less_int(plus_plus_int(U_78,U_80),plus_plus_int(U_77,U_79))
| ~ ord_less_eq_int(U_80,U_79)
| ~ ord_less_int(U_78,U_77) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
( ord_less_int(plus_plus_int(U_78,U_80),plus_plus_int(U_77,U_79))
| ~ ord_less_eq_int(U_80,U_79)
| ~ ord_less_int(U_78,U_77) ),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
! [X_3,P,Q] : times_times_int(power_power_int(X_3,P),power_power_int(X_3,Q)) = power_power_int(X_3,plus_plus_nat(P,Q)),
inference(fof_nnf,[status(thm)],[fact_42_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J]) ).
fof(f_43_2,plain,
! [U_83,U_82,U_81] : times_times_int(power_power_int(U_83,U_82),power_power_int(U_83,U_81)) = power_power_int(U_83,plus_plus_nat(U_82,U_81)),
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
times_times_int(power_power_int(U_83,U_82),power_power_int(U_83,U_81)) = power_power_int(U_83,plus_plus_nat(U_82,U_81)),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_44_1,plain,
! [X_3,P,Q] : times_times_nat(power_power_nat(X_3,P),power_power_nat(X_3,Q)) = power_power_nat(X_3,plus_plus_nat(P,Q)),
inference(fof_nnf,[status(thm)],[fact_43_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J]) ).
fof(f_44_2,plain,
! [U_86,U_85,U_84] : times_times_nat(power_power_nat(U_86,U_85),power_power_nat(U_86,U_84)) = power_power_nat(U_86,plus_plus_nat(U_85,U_84)),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
times_times_nat(power_power_nat(U_86,U_85),power_power_nat(U_86,U_84)) = power_power_nat(U_86,plus_plus_nat(U_85,U_84)),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_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_44_zpower__zadd__distrib]) ).
fof(f_45_2,plain,
! [U_89,U_88,U_87] : power_power_int(U_89,plus_plus_nat(U_88,U_87)) = times_times_int(power_power_int(U_89,U_88),power_power_int(U_89,U_87)),
inference(variable_rename,[status(thm)],[f_45_1]) ).
cnf(f_45_3,plain,
power_power_int(U_89,plus_plus_nat(U_88,U_87)) = times_times_int(power_power_int(U_89,U_88),power_power_int(U_89,U_87)),
inference(clausify,[status(thm)],[f_45_2]) ).
fof(f_46_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_45_nat__mult__2]) ).
fof(f_46_2,plain,
! [U_90] : times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_90) = plus_plus_nat(U_90,U_90),
inference(variable_rename,[status(thm)],[f_46_1]) ).
cnf(f_46_3,plain,
times_times_nat(number_number_of_nat(bit0(bit1(pls))),U_90) = plus_plus_nat(U_90,U_90),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_47_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_46_nat__mult__2__right]) ).
fof(f_47_2,plain,
! [U_91] : times_times_nat(U_91,number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(U_91,U_91),
inference(variable_rename,[status(thm)],[f_47_1]) ).
cnf(f_47_3,plain,
times_times_nat(U_91,number_number_of_nat(bit0(bit1(pls)))) = plus_plus_nat(U_91,U_91),
inference(clausify,[status(thm)],[f_47_2]) ).
fof(f_48_1,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_47_nat__1__add__1]) ).
cnf(f_48_2,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_48_1]) ).
fof(f_49_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_48_less__int__code_I16_J]) ).
fof(f_49_2,plain,
! [U_93,U_92] :
( ( ord_less_int(bit1(U_93),bit1(U_92))
| ~ ord_less_int(U_93,U_92) )
& ( ord_less_int(U_93,U_92)
| ~ ord_less_int(bit1(U_93),bit1(U_92)) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_97,U_95] :
( ord_less_int(bit1(U_97),bit1(U_95))
| ~ ord_less_int(U_97,U_95) )
& ! [U_96,U_94] :
( ord_less_int(U_96,U_94)
| ~ ord_less_int(bit1(U_96),bit1(U_94)) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
cnf(f_49_4,plain,
( ord_less_int(U_96,U_94)
| ~ ord_less_int(bit1(U_96),bit1(U_94)) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_5,plain,
( ord_less_int(bit1(U_97),bit1(U_95))
| ~ ord_less_int(U_97,U_95) ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_50_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_49_rel__simps_I17_J]) ).
fof(f_50_2,plain,
! [U_99,U_98] :
( ( ord_less_int(bit1(U_99),bit1(U_98))
| ~ ord_less_int(U_99,U_98) )
& ( ord_less_int(U_99,U_98)
| ~ ord_less_int(bit1(U_99),bit1(U_98)) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_103,U_101] :
( ord_less_int(bit1(U_103),bit1(U_101))
| ~ ord_less_int(U_103,U_101) )
& ! [U_102,U_100] :
( ord_less_int(U_102,U_100)
| ~ ord_less_int(bit1(U_102),bit1(U_100)) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( ord_less_int(U_102,U_100)
| ~ ord_less_int(bit1(U_102),bit1(U_100)) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_5,plain,
( ord_less_int(bit1(U_103),bit1(U_101))
| ~ ord_less_int(U_103,U_101) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_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_50_less__eq__int__code_I16_J]) ).
fof(f_51_2,plain,
! [U_105,U_104] :
( ( ord_less_eq_int(bit1(U_105),bit1(U_104))
| ~ ord_less_eq_int(U_105,U_104) )
& ( ord_less_eq_int(U_105,U_104)
| ~ ord_less_eq_int(bit1(U_105),bit1(U_104)) ) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
fof(f_51_3,plain,
( ! [U_109,U_107] :
( ord_less_eq_int(bit1(U_109),bit1(U_107))
| ~ ord_less_eq_int(U_109,U_107) )
& ! [U_108,U_106] :
( ord_less_eq_int(U_108,U_106)
| ~ ord_less_eq_int(bit1(U_108),bit1(U_106)) ) ),
inference(miniscope,[status(thm)],[f_51_2]) ).
cnf(f_51_4,plain,
( ord_less_eq_int(U_108,U_106)
| ~ ord_less_eq_int(bit1(U_108),bit1(U_106)) ),
inference(clausify,[status(thm)],[f_51_3]) ).
cnf(f_51_5,plain,
( ord_less_eq_int(bit1(U_109),bit1(U_107))
| ~ ord_less_eq_int(U_109,U_107) ),
inference(clausify,[status(thm)],[f_51_3]) ).
fof(f_52_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_51_rel__simps_I34_J]) ).
fof(f_52_2,plain,
! [U_111,U_110] :
( ( ord_less_eq_int(bit1(U_111),bit1(U_110))
| ~ ord_less_eq_int(U_111,U_110) )
& ( ord_less_eq_int(U_111,U_110)
| ~ ord_less_eq_int(bit1(U_111),bit1(U_110)) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_115,U_113] :
( ord_less_eq_int(bit1(U_115),bit1(U_113))
| ~ ord_less_eq_int(U_115,U_113) )
& ! [U_114,U_112] :
( ord_less_eq_int(U_114,U_112)
| ~ ord_less_eq_int(bit1(U_114),bit1(U_112)) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
cnf(f_52_4,plain,
( ord_less_eq_int(U_114,U_112)
| ~ ord_less_eq_int(bit1(U_114),bit1(U_112)) ),
inference(clausify,[status(thm)],[f_52_3]) ).
cnf(f_52_5,plain,
( ord_less_eq_int(bit1(U_115),bit1(U_113))
| ~ ord_less_eq_int(U_115,U_113) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,plain,
~ ord_less_int(pls,pls),
inference(fof_nnf,[status(thm)],[fact_52_rel__simps_I2_J]) ).
cnf(f_53_2,plain,
~ ord_less_int(pls,pls),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_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_53_less__int__code_I13_J]) ).
fof(f_54_2,plain,
! [U_117,U_116] :
( ( ord_less_int(bit0(U_117),bit0(U_116))
| ~ ord_less_int(U_117,U_116) )
& ( ord_less_int(U_117,U_116)
| ~ ord_less_int(bit0(U_117),bit0(U_116)) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_121,U_119] :
( ord_less_int(bit0(U_121),bit0(U_119))
| ~ ord_less_int(U_121,U_119) )
& ! [U_120,U_118] :
( ord_less_int(U_120,U_118)
| ~ ord_less_int(bit0(U_120),bit0(U_118)) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( ord_less_int(U_120,U_118)
| ~ ord_less_int(bit0(U_120),bit0(U_118)) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( ord_less_int(bit0(U_121),bit0(U_119))
| ~ ord_less_int(U_121,U_119) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_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_54_rel__simps_I14_J]) ).
fof(f_55_2,plain,
! [U_123,U_122] :
( ( ord_less_int(bit0(U_123),bit0(U_122))
| ~ ord_less_int(U_123,U_122) )
& ( ord_less_int(U_123,U_122)
| ~ ord_less_int(bit0(U_123),bit0(U_122)) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_127,U_125] :
( ord_less_int(bit0(U_127),bit0(U_125))
| ~ ord_less_int(U_127,U_125) )
& ! [U_126,U_124] :
( ord_less_int(U_126,U_124)
| ~ ord_less_int(bit0(U_126),bit0(U_124)) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
cnf(f_55_4,plain,
( ord_less_int(U_126,U_124)
| ~ ord_less_int(bit0(U_126),bit0(U_124)) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_5,plain,
( ord_less_int(bit0(U_127),bit0(U_125))
| ~ ord_less_int(U_127,U_125) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_1,plain,
ord_less_eq_int(pls,pls),
inference(fof_nnf,[status(thm)],[fact_55_rel__simps_I19_J]) ).
cnf(f_56_2,plain,
ord_less_eq_int(pls,pls),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_57_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_56_less__eq__int__code_I13_J]) ).
fof(f_57_2,plain,
! [U_129,U_128] :
( ( ord_less_eq_int(bit0(U_129),bit0(U_128))
| ~ ord_less_eq_int(U_129,U_128) )
& ( ord_less_eq_int(U_129,U_128)
| ~ ord_less_eq_int(bit0(U_129),bit0(U_128)) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_133,U_131] :
( ord_less_eq_int(bit0(U_133),bit0(U_131))
| ~ ord_less_eq_int(U_133,U_131) )
& ! [U_132,U_130] :
( ord_less_eq_int(U_132,U_130)
| ~ ord_less_eq_int(bit0(U_132),bit0(U_130)) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( ord_less_eq_int(U_132,U_130)
| ~ ord_less_eq_int(bit0(U_132),bit0(U_130)) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( ord_less_eq_int(bit0(U_133),bit0(U_131))
| ~ ord_less_eq_int(U_133,U_131) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_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_57_rel__simps_I31_J]) ).
fof(f_58_2,plain,
! [U_135,U_134] :
( ( ord_less_eq_int(bit0(U_135),bit0(U_134))
| ~ ord_less_eq_int(U_135,U_134) )
& ( ord_less_eq_int(U_135,U_134)
| ~ ord_less_eq_int(bit0(U_135),bit0(U_134)) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_139,U_137] :
( ord_less_eq_int(bit0(U_139),bit0(U_137))
| ~ ord_less_eq_int(U_139,U_137) )
& ! [U_138,U_136] :
( ord_less_eq_int(U_138,U_136)
| ~ ord_less_eq_int(bit0(U_138),bit0(U_136)) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( ord_less_eq_int(U_138,U_136)
| ~ ord_less_eq_int(bit0(U_138),bit0(U_136)) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( ord_less_eq_int(bit0(U_139),bit0(U_137))
| ~ ord_less_eq_int(U_139,U_137) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_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_58_less__number__of__int__code]) ).
fof(f_59_2,plain,
! [U_141,U_140] :
( ( ord_less_int(number_number_of_int(U_141),number_number_of_int(U_140))
| ~ ord_less_int(U_141,U_140) )
& ( ord_less_int(U_141,U_140)
| ~ ord_less_int(number_number_of_int(U_141),number_number_of_int(U_140)) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_145,U_143] :
( ord_less_int(number_number_of_int(U_145),number_number_of_int(U_143))
| ~ ord_less_int(U_145,U_143) )
& ! [U_144,U_142] :
( ord_less_int(U_144,U_142)
| ~ ord_less_int(number_number_of_int(U_144),number_number_of_int(U_142)) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
cnf(f_59_4,plain,
( ord_less_int(U_144,U_142)
| ~ ord_less_int(number_number_of_int(U_144),number_number_of_int(U_142)) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_5,plain,
( ord_less_int(number_number_of_int(U_145),number_number_of_int(U_143))
| ~ ord_less_int(U_145,U_143) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_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_59_less__eq__number__of__int__code]) ).
fof(f_60_2,plain,
! [U_147,U_146] :
( ( ord_less_eq_int(number_number_of_int(U_147),number_number_of_int(U_146))
| ~ ord_less_eq_int(U_147,U_146) )
& ( ord_less_eq_int(U_147,U_146)
| ~ ord_less_eq_int(number_number_of_int(U_147),number_number_of_int(U_146)) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_151,U_149] :
( ord_less_eq_int(number_number_of_int(U_151),number_number_of_int(U_149))
| ~ ord_less_eq_int(U_151,U_149) )
& ! [U_150,U_148] :
( ord_less_eq_int(U_150,U_148)
| ~ ord_less_eq_int(number_number_of_int(U_150),number_number_of_int(U_148)) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
cnf(f_60_4,plain,
( ord_less_eq_int(U_150,U_148)
| ~ ord_less_eq_int(number_number_of_int(U_150),number_number_of_int(U_148)) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_5,plain,
( ord_less_eq_int(number_number_of_int(U_151),number_number_of_int(U_149))
| ~ ord_less_eq_int(U_151,U_149) ),
inference(clausify,[status(thm)],[f_60_3]) ).
fof(f_61_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_60_zadd__strict__right__mono]) ).
fof(f_61_2,plain,
! [U_154,U_153,U_152] :
( ord_less_int(plus_plus_int(U_153,U_154),plus_plus_int(U_152,U_154))
| ~ ord_less_int(U_153,U_152) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
cnf(f_61_3,plain,
( ord_less_int(plus_plus_int(U_153,U_154),plus_plus_int(U_152,U_154))
| ~ ord_less_int(U_153,U_152) ),
inference(clausify,[status(thm)],[f_61_2]) ).
fof(f_62_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_61_zadd__left__mono]) ).
fof(f_62_2,plain,
! [U_157,U_156,U_155] :
( ord_less_eq_int(plus_plus_int(U_157,U_156),plus_plus_int(U_157,U_155))
| ~ ord_less_eq_int(U_156,U_155) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
cnf(f_62_3,plain,
( ord_less_eq_int(plus_plus_int(U_157,U_156),plus_plus_int(U_157,U_155))
| ~ ord_less_eq_int(U_156,U_155) ),
inference(clausify,[status(thm)],[f_62_2]) ).
fof(f_63_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_62_add__nat__number__of]) ).
fof(f_63_2,plain,
! [U_159,U_158] :
( ( ( ( plus_plus_nat(number_number_of_nat(U_158),number_number_of_nat(U_159)) = number_number_of_nat(plus_plus_int(U_158,U_159))
| ord_less_int(U_159,pls) )
& ( plus_plus_nat(number_number_of_nat(U_158),number_number_of_nat(U_159)) = number_number_of_nat(U_158)
| ~ ord_less_int(U_159,pls) ) )
| ord_less_int(U_158,pls) )
& ( plus_plus_nat(number_number_of_nat(U_158),number_number_of_nat(U_159)) = number_number_of_nat(U_159)
| ~ ord_less_int(U_158,pls) ) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
fof(f_63_3,plain,
( ! [U_163,U_161] :
( ( ( plus_plus_nat(number_number_of_nat(U_161),number_number_of_nat(U_163)) = number_number_of_nat(plus_plus_int(U_161,U_163))
| ord_less_int(U_163,pls) )
& ( plus_plus_nat(number_number_of_nat(U_161),number_number_of_nat(U_163)) = number_number_of_nat(U_161)
| ~ ord_less_int(U_163,pls) ) )
| ord_less_int(U_161,pls) )
& ! [U_162,U_160] :
( plus_plus_nat(number_number_of_nat(U_160),number_number_of_nat(U_162)) = number_number_of_nat(U_162)
| ~ ord_less_int(U_160,pls) ) ),
inference(miniscope,[status(thm)],[f_63_2]) ).
cnf(f_63_4,plain,
( plus_plus_nat(number_number_of_nat(U_160),number_number_of_nat(U_162)) = number_number_of_nat(U_162)
| ~ ord_less_int(U_160,pls) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_5,plain,
( plus_plus_nat(number_number_of_nat(U_161),number_number_of_nat(U_163)) = number_number_of_nat(U_161)
| ~ ord_less_int(U_163,pls)
| ord_less_int(U_161,pls) ),
inference(clausify,[status(thm)],[f_63_3]) ).
cnf(f_63_6,plain,
( plus_plus_nat(number_number_of_nat(U_161),number_number_of_nat(U_163)) = number_number_of_nat(plus_plus_int(U_161,U_163))
| ord_less_int(U_163,pls)
| ord_less_int(U_161,pls) ),
inference(clausify,[status(thm)],[f_63_3]) ).
fof(f_64_1,plain,
number_number_of_nat(bit1(pls)) = one_one_nat,
inference(fof_nnf,[status(thm)],[fact_63_nat__numeral__1__eq__1]) ).
cnf(f_64_2,plain,
number_number_of_nat(bit1(pls)) = one_one_nat,
inference(clausify,[status(thm)],[f_64_1]) ).
fof(f_65_1,plain,
one_one_nat = number_number_of_nat(bit1(pls)),
inference(fof_nnf,[status(thm)],[fact_64_Numeral1__eq1__nat]) ).
cnf(f_65_2,plain,
one_one_nat = number_number_of_nat(bit1(pls)),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_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_65_rel__simps_I29_J]) ).
fof(f_66_2,plain,
! [U_164] :
( ( ord_less_eq_int(bit1(U_164),pls)
| ~ ord_less_int(U_164,pls) )
& ( ord_less_int(U_164,pls)
| ~ ord_less_eq_int(bit1(U_164),pls) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_166] :
( ord_less_eq_int(bit1(U_166),pls)
| ~ ord_less_int(U_166,pls) )
& ! [U_165] :
( ord_less_int(U_165,pls)
| ~ ord_less_eq_int(bit1(U_165),pls) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( ord_less_int(U_165,pls)
| ~ ord_less_eq_int(bit1(U_165),pls) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( ord_less_eq_int(bit1(U_166),pls)
| ~ ord_less_int(U_166,pls) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_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_66_rel__simps_I5_J]) ).
fof(f_67_2,plain,
! [U_167] :
( ( ord_less_int(pls,bit1(U_167))
| ~ ord_less_eq_int(pls,U_167) )
& ( ord_less_eq_int(pls,U_167)
| ~ ord_less_int(pls,bit1(U_167)) ) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
fof(f_67_3,plain,
( ! [U_169] :
( ord_less_int(pls,bit1(U_169))
| ~ ord_less_eq_int(pls,U_169) )
& ! [U_168] :
( ord_less_eq_int(pls,U_168)
| ~ ord_less_int(pls,bit1(U_168)) ) ),
inference(miniscope,[status(thm)],[f_67_2]) ).
cnf(f_67_4,plain,
( ord_less_eq_int(pls,U_168)
| ~ ord_less_int(pls,bit1(U_168)) ),
inference(clausify,[status(thm)],[f_67_3]) ).
cnf(f_67_5,plain,
( ord_less_int(pls,bit1(U_169))
| ~ ord_less_eq_int(pls,U_169) ),
inference(clausify,[status(thm)],[f_67_3]) ).
fof(f_68_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_67_less__eq__int__code_I15_J]) ).
fof(f_68_2,plain,
! [U_171,U_170] :
( ( ord_less_eq_int(bit1(U_171),bit0(U_170))
| ~ ord_less_int(U_171,U_170) )
& ( ord_less_int(U_171,U_170)
| ~ ord_less_eq_int(bit1(U_171),bit0(U_170)) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_175,U_173] :
( ord_less_eq_int(bit1(U_175),bit0(U_173))
| ~ ord_less_int(U_175,U_173) )
& ! [U_174,U_172] :
( ord_less_int(U_174,U_172)
| ~ ord_less_eq_int(bit1(U_174),bit0(U_172)) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ord_less_int(U_174,U_172)
| ~ ord_less_eq_int(bit1(U_174),bit0(U_172)) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( ord_less_eq_int(bit1(U_175),bit0(U_173))
| ~ ord_less_int(U_175,U_173) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_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_68_rel__simps_I33_J]) ).
fof(f_69_2,plain,
! [U_177,U_176] :
( ( ord_less_eq_int(bit1(U_177),bit0(U_176))
| ~ ord_less_int(U_177,U_176) )
& ( ord_less_int(U_177,U_176)
| ~ ord_less_eq_int(bit1(U_177),bit0(U_176)) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_181,U_179] :
( ord_less_eq_int(bit1(U_181),bit0(U_179))
| ~ ord_less_int(U_181,U_179) )
& ! [U_180,U_178] :
( ord_less_int(U_180,U_178)
| ~ ord_less_eq_int(bit1(U_180),bit0(U_178)) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
cnf(f_69_4,plain,
( ord_less_int(U_180,U_178)
| ~ ord_less_eq_int(bit1(U_180),bit0(U_178)) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(f_69_5,plain,
( ord_less_eq_int(bit1(U_181),bit0(U_179))
| ~ ord_less_int(U_181,U_179) ),
inference(clausify,[status(thm)],[f_69_3]) ).
fof(f_70_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_69_less__int__code_I14_J]) ).
fof(f_70_2,plain,
! [U_183,U_182] :
( ( ord_less_int(bit0(U_183),bit1(U_182))
| ~ ord_less_eq_int(U_183,U_182) )
& ( ord_less_eq_int(U_183,U_182)
| ~ ord_less_int(bit0(U_183),bit1(U_182)) ) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_187,U_185] :
( ord_less_int(bit0(U_187),bit1(U_185))
| ~ ord_less_eq_int(U_187,U_185) )
& ! [U_186,U_184] :
( ord_less_eq_int(U_186,U_184)
| ~ ord_less_int(bit0(U_186),bit1(U_184)) ) ),
inference(miniscope,[status(thm)],[f_70_2]) ).
cnf(f_70_4,plain,
( ord_less_eq_int(U_186,U_184)
| ~ ord_less_int(bit0(U_186),bit1(U_184)) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_5,plain,
( ord_less_int(bit0(U_187),bit1(U_185))
| ~ ord_less_eq_int(U_187,U_185) ),
inference(clausify,[status(thm)],[f_70_3]) ).
fof(f_71_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_70_rel__simps_I15_J]) ).
fof(f_71_2,plain,
! [U_189,U_188] :
( ( ord_less_int(bit0(U_189),bit1(U_188))
| ~ ord_less_eq_int(U_189,U_188) )
& ( ord_less_eq_int(U_189,U_188)
| ~ ord_less_int(bit0(U_189),bit1(U_188)) ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_193,U_191] :
( ord_less_int(bit0(U_193),bit1(U_191))
| ~ ord_less_eq_int(U_193,U_191) )
& ! [U_192,U_190] :
( ord_less_eq_int(U_192,U_190)
| ~ ord_less_int(bit0(U_192),bit1(U_190)) ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( ord_less_eq_int(U_192,U_190)
| ~ ord_less_int(bit0(U_192),bit1(U_190)) ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( ord_less_int(bit0(U_193),bit1(U_191))
| ~ ord_less_eq_int(U_193,U_191) ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_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_71_zless__imp__add1__zle]) ).
fof(f_72_2,plain,
! [U_195,U_194] :
( ord_less_eq_int(plus_plus_int(U_195,one_one_int),U_194)
| ~ ord_less_int(U_195,U_194) ),
inference(variable_rename,[status(thm)],[f_72_1]) ).
cnf(f_72_3,plain,
( ord_less_eq_int(plus_plus_int(U_195,one_one_int),U_194)
| ~ ord_less_int(U_195,U_194) ),
inference(clausify,[status(thm)],[f_72_2]) ).
fof(f_73_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_72_add1__zle__eq]) ).
fof(f_73_2,plain,
! [U_197,U_196] :
( ( ord_less_eq_int(plus_plus_int(U_197,one_one_int),U_196)
| ~ ord_less_int(U_197,U_196) )
& ( ord_less_int(U_197,U_196)
| ~ ord_less_eq_int(plus_plus_int(U_197,one_one_int),U_196) ) ),
inference(variable_rename,[status(thm)],[f_73_1]) ).
fof(f_73_3,plain,
( ! [U_201,U_199] :
( ord_less_eq_int(plus_plus_int(U_201,one_one_int),U_199)
| ~ ord_less_int(U_201,U_199) )
& ! [U_200,U_198] :
( ord_less_int(U_200,U_198)
| ~ ord_less_eq_int(plus_plus_int(U_200,one_one_int),U_198) ) ),
inference(miniscope,[status(thm)],[f_73_2]) ).
cnf(f_73_4,plain,
( ord_less_int(U_200,U_198)
| ~ ord_less_eq_int(plus_plus_int(U_200,one_one_int),U_198) ),
inference(clausify,[status(thm)],[f_73_3]) ).
cnf(f_73_5,plain,
( ord_less_eq_int(plus_plus_int(U_201,one_one_int),U_199)
| ~ ord_less_int(U_201,U_199) ),
inference(clausify,[status(thm)],[f_73_3]) ).
fof(f_74_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_73_zle__add1__eq__le]) ).
fof(f_74_2,plain,
! [U_203,U_202] :
( ( ord_less_int(U_203,plus_plus_int(U_202,one_one_int))
| ~ ord_less_eq_int(U_203,U_202) )
& ( ord_less_eq_int(U_203,U_202)
| ~ ord_less_int(U_203,plus_plus_int(U_202,one_one_int)) ) ),
inference(variable_rename,[status(thm)],[f_74_1]) ).
fof(f_74_3,plain,
( ! [U_207,U_205] :
( ord_less_int(U_207,plus_plus_int(U_205,one_one_int))
| ~ ord_less_eq_int(U_207,U_205) )
& ! [U_206,U_204] :
( ord_less_eq_int(U_206,U_204)
| ~ ord_less_int(U_206,plus_plus_int(U_204,one_one_int)) ) ),
inference(miniscope,[status(thm)],[f_74_2]) ).
cnf(f_74_4,plain,
( ord_less_eq_int(U_206,U_204)
| ~ ord_less_int(U_206,plus_plus_int(U_204,one_one_int)) ),
inference(clausify,[status(thm)],[f_74_3]) ).
cnf(f_74_5,plain,
( ord_less_int(U_207,plus_plus_int(U_205,one_one_int))
| ~ ord_less_eq_int(U_207,U_205) ),
inference(clausify,[status(thm)],[f_74_3]) ).
fof(f_75_1,plain,
zprime(number_number_of_int(bit0(bit1(pls)))),
inference(fof_nnf,[status(thm)],[fact_74_zprime__2]) ).
cnf(f_75_2,plain,
zprime(number_number_of_int(bit0(bit1(pls)))),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
! [Y_1,X_1] :
( twoSqu526106917sum2sq(times_times_int(X_1,Y_1))
| ~ twoSqu526106917sum2sq(Y_1)
| ~ twoSqu526106917sum2sq(X_1) ),
inference(fof_nnf,[status(thm)],[fact_75_is__mult__sum2sq]) ).
fof(f_76_2,plain,
! [U_209,U_208] :
( twoSqu526106917sum2sq(times_times_int(U_208,U_209))
| ~ twoSqu526106917sum2sq(U_209)
| ~ twoSqu526106917sum2sq(U_208) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
cnf(f_76_3,plain,
( twoSqu526106917sum2sq(times_times_int(U_208,U_209))
| ~ twoSqu526106917sum2sq(U_209)
| ~ twoSqu526106917sum2sq(U_208) ),
inference(clausify,[status(thm)],[f_76_2]) ).
fof(f_77_1,plain,
! [Lx_6,Ly_4,Rx_6,Ry_4] : times_times_int(times_times_int(Lx_6,Ly_4),times_times_int(Rx_6,Ry_4)) = times_times_int(times_times_int(Lx_6,Rx_6),times_times_int(Ly_4,Ry_4)),
inference(fof_nnf,[status(thm)],[fact_76_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J]) ).
fof(f_77_2,plain,
! [U_213,U_212,U_211,U_210] : times_times_int(times_times_int(U_213,U_212),times_times_int(U_211,U_210)) = times_times_int(times_times_int(U_213,U_211),times_times_int(U_212,U_210)),
inference(variable_rename,[status(thm)],[f_77_1]) ).
cnf(f_77_3,plain,
times_times_int(times_times_int(U_213,U_212),times_times_int(U_211,U_210)) = times_times_int(times_times_int(U_213,U_211),times_times_int(U_212,U_210)),
inference(clausify,[status(thm)],[f_77_2]) ).
fof(f_78_1,plain,
! [Lx_6,Ly_4,Rx_6,Ry_4] : times_times_nat(times_times_nat(Lx_6,Ly_4),times_times_nat(Rx_6,Ry_4)) = times_times_nat(times_times_nat(Lx_6,Rx_6),times_times_nat(Ly_4,Ry_4)),
inference(fof_nnf,[status(thm)],[fact_77_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J]) ).
fof(f_78_2,plain,
! [U_217,U_216,U_215,U_214] : times_times_nat(times_times_nat(U_217,U_216),times_times_nat(U_215,U_214)) = times_times_nat(times_times_nat(U_217,U_215),times_times_nat(U_216,U_214)),
inference(variable_rename,[status(thm)],[f_78_1]) ).
cnf(f_78_3,plain,
times_times_nat(times_times_nat(U_217,U_216),times_times_nat(U_215,U_214)) = times_times_nat(times_times_nat(U_217,U_215),times_times_nat(U_216,U_214)),
inference(clausify,[status(thm)],[f_78_2]) ).
fof(f_79_1,plain,
! [Lx_5,Ly_3,Rx_5,Ry_3] : times_times_int(times_times_int(Lx_5,Ly_3),times_times_int(Rx_5,Ry_3)) = times_times_int(Rx_5,times_times_int(times_times_int(Lx_5,Ly_3),Ry_3)),
inference(fof_nnf,[status(thm)],[fact_78_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J]) ).
fof(f_79_2,plain,
! [U_221,U_220,U_219,U_218] : times_times_int(times_times_int(U_221,U_220),times_times_int(U_219,U_218)) = times_times_int(U_219,times_times_int(times_times_int(U_221,U_220),U_218)),
inference(variable_rename,[status(thm)],[f_79_1]) ).
cnf(f_79_3,plain,
times_times_int(times_times_int(U_221,U_220),times_times_int(U_219,U_218)) = times_times_int(U_219,times_times_int(times_times_int(U_221,U_220),U_218)),
inference(clausify,[status(thm)],[f_79_2]) ).
fof(f_80_1,plain,
! [Lx_5,Ly_3,Rx_5,Ry_3] : times_times_nat(times_times_nat(Lx_5,Ly_3),times_times_nat(Rx_5,Ry_3)) = times_times_nat(Rx_5,times_times_nat(times_times_nat(Lx_5,Ly_3),Ry_3)),
inference(fof_nnf,[status(thm)],[fact_79_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J]) ).
fof(f_80_2,plain,
! [U_225,U_224,U_223,U_222] : times_times_nat(times_times_nat(U_225,U_224),times_times_nat(U_223,U_222)) = times_times_nat(U_223,times_times_nat(times_times_nat(U_225,U_224),U_222)),
inference(variable_rename,[status(thm)],[f_80_1]) ).
cnf(f_80_3,plain,
times_times_nat(times_times_nat(U_225,U_224),times_times_nat(U_223,U_222)) = times_times_nat(U_223,times_times_nat(times_times_nat(U_225,U_224),U_222)),
inference(clausify,[status(thm)],[f_80_2]) ).
fof(f_81_1,plain,
! [Lx_4,Ly_2,Rx_4,Ry_2] : times_times_int(times_times_int(Lx_4,Ly_2),times_times_int(Rx_4,Ry_2)) = times_times_int(Lx_4,times_times_int(Ly_2,times_times_int(Rx_4,Ry_2))),
inference(fof_nnf,[status(thm)],[fact_80_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J]) ).
fof(f_81_2,plain,
! [U_229,U_228,U_227,U_226] : times_times_int(times_times_int(U_229,U_228),times_times_int(U_227,U_226)) = times_times_int(U_229,times_times_int(U_228,times_times_int(U_227,U_226))),
inference(variable_rename,[status(thm)],[f_81_1]) ).
cnf(f_81_3,plain,
times_times_int(times_times_int(U_229,U_228),times_times_int(U_227,U_226)) = times_times_int(U_229,times_times_int(U_228,times_times_int(U_227,U_226))),
inference(clausify,[status(thm)],[f_81_2]) ).
fof(f_82_1,plain,
! [Lx_4,Ly_2,Rx_4,Ry_2] : times_times_nat(times_times_nat(Lx_4,Ly_2),times_times_nat(Rx_4,Ry_2)) = times_times_nat(Lx_4,times_times_nat(Ly_2,times_times_nat(Rx_4,Ry_2))),
inference(fof_nnf,[status(thm)],[fact_81_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J]) ).
fof(f_82_2,plain,
! [U_233,U_232,U_231,U_230] : times_times_nat(times_times_nat(U_233,U_232),times_times_nat(U_231,U_230)) = times_times_nat(U_233,times_times_nat(U_232,times_times_nat(U_231,U_230))),
inference(variable_rename,[status(thm)],[f_82_1]) ).
cnf(f_82_3,plain,
times_times_nat(times_times_nat(U_233,U_232),times_times_nat(U_231,U_230)) = times_times_nat(U_233,times_times_nat(U_232,times_times_nat(U_231,U_230))),
inference(clausify,[status(thm)],[f_82_2]) ).
fof(f_83_1,plain,
! [Lx_3,Ly_1,Rx_3] : times_times_int(times_times_int(Lx_3,Ly_1),Rx_3) = times_times_int(times_times_int(Lx_3,Rx_3),Ly_1),
inference(fof_nnf,[status(thm)],[fact_82_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J]) ).
fof(f_83_2,plain,
! [U_236,U_235,U_234] : times_times_int(times_times_int(U_236,U_235),U_234) = times_times_int(times_times_int(U_236,U_234),U_235),
inference(variable_rename,[status(thm)],[f_83_1]) ).
cnf(f_83_3,plain,
times_times_int(times_times_int(U_236,U_235),U_234) = times_times_int(times_times_int(U_236,U_234),U_235),
inference(clausify,[status(thm)],[f_83_2]) ).
fof(f_84_1,plain,
! [Lx_3,Ly_1,Rx_3] : times_times_nat(times_times_nat(Lx_3,Ly_1),Rx_3) = times_times_nat(times_times_nat(Lx_3,Rx_3),Ly_1),
inference(fof_nnf,[status(thm)],[fact_83_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J]) ).
fof(f_84_2,plain,
! [U_239,U_238,U_237] : times_times_nat(times_times_nat(U_239,U_238),U_237) = times_times_nat(times_times_nat(U_239,U_237),U_238),
inference(variable_rename,[status(thm)],[f_84_1]) ).
cnf(f_84_3,plain,
times_times_nat(times_times_nat(U_239,U_238),U_237) = times_times_nat(times_times_nat(U_239,U_237),U_238),
inference(clausify,[status(thm)],[f_84_2]) ).
fof(f_85_1,plain,
! [Lx_2,Ly,Rx_2] : times_times_int(times_times_int(Lx_2,Ly),Rx_2) = times_times_int(Lx_2,times_times_int(Ly,Rx_2)),
inference(fof_nnf,[status(thm)],[fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J]) ).
fof(f_85_2,plain,
! [U_242,U_241,U_240] : times_times_int(times_times_int(U_242,U_241),U_240) = times_times_int(U_242,times_times_int(U_241,U_240)),
inference(variable_rename,[status(thm)],[f_85_1]) ).
cnf(f_85_3,plain,
times_times_int(times_times_int(U_242,U_241),U_240) = times_times_int(U_242,times_times_int(U_241,U_240)),
inference(clausify,[status(thm)],[f_85_2]) ).
fof(f_86_1,plain,
! [Lx_2,Ly,Rx_2] : times_times_nat(times_times_nat(Lx_2,Ly),Rx_2) = times_times_nat(Lx_2,times_times_nat(Ly,Rx_2)),
inference(fof_nnf,[status(thm)],[fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J]) ).
fof(f_86_2,plain,
! [U_245,U_244,U_243] : times_times_nat(times_times_nat(U_245,U_244),U_243) = times_times_nat(U_245,times_times_nat(U_244,U_243)),
inference(variable_rename,[status(thm)],[f_86_1]) ).
cnf(f_86_3,plain,
times_times_nat(times_times_nat(U_245,U_244),U_243) = times_times_nat(U_245,times_times_nat(U_244,U_243)),
inference(clausify,[status(thm)],[f_86_2]) ).
fof(f_87_1,plain,
! [Lx_1,Rx_1,Ry_1] : times_times_int(Lx_1,times_times_int(Rx_1,Ry_1)) = times_times_int(times_times_int(Lx_1,Rx_1),Ry_1),
inference(fof_nnf,[status(thm)],[fact_86_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J]) ).
fof(f_87_2,plain,
! [U_248,U_247,U_246] : times_times_int(U_248,times_times_int(U_247,U_246)) = times_times_int(times_times_int(U_248,U_247),U_246),
inference(variable_rename,[status(thm)],[f_87_1]) ).
cnf(f_87_3,plain,
times_times_int(U_248,times_times_int(U_247,U_246)) = times_times_int(times_times_int(U_248,U_247),U_246),
inference(clausify,[status(thm)],[f_87_2]) ).
fof(f_88_1,plain,
! [Lx_1,Rx_1,Ry_1] : times_times_nat(Lx_1,times_times_nat(Rx_1,Ry_1)) = times_times_nat(times_times_nat(Lx_1,Rx_1),Ry_1),
inference(fof_nnf,[status(thm)],[fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J]) ).
fof(f_88_2,plain,
! [U_251,U_250,U_249] : times_times_nat(U_251,times_times_nat(U_250,U_249)) = times_times_nat(times_times_nat(U_251,U_250),U_249),
inference(variable_rename,[status(thm)],[f_88_1]) ).
cnf(f_88_3,plain,
times_times_nat(U_251,times_times_nat(U_250,U_249)) = times_times_nat(times_times_nat(U_251,U_250),U_249),
inference(clausify,[status(thm)],[f_88_2]) ).
fof(f_89_1,plain,
! [Lx,Rx,Ry] : times_times_int(Lx,times_times_int(Rx,Ry)) = times_times_int(Rx,times_times_int(Lx,Ry)),
inference(fof_nnf,[status(thm)],[fact_88_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J]) ).
fof(f_89_2,plain,
! [U_254,U_253,U_252] : times_times_int(U_254,times_times_int(U_253,U_252)) = times_times_int(U_253,times_times_int(U_254,U_252)),
inference(variable_rename,[status(thm)],[f_89_1]) ).
cnf(f_89_3,plain,
times_times_int(U_254,times_times_int(U_253,U_252)) = times_times_int(U_253,times_times_int(U_254,U_252)),
inference(clausify,[status(thm)],[f_89_2]) ).
fof(f_90_1,plain,
! [Lx,Rx,Ry] : times_times_nat(Lx,times_times_nat(Rx,Ry)) = times_times_nat(Rx,times_times_nat(Lx,Ry)),
inference(fof_nnf,[status(thm)],[fact_89_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J]) ).
fof(f_90_2,plain,
! [U_257,U_256,U_255] : times_times_nat(U_257,times_times_nat(U_256,U_255)) = times_times_nat(U_256,times_times_nat(U_257,U_255)),
inference(variable_rename,[status(thm)],[f_90_1]) ).
cnf(f_90_3,plain,
times_times_nat(U_257,times_times_nat(U_256,U_255)) = times_times_nat(U_256,times_times_nat(U_257,U_255)),
inference(clausify,[status(thm)],[f_90_2]) ).
fof(f_91_1,plain,
! [A_6,B_3] : times_times_int(A_6,B_3) = times_times_int(B_3,A_6),
inference(fof_nnf,[status(thm)],[fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J]) ).
fof(f_91_2,plain,
! [U_259,U_258] : times_times_int(U_259,U_258) = times_times_int(U_258,U_259),
inference(variable_rename,[status(thm)],[f_91_1]) ).
cnf(f_91_3,plain,
times_times_int(U_259,U_258) = times_times_int(U_258,U_259),
inference(clausify,[status(thm)],[f_91_2]) ).
fof(f_92_1,plain,
! [A_6,B_3] : times_times_nat(A_6,B_3) = times_times_nat(B_3,A_6),
inference(fof_nnf,[status(thm)],[fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J]) ).
fof(f_92_2,plain,
! [U_261,U_260] : times_times_nat(U_261,U_260) = times_times_nat(U_260,U_261),
inference(variable_rename,[status(thm)],[f_92_1]) ).
cnf(f_92_3,plain,
times_times_nat(U_261,U_260) = times_times_nat(U_260,U_261),
inference(clausify,[status(thm)],[f_92_2]) ).
fof(f_93_1,plain,
! [A_5,B_2,C_5,D_2] : plus_plus_int(plus_plus_int(A_5,B_2),plus_plus_int(C_5,D_2)) = plus_plus_int(plus_plus_int(A_5,C_5),plus_plus_int(B_2,D_2)),
inference(fof_nnf,[status(thm)],[fact_92_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J]) ).
fof(f_93_2,plain,
! [U_265,U_264,U_263,U_262] : plus_plus_int(plus_plus_int(U_265,U_264),plus_plus_int(U_263,U_262)) = plus_plus_int(plus_plus_int(U_265,U_263),plus_plus_int(U_264,U_262)),
inference(variable_rename,[status(thm)],[f_93_1]) ).
cnf(f_93_3,plain,
plus_plus_int(plus_plus_int(U_265,U_264),plus_plus_int(U_263,U_262)) = plus_plus_int(plus_plus_int(U_265,U_263),plus_plus_int(U_264,U_262)),
inference(clausify,[status(thm)],[f_93_2]) ).
fof(f_94_1,plain,
! [A_5,B_2,C_5,D_2] : plus_plus_nat(plus_plus_nat(A_5,B_2),plus_plus_nat(C_5,D_2)) = plus_plus_nat(plus_plus_nat(A_5,C_5),plus_plus_nat(B_2,D_2)),
inference(fof_nnf,[status(thm)],[fact_93_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J]) ).
fof(f_94_2,plain,
! [U_269,U_268,U_267,U_266] : plus_plus_nat(plus_plus_nat(U_269,U_268),plus_plus_nat(U_267,U_266)) = plus_plus_nat(plus_plus_nat(U_269,U_267),plus_plus_nat(U_268,U_266)),
inference(variable_rename,[status(thm)],[f_94_1]) ).
cnf(f_94_3,plain,
plus_plus_nat(plus_plus_nat(U_269,U_268),plus_plus_nat(U_267,U_266)) = plus_plus_nat(plus_plus_nat(U_269,U_267),plus_plus_nat(U_268,U_266)),
inference(clausify,[status(thm)],[f_94_2]) ).
fof(f_95_1,plain,
! [A_4,B_1,C_4] : plus_plus_int(plus_plus_int(A_4,B_1),C_4) = plus_plus_int(plus_plus_int(A_4,C_4),B_1),
inference(fof_nnf,[status(thm)],[fact_94_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J]) ).
fof(f_95_2,plain,
! [U_272,U_271,U_270] : plus_plus_int(plus_plus_int(U_272,U_271),U_270) = plus_plus_int(plus_plus_int(U_272,U_270),U_271),
inference(variable_rename,[status(thm)],[f_95_1]) ).
cnf(f_95_3,plain,
plus_plus_int(plus_plus_int(U_272,U_271),U_270) = plus_plus_int(plus_plus_int(U_272,U_270),U_271),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_96_1,plain,
! [A_4,B_1,C_4] : plus_plus_nat(plus_plus_nat(A_4,B_1),C_4) = plus_plus_nat(plus_plus_nat(A_4,C_4),B_1),
inference(fof_nnf,[status(thm)],[fact_95_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J]) ).
fof(f_96_2,plain,
! [U_275,U_274,U_273] : plus_plus_nat(plus_plus_nat(U_275,U_274),U_273) = plus_plus_nat(plus_plus_nat(U_275,U_273),U_274),
inference(variable_rename,[status(thm)],[f_96_1]) ).
cnf(f_96_3,plain,
plus_plus_nat(plus_plus_nat(U_275,U_274),U_273) = plus_plus_nat(plus_plus_nat(U_275,U_273),U_274),
inference(clausify,[status(thm)],[f_96_2]) ).
fof(f_97_1,plain,
! [A_3,B,C_3] : plus_plus_int(plus_plus_int(A_3,B),C_3) = plus_plus_int(A_3,plus_plus_int(B,C_3)),
inference(fof_nnf,[status(thm)],[fact_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J]) ).
fof(f_97_2,plain,
! [U_278,U_277,U_276] : plus_plus_int(plus_plus_int(U_278,U_277),U_276) = plus_plus_int(U_278,plus_plus_int(U_277,U_276)),
inference(variable_rename,[status(thm)],[f_97_1]) ).
cnf(f_97_3,plain,
plus_plus_int(plus_plus_int(U_278,U_277),U_276) = plus_plus_int(U_278,plus_plus_int(U_277,U_276)),
inference(clausify,[status(thm)],[f_97_2]) ).
fof(f_98_1,plain,
! [A_3,B,C_3] : plus_plus_nat(plus_plus_nat(A_3,B),C_3) = plus_plus_nat(A_3,plus_plus_nat(B,C_3)),
inference(fof_nnf,[status(thm)],[fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J]) ).
fof(f_98_2,plain,
! [U_281,U_280,U_279] : plus_plus_nat(plus_plus_nat(U_281,U_280),U_279) = plus_plus_nat(U_281,plus_plus_nat(U_280,U_279)),
inference(variable_rename,[status(thm)],[f_98_1]) ).
cnf(f_98_3,plain,
plus_plus_nat(plus_plus_nat(U_281,U_280),U_279) = plus_plus_nat(U_281,plus_plus_nat(U_280,U_279)),
inference(clausify,[status(thm)],[f_98_2]) ).
fof(f_99_1,plain,
! [A_2,C_2,D_1] : plus_plus_int(A_2,plus_plus_int(C_2,D_1)) = plus_plus_int(plus_plus_int(A_2,C_2),D_1),
inference(fof_nnf,[status(thm)],[fact_98_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J]) ).
fof(f_99_2,plain,
! [U_284,U_283,U_282] : plus_plus_int(U_284,plus_plus_int(U_283,U_282)) = plus_plus_int(plus_plus_int(U_284,U_283),U_282),
inference(variable_rename,[status(thm)],[f_99_1]) ).
cnf(f_99_3,plain,
plus_plus_int(U_284,plus_plus_int(U_283,U_282)) = plus_plus_int(plus_plus_int(U_284,U_283),U_282),
inference(clausify,[status(thm)],[f_99_2]) ).
fof(f_100_1,plain,
! [A_2,C_2,D_1] : plus_plus_nat(A_2,plus_plus_nat(C_2,D_1)) = plus_plus_nat(plus_plus_nat(A_2,C_2),D_1),
inference(fof_nnf,[status(thm)],[fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J]) ).
fof(f_100_2,plain,
! [U_287,U_286,U_285] : plus_plus_nat(U_287,plus_plus_nat(U_286,U_285)) = plus_plus_nat(plus_plus_nat(U_287,U_286),U_285),
inference(variable_rename,[status(thm)],[f_100_1]) ).
cnf(f_100_3,plain,
plus_plus_nat(U_287,plus_plus_nat(U_286,U_285)) = plus_plus_nat(plus_plus_nat(U_287,U_286),U_285),
inference(clausify,[status(thm)],[f_100_2]) ).
fof(f_101_1,plain,
! [A_1,C_1,D] : plus_plus_int(A_1,plus_plus_int(C_1,D)) = plus_plus_int(C_1,plus_plus_int(A_1,D)),
inference(fof_nnf,[status(thm)],[fact_100_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J]) ).
fof(f_101_2,plain,
! [U_290,U_289,U_288] : plus_plus_int(U_290,plus_plus_int(U_289,U_288)) = plus_plus_int(U_289,plus_plus_int(U_290,U_288)),
inference(variable_rename,[status(thm)],[f_101_1]) ).
cnf(f_101_3,plain,
plus_plus_int(U_290,plus_plus_int(U_289,U_288)) = plus_plus_int(U_289,plus_plus_int(U_290,U_288)),
inference(clausify,[status(thm)],[f_101_2]) ).
fof(f_102_1,plain,
! [A_1,C_1,D] : plus_plus_nat(A_1,plus_plus_nat(C_1,D)) = plus_plus_nat(C_1,plus_plus_nat(A_1,D)),
inference(fof_nnf,[status(thm)],[fact_101_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J]) ).
fof(f_102_2,plain,
! [U_293,U_292,U_291] : plus_plus_nat(U_293,plus_plus_nat(U_292,U_291)) = plus_plus_nat(U_292,plus_plus_nat(U_293,U_291)),
inference(variable_rename,[status(thm)],[f_102_1]) ).
cnf(f_102_3,plain,
plus_plus_nat(U_293,plus_plus_nat(U_292,U_291)) = plus_plus_nat(U_292,plus_plus_nat(U_293,U_291)),
inference(clausify,[status(thm)],[f_102_2]) ).
fof(f_103_1,plain,
! [A,C] : plus_plus_int(A,C) = plus_plus_int(C,A),
inference(fof_nnf,[status(thm)],[fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J]) ).
fof(f_103_2,plain,
! [U_295,U_294] : plus_plus_int(U_295,U_294) = plus_plus_int(U_294,U_295),
inference(variable_rename,[status(thm)],[f_103_1]) ).
cnf(f_103_3,plain,
plus_plus_int(U_295,U_294) = plus_plus_int(U_294,U_295),
inference(clausify,[status(thm)],[f_103_2]) ).
fof(f_104_1,plain,
! [A,C] : plus_plus_nat(A,C) = plus_plus_nat(C,A),
inference(fof_nnf,[status(thm)],[fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J]) ).
fof(f_104_2,plain,
! [U_297,U_296] : plus_plus_nat(U_297,U_296) = plus_plus_nat(U_296,U_297),
inference(variable_rename,[status(thm)],[f_104_1]) ).
cnf(f_104_3,plain,
plus_plus_nat(U_297,U_296) = plus_plus_nat(U_296,U_297),
inference(clausify,[status(thm)],[f_104_2]) ).
fof(f_105_1,plain,
! [X_2,Y_2] :
( ( number_number_of_int(X_2) = number_number_of_int(Y_2)
| X_2 != Y_2 )
& ( X_2 = Y_2
| number_number_of_int(X_2) != number_number_of_int(Y_2) ) ),
inference(fof_nnf,[status(thm)],[fact_104_eq__number__of]) ).
fof(f_105_2,plain,
! [U_299,U_298] :
( ( number_number_of_int(U_299) = number_number_of_int(U_298)
| U_299 != U_298 )
& ( U_299 = U_298
| number_number_of_int(U_299) != number_number_of_int(U_298) ) ),
inference(variable_rename,[status(thm)],[f_105_1]) ).
fof(f_105_3,plain,
( ! [U_303,U_301] :
( number_number_of_int(U_303) = number_number_of_int(U_301)
| U_303 != U_301 )
& ! [U_302,U_300] :
( U_302 = U_300
| number_number_of_int(U_302) != number_number_of_int(U_300) ) ),
inference(miniscope,[status(thm)],[f_105_2]) ).
cnf(f_105_4,plain,
( U_302 = U_300
| number_number_of_int(U_302) != number_number_of_int(U_300) ),
inference(clausify,[status(thm)],[f_105_3]) ).
cnf(f_105_5,plain,
( number_number_of_int(U_303) = number_number_of_int(U_301)
| U_303 != U_301 ),
inference(clausify,[status(thm)],[f_105_3]) ).
fof(f_106_1,plain,
! [W_1,X_2] :
( ( number_number_of_nat(W_1) = X_2
| X_2 != number_number_of_nat(W_1) )
& ( X_2 = number_number_of_nat(W_1)
| number_number_of_nat(W_1) != X_2 ) ),
inference(fof_nnf,[status(thm)],[fact_105_number__of__reorient]) ).
fof(f_106_2,plain,
! [U_305,U_304] :
( ( number_number_of_nat(U_305) = U_304
| U_304 != number_number_of_nat(U_305) )
& ( U_304 = number_number_of_nat(U_305)
| number_number_of_nat(U_305) != U_304 ) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
fof(f_106_3,plain,
( ! [U_309,U_307] :
( number_number_of_nat(U_309) = U_307
| U_307 != number_number_of_nat(U_309) )
& ! [U_308,U_306] :
( U_306 = number_number_of_nat(U_308)
| number_number_of_nat(U_308) != U_306 ) ),
inference(miniscope,[status(thm)],[f_106_2]) ).
cnf(f_106_4,plain,
( U_306 = number_number_of_nat(U_308)
| number_number_of_nat(U_308) != U_306 ),
inference(clausify,[status(thm)],[f_106_3]) ).
cnf(f_106_5,plain,
( number_number_of_nat(U_309) = U_307
| U_307 != number_number_of_nat(U_309) ),
inference(clausify,[status(thm)],[f_106_3]) ).
fof(f_107_1,plain,
! [W_1,X_2] :
( ( number_number_of_int(W_1) = X_2
| X_2 != number_number_of_int(W_1) )
& ( X_2 = number_number_of_int(W_1)
| number_number_of_int(W_1) != X_2 ) ),
inference(fof_nnf,[status(thm)],[fact_106_number__of__reorient]) ).
fof(f_107_2,plain,
! [U_311,U_310] :
( ( number_number_of_int(U_311) = U_310
| U_310 != number_number_of_int(U_311) )
& ( U_310 = number_number_of_int(U_311)
| number_number_of_int(U_311) != U_310 ) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
fof(f_107_3,plain,
( ! [U_315,U_313] :
( number_number_of_int(U_315) = U_313
| U_313 != number_number_of_int(U_315) )
& ! [U_314,U_312] :
( U_312 = number_number_of_int(U_314)
| number_number_of_int(U_314) != U_312 ) ),
inference(miniscope,[status(thm)],[f_107_2]) ).
cnf(f_107_4,plain,
( U_312 = number_number_of_int(U_314)
| number_number_of_int(U_314) != U_312 ),
inference(clausify,[status(thm)],[f_107_3]) ).
cnf(f_107_5,plain,
( number_number_of_int(U_315) = U_313
| U_313 != number_number_of_int(U_315) ),
inference(clausify,[status(thm)],[f_107_3]) ).
fof(f_108_1,plain,
! [K,L] :
( ( bit1(K) = bit1(L)
| K != L )
& ( K = L
| bit1(K) != bit1(L) ) ),
inference(fof_nnf,[status(thm)],[fact_107_rel__simps_I51_J]) ).
fof(f_108_2,plain,
! [U_317,U_316] :
( ( bit1(U_317) = bit1(U_316)
| U_317 != U_316 )
& ( U_317 = U_316
| bit1(U_317) != bit1(U_316) ) ),
inference(variable_rename,[status(thm)],[f_108_1]) ).
fof(f_108_3,plain,
( ! [U_321,U_319] :
( bit1(U_321) = bit1(U_319)
| U_321 != U_319 )
& ! [U_320,U_318] :
( U_320 = U_318
| bit1(U_320) != bit1(U_318) ) ),
inference(miniscope,[status(thm)],[f_108_2]) ).
cnf(f_108_4,plain,
( U_320 = U_318
| bit1(U_320) != bit1(U_318) ),
inference(clausify,[status(thm)],[f_108_3]) ).
cnf(f_108_5,plain,
( bit1(U_321) = bit1(U_319)
| U_321 != U_319 ),
inference(clausify,[status(thm)],[f_108_3]) ).
fof(f_109_1,plain,
! [K,L] :
( ( bit0(K) = bit0(L)
| K != L )
& ( K = L
| bit0(K) != bit0(L) ) ),
inference(fof_nnf,[status(thm)],[fact_108_rel__simps_I48_J]) ).
fof(f_109_2,plain,
! [U_323,U_322] :
( ( bit0(U_323) = bit0(U_322)
| U_323 != U_322 )
& ( U_323 = U_322
| bit0(U_323) != bit0(U_322) ) ),
inference(variable_rename,[status(thm)],[f_109_1]) ).
fof(f_109_3,plain,
( ! [U_327,U_325] :
( bit0(U_327) = bit0(U_325)
| U_327 != U_325 )
& ! [U_326,U_324] :
( U_326 = U_324
| bit0(U_326) != bit0(U_324) ) ),
inference(miniscope,[status(thm)],[f_109_2]) ).
cnf(f_109_4,plain,
( U_326 = U_324
| bit0(U_326) != bit0(U_324) ),
inference(clausify,[status(thm)],[f_109_3]) ).
cnf(f_109_5,plain,
( bit0(U_327) = bit0(U_325)
| U_327 != U_325 ),
inference(clausify,[status(thm)],[f_109_3]) ).
fof(f_110_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_109_zmult__assoc]) ).
fof(f_110_2,plain,
! [U_330,U_329,U_328] : times_times_int(times_times_int(U_330,U_329),U_328) = times_times_int(U_330,times_times_int(U_329,U_328)),
inference(variable_rename,[status(thm)],[f_110_1]) ).
cnf(f_110_3,plain,
times_times_int(times_times_int(U_330,U_329),U_328) = times_times_int(U_330,times_times_int(U_329,U_328)),
inference(clausify,[status(thm)],[f_110_2]) ).
fof(f_111_1,plain,
! [Z,W] : times_times_int(Z,W) = times_times_int(W,Z),
inference(fof_nnf,[status(thm)],[fact_110_zmult__commute]) ).
fof(f_111_2,plain,
! [U_332,U_331] : times_times_int(U_332,U_331) = times_times_int(U_331,U_332),
inference(variable_rename,[status(thm)],[f_111_1]) ).
cnf(f_111_3,plain,
times_times_int(U_332,U_331) = times_times_int(U_331,U_332),
inference(clausify,[status(thm)],[f_111_2]) ).
fof(f_112_1,plain,
! [K_1] : number_number_of_int(K_1) = K_1,
inference(fof_nnf,[status(thm)],[fact_111_number__of__is__id]) ).
fof(f_112_2,plain,
! [U_333] : number_number_of_int(U_333) = U_333,
inference(variable_rename,[status(thm)],[f_112_1]) ).
cnf(f_112_3,plain,
number_number_of_int(U_333) = U_333,
inference(clausify,[status(thm)],[f_112_2]) ).
fof(f_113_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_112_zadd__assoc]) ).
fof(f_113_2,plain,
! [U_336,U_335,U_334] : plus_plus_int(plus_plus_int(U_336,U_335),U_334) = plus_plus_int(U_336,plus_plus_int(U_335,U_334)),
inference(variable_rename,[status(thm)],[f_113_1]) ).
cnf(f_113_3,plain,
plus_plus_int(plus_plus_int(U_336,U_335),U_334) = plus_plus_int(U_336,plus_plus_int(U_335,U_334)),
inference(clausify,[status(thm)],[f_113_2]) ).
fof(f_114_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_113_zadd__left__commute]) ).
fof(f_114_2,plain,
! [U_339,U_338,U_337] : plus_plus_int(U_339,plus_plus_int(U_338,U_337)) = plus_plus_int(U_338,plus_plus_int(U_339,U_337)),
inference(variable_rename,[status(thm)],[f_114_1]) ).
cnf(f_114_3,plain,
plus_plus_int(U_339,plus_plus_int(U_338,U_337)) = plus_plus_int(U_338,plus_plus_int(U_339,U_337)),
inference(clausify,[status(thm)],[f_114_2]) ).
fof(f_115_1,plain,
! [Z,W] : plus_plus_int(Z,W) = plus_plus_int(W,Z),
inference(fof_nnf,[status(thm)],[fact_114_zadd__commute]) ).
fof(f_115_2,plain,
! [U_341,U_340] : plus_plus_int(U_341,U_340) = plus_plus_int(U_340,U_341),
inference(variable_rename,[status(thm)],[f_115_1]) ).
cnf(f_115_3,plain,
plus_plus_int(U_341,U_340) = plus_plus_int(U_340,U_341),
inference(clausify,[status(thm)],[f_115_2]) ).
fof(f_116_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_115_rel__simps_I12_J]) ).
fof(f_116_2,plain,
! [U_342] :
( ( ord_less_int(bit1(U_342),pls)
| ~ ord_less_int(U_342,pls) )
& ( ord_less_int(U_342,pls)
| ~ ord_less_int(bit1(U_342),pls) ) ),
inference(variable_rename,[status(thm)],[f_116_1]) ).
fof(f_116_3,plain,
( ! [U_344] :
( ord_less_int(bit1(U_344),pls)
| ~ ord_less_int(U_344,pls) )
& ! [U_343] :
( ord_less_int(U_343,pls)
| ~ ord_less_int(bit1(U_343),pls) ) ),
inference(miniscope,[status(thm)],[f_116_2]) ).
cnf(f_116_4,plain,
( ord_less_int(U_343,pls)
| ~ ord_less_int(bit1(U_343),pls) ),
inference(clausify,[status(thm)],[f_116_3]) ).
cnf(f_116_5,plain,
( ord_less_int(bit1(U_344),pls)
| ~ ord_less_int(U_344,pls) ),
inference(clausify,[status(thm)],[f_116_3]) ).
fof(f_117_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_116_less__int__code_I15_J]) ).
fof(f_117_2,plain,
! [U_346,U_345] :
( ( ord_less_int(bit1(U_346),bit0(U_345))
| ~ ord_less_int(U_346,U_345) )
& ( ord_less_int(U_346,U_345)
| ~ ord_less_int(bit1(U_346),bit0(U_345)) ) ),
inference(variable_rename,[status(thm)],[f_117_1]) ).
fof(f_117_3,plain,
( ! [U_350,U_348] :
( ord_less_int(bit1(U_350),bit0(U_348))
| ~ ord_less_int(U_350,U_348) )
& ! [U_349,U_347] :
( ord_less_int(U_349,U_347)
| ~ ord_less_int(bit1(U_349),bit0(U_347)) ) ),
inference(miniscope,[status(thm)],[f_117_2]) ).
cnf(f_117_4,plain,
( ord_less_int(U_349,U_347)
| ~ ord_less_int(bit1(U_349),bit0(U_347)) ),
inference(clausify,[status(thm)],[f_117_3]) ).
cnf(f_117_5,plain,
( ord_less_int(bit1(U_350),bit0(U_348))
| ~ ord_less_int(U_350,U_348) ),
inference(clausify,[status(thm)],[f_117_3]) ).
fof(f_118_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_117_rel__simps_I16_J]) ).
fof(f_118_2,plain,
! [U_352,U_351] :
( ( ord_less_int(bit1(U_352),bit0(U_351))
| ~ ord_less_int(U_352,U_351) )
& ( ord_less_int(U_352,U_351)
| ~ ord_less_int(bit1(U_352),bit0(U_351)) ) ),
inference(variable_rename,[status(thm)],[f_118_1]) ).
fof(f_118_3,plain,
( ! [U_356,U_354] :
( ord_less_int(bit1(U_356),bit0(U_354))
| ~ ord_less_int(U_356,U_354) )
& ! [U_355,U_353] :
( ord_less_int(U_355,U_353)
| ~ ord_less_int(bit1(U_355),bit0(U_353)) ) ),
inference(miniscope,[status(thm)],[f_118_2]) ).
cnf(f_118_4,plain,
( ord_less_int(U_355,U_353)
| ~ ord_less_int(bit1(U_355),bit0(U_353)) ),
inference(clausify,[status(thm)],[f_118_3]) ).
cnf(f_118_5,plain,
( ord_less_int(bit1(U_356),bit0(U_354))
| ~ ord_less_int(U_356,U_354) ),
inference(clausify,[status(thm)],[f_118_3]) ).
fof(f_119_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_118_rel__simps_I10_J]) ).
fof(f_119_2,plain,
! [U_357] :
( ( ord_less_int(bit0(U_357),pls)
| ~ ord_less_int(U_357,pls) )
& ( ord_less_int(U_357,pls)
| ~ ord_less_int(bit0(U_357),pls) ) ),
inference(variable_rename,[status(thm)],[f_119_1]) ).
fof(f_119_3,plain,
( ! [U_359] :
( ord_less_int(bit0(U_359),pls)
| ~ ord_less_int(U_359,pls) )
& ! [U_358] :
( ord_less_int(U_358,pls)
| ~ ord_less_int(bit0(U_358),pls) ) ),
inference(miniscope,[status(thm)],[f_119_2]) ).
cnf(f_119_4,plain,
( ord_less_int(U_358,pls)
| ~ ord_less_int(bit0(U_358),pls) ),
inference(clausify,[status(thm)],[f_119_3]) ).
cnf(f_119_5,plain,
( ord_less_int(bit0(U_359),pls)
| ~ ord_less_int(U_359,pls) ),
inference(clausify,[status(thm)],[f_119_3]) ).
fof(f_120_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_119_rel__simps_I4_J]) ).
fof(f_120_2,plain,
! [U_360] :
( ( ord_less_int(pls,bit0(U_360))
| ~ ord_less_int(pls,U_360) )
& ( ord_less_int(pls,U_360)
| ~ ord_less_int(pls,bit0(U_360)) ) ),
inference(variable_rename,[status(thm)],[f_120_1]) ).
fof(f_120_3,plain,
( ! [U_362] :
( ord_less_int(pls,bit0(U_362))
| ~ ord_less_int(pls,U_362) )
& ! [U_361] :
( ord_less_int(pls,U_361)
| ~ ord_less_int(pls,bit0(U_361)) ) ),
inference(miniscope,[status(thm)],[f_120_2]) ).
cnf(f_120_4,plain,
( ord_less_int(pls,U_361)
| ~ ord_less_int(pls,bit0(U_361)) ),
inference(clausify,[status(thm)],[f_120_3]) ).
cnf(f_120_5,plain,
( ord_less_int(pls,bit0(U_362))
| ~ ord_less_int(pls,U_362) ),
inference(clausify,[status(thm)],[f_120_3]) ).
fof(f_121_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_120_rel__simps_I22_J]) ).
fof(f_121_2,plain,
! [U_363] :
( ( ord_less_eq_int(pls,bit1(U_363))
| ~ ord_less_eq_int(pls,U_363) )
& ( ord_less_eq_int(pls,U_363)
| ~ ord_less_eq_int(pls,bit1(U_363)) ) ),
inference(variable_rename,[status(thm)],[f_121_1]) ).
fof(f_121_3,plain,
( ! [U_365] :
( ord_less_eq_int(pls,bit1(U_365))
| ~ ord_less_eq_int(pls,U_365) )
& ! [U_364] :
( ord_less_eq_int(pls,U_364)
| ~ ord_less_eq_int(pls,bit1(U_364)) ) ),
inference(miniscope,[status(thm)],[f_121_2]) ).
cnf(f_121_4,plain,
( ord_less_eq_int(pls,U_364)
| ~ ord_less_eq_int(pls,bit1(U_364)) ),
inference(clausify,[status(thm)],[f_121_3]) ).
cnf(f_121_5,plain,
( ord_less_eq_int(pls,bit1(U_365))
| ~ ord_less_eq_int(pls,U_365) ),
inference(clausify,[status(thm)],[f_121_3]) ).
fof(f_122_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_121_less__eq__int__code_I14_J]) ).
fof(f_122_2,plain,
! [U_367,U_366] :
( ( ord_less_eq_int(bit0(U_367),bit1(U_366))
| ~ ord_less_eq_int(U_367,U_366) )
& ( ord_less_eq_int(U_367,U_366)
| ~ ord_less_eq_int(bit0(U_367),bit1(U_366)) ) ),
inference(variable_rename,[status(thm)],[f_122_1]) ).
fof(f_122_3,plain,
( ! [U_371,U_369] :
( ord_less_eq_int(bit0(U_371),bit1(U_369))
| ~ ord_less_eq_int(U_371,U_369) )
& ! [U_370,U_368] :
( ord_less_eq_int(U_370,U_368)
| ~ ord_less_eq_int(bit0(U_370),bit1(U_368)) ) ),
inference(miniscope,[status(thm)],[f_122_2]) ).
cnf(f_122_4,plain,
( ord_less_eq_int(U_370,U_368)
| ~ ord_less_eq_int(bit0(U_370),bit1(U_368)) ),
inference(clausify,[status(thm)],[f_122_3]) ).
cnf(f_122_5,plain,
( ord_less_eq_int(bit0(U_371),bit1(U_369))
| ~ ord_less_eq_int(U_371,U_369) ),
inference(clausify,[status(thm)],[f_122_3]) ).
fof(f_123_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_122_rel__simps_I32_J]) ).
fof(f_123_2,plain,
! [U_373,U_372] :
( ( ord_less_eq_int(bit0(U_373),bit1(U_372))
| ~ ord_less_eq_int(U_373,U_372) )
& ( ord_less_eq_int(U_373,U_372)
| ~ ord_less_eq_int(bit0(U_373),bit1(U_372)) ) ),
inference(variable_rename,[status(thm)],[f_123_1]) ).
fof(f_123_3,plain,
( ! [U_377,U_375] :
( ord_less_eq_int(bit0(U_377),bit1(U_375))
| ~ ord_less_eq_int(U_377,U_375) )
& ! [U_376,U_374] :
( ord_less_eq_int(U_376,U_374)
| ~ ord_less_eq_int(bit0(U_376),bit1(U_374)) ) ),
inference(miniscope,[status(thm)],[f_123_2]) ).
cnf(f_123_4,plain,
( ord_less_eq_int(U_376,U_374)
| ~ ord_less_eq_int(bit0(U_376),bit1(U_374)) ),
inference(clausify,[status(thm)],[f_123_3]) ).
cnf(f_123_5,plain,
( ord_less_eq_int(bit0(U_377),bit1(U_375))
| ~ ord_less_eq_int(U_377,U_375) ),
inference(clausify,[status(thm)],[f_123_3]) ).
fof(f_124_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_124_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_124_1]) ).
fof(f_124_3,negated_conjecture,
! [U_379,U_378] : plus_plus_int(power_power_int(U_379,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_378,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_124_2]) ).
fof(f_124_4,negated_conjecture,
! [U_378,U_379] : plus_plus_int(power_power_int(U_379,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_378,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_124_3]) ).
cnf(f_124_5,negated_conjecture,
plus_plus_int(power_power_int(U_379,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_378,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_124_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,
( bit1(Eq_x_0) = bit1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( bit0(Eq_x_0) = bit0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( number_number_of_nat(Eq_x_0) = number_number_of_nat(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( power_power_int(Eq_x_0,Eq_x_1) = power_power_int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( plus_plus_int(Eq_x_0,Eq_x_1) = plus_plus_int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( number_number_of_int(Eq_x_0) = number_number_of_int(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( times_times_int(Eq_x_0,Eq_x_1) = times_times_int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( plus_plus_nat(Eq_x_0,Eq_x_1) = plus_plus_nat(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_nat(Eq_x_0,Eq_x_1) = power_power_nat(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( times_times_nat(Eq_x_0,Eq_x_1) = times_times_nat(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( ord_less_eq_int(Eq_y_0,Eq_y_1)
| ~ ord_less_eq_int(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( ord_less_int(Eq_y_0,Eq_y_1)
| ~ ord_less_int(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| 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,
( twoSqu526106917sum2sq(Eq_y_0)
| ~ twoSqu526106917sum2sq(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( ord_less_eq_nat(Eq_y_0,Eq_y_1)
| ~ ord_less_eq_nat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( ord_less_nat(Eq_y_0,Eq_y_1)
| ~ ord_less_nat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| 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.02 % Problem : NUM926+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % 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/5.38 % Computer : n006.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sat Sep 19 19:26:02 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.93/6.25 % SZS status Theorem for theBenchmark
% 0.93/6.25 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------