%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM924^3 : TPTP v9.2.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 02:12:26 PM UTC 2025
% Result : Theorem 8.26s 8.42s
% Output : Proof 8.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM924^3 : TPTP v9.2.0. Released v5.3.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 22:24:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 8.26/8.42 % SZS status Theorem
% 8.26/8.42 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 8.26/8.42 % Inferences: 0
% 8.26/8.42 % SZS output start Proof
% 8.26/8.42 thf(ty_int, type, int : $tType).
% 8.26/8.42 thf(ty_nat, type, nat : $tType).
% 8.26/8.42 thf(ty_eigen__2, type, eigen__2 : int).
% 8.26/8.42 thf(ty_s, type, s : int).
% 8.26/8.42 thf(ty_eigen__1, type, eigen__1 : int).
% 8.26/8.42 thf(ty_eigen__0, type, eigen__0 : int).
% 8.26/8.42 thf(ty_bit1, type, bit1 : (int>int)).
% 8.26/8.42 thf(ty_bit0, type, bit0 : (int>int)).
% 8.26/8.42 thf(ty_zcong, type, zcong : (int>int>int>$o)).
% 8.26/8.42 thf(ty_times_times_int, type, times_times_int : (int>int>int)).
% 8.26/8.42 thf(ty_eigen__3, type, eigen__3 : int).
% 8.26/8.42 thf(ty_ord_less_eq_int, type, ord_less_eq_int : (int>int>$o)).
% 8.26/8.42 thf(ty_min, type, min : int).
% 8.26/8.42 thf(ty_t, type, t : int).
% 8.26/8.42 thf(ty_zero_zero_int, type, zero_zero_int : int).
% 8.26/8.42 thf(ty_one_one_int, type, one_one_int : int).
% 8.26/8.42 thf(ty_pls, type, pls : int).
% 8.26/8.42 thf(ty_power_power_int, type, power_power_int : (int>nat>int)).
% 8.26/8.42 thf(ty_plus_plus_int, type, plus_plus_int : (int>int>int)).
% 8.26/8.42 thf(ty_ord_less_int, type, ord_less_int : (int>int>$o)).
% 8.26/8.42 thf(ty_number_number_of_int, type, number_number_of_int : (int>int)).
% 8.26/8.42 thf(ty_s1, type, s1 : int).
% 8.26/8.42 thf(ty_m, type, m : int).
% 8.26/8.42 thf(ty_number_number_of_nat, type, number_number_of_nat : (int>nat)).
% 8.26/8.42 thf(conj_0,conjecture,((ord_less_int @ ((plus_plus_int @ ((power_power_int @ s) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ one_one_int)) @ zero_zero_int)).
% 8.26/8.42 thf(h0,negated_conjecture,(~(((ord_less_int @ ((plus_plus_int @ ((power_power_int @ s) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ one_one_int)) @ zero_zero_int))),inference(assume_negation,[status(cth)],[conj_0])).
% 8.26/8.42 thf(h1,assumption,(((zcong @ ((power_power_int @ eigen__0) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ (number_number_of_int @ min)) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h2,assumption,(~(((~((((ord_less_eq_int @ zero_zero_int) @ eigen__1) => (~(((ord_less_int @ eigen__1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ eigen__1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h3,assumption,(~((((ord_less_eq_int @ zero_zero_int) @ eigen__1) => (~(((ord_less_int @ eigen__1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h4,assumption,(((zcong @ s1) @ eigen__1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h5,assumption,((ord_less_eq_int @ zero_zero_int) @ eigen__1),introduced(assumption,[])).
% 8.26/8.42 thf(h6,assumption,((ord_less_int @ eigen__1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h7,assumption,(~(((~(((~((((ord_less_eq_int @ zero_zero_int) @ eigen__2) => (~(((ord_less_int @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((![X1:int]:((~(((~((((ord_less_eq_int @ zero_zero_int) @ X1) => (~(((ord_less_int @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (X1 = eigen__2)))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h8,assumption,(~(((~((((ord_less_eq_int @ zero_zero_int) @ eigen__2) => (~(((ord_less_int @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h9,assumption,(![X1:int]:((~(((~((((ord_less_eq_int @ zero_zero_int) @ X1) => (~(((ord_less_int @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (X1 = eigen__2))),introduced(assumption,[])).
% 8.26/8.42 thf(h10,assumption,(~((((ord_less_eq_int @ zero_zero_int) @ eigen__2) => (~(((ord_less_int @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h11,assumption,(((zcong @ s1) @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h12,assumption,((ord_less_eq_int @ zero_zero_int) @ eigen__2),introduced(assumption,[])).
% 8.26/8.42 thf(h13,assumption,((ord_less_int @ eigen__2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h14,assumption,(~((((ord_less_eq_int @ zero_zero_int) @ s) => (~(((ord_less_int @ s) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))),introduced(assumption,[])).
% 8.26/8.42 thf(h15,assumption,(((zcong @ s1) @ s) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h16,assumption,((ord_less_eq_int @ zero_zero_int) @ s),introduced(assumption,[])).
% 8.26/8.42 thf(h17,assumption,((ord_less_int @ s) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)),introduced(assumption,[])).
% 8.26/8.42 thf(h18,assumption,(((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)) @ eigen__3)),introduced(assumption,[])).
% 8.26/8.42 thf(h19,assumption,(~((t = zero_zero_int))),introduced(assumption,[])).
% 8.26/8.42 thf(h20,assumption,(((plus_plus_int @ ((power_power_int @ s) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ one_one_int) = zero_zero_int),introduced(assumption,[])).
% 8.26/8.42 thf(pax136, axiom, (p136=>![X44:int]:(fbit0 @ X44)=(fplus_plus_int @ X44 @ X44)), file('<stdin>', pax136)).
% 8.26/8.42 thf(pax59, axiom, (p59=>![X80:int, X81:int]:(ftimes_times_int @ (fbit0 @ X80) @ X81)=(fbit0 @ (ftimes_times_int @ X80 @ X81))), file('<stdin>', pax59)).
% 8.26/8.42 thf(pax62, axiom, (p62=>![X80:int]:(ftimes_times_int @ fone_one_int @ X80)=(X80)), file('<stdin>', pax62)).
% 8.26/8.42 thf(pax141, axiom, (p141=>![X44:int]:(ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X44))=(fnumber_number_of_int @ (fbit0 @ X44))), file('<stdin>', pax141)).
% 8.26/8.42 thf(ax110, axiom, p136, file('<stdin>', ax110)).
% 8.26/8.42 thf(ax187, axiom, p59, file('<stdin>', ax187)).
% 8.26/8.42 thf(ax184, axiom, p62, file('<stdin>', ax184)).
% 8.26/8.42 thf(pax117, axiom, (p117=>(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), file('<stdin>', pax117)).
% 8.26/8.42 thf(pax93, axiom, (p93=>![X72:int, X73:int]:(fplus_plus_int @ X72 @ X73)=(fplus_plus_int @ X73 @ X72)), file('<stdin>', pax93)).
% 8.26/8.42 thf(pax209, axiom, (p209=>![X15:int]:(ftimes_times_int @ X15 @ X15)=(fpower_power_int @ X15 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), file('<stdin>', pax209)).
% 8.26/8.42 thf(pax128, axiom, (p128=>(fpls)=(fzero_zero_int)), file('<stdin>', pax128)).
% 8.26/8.42 thf(pax2, axiom, (p2=>(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)), file('<stdin>', pax2)).
% 8.26/8.42 thf(ax105, axiom, p141, file('<stdin>', ax105)).
% 8.26/8.42 thf(ax129, axiom, p117, file('<stdin>', ax129)).
% 8.26/8.42 thf(ax153, axiom, p93, file('<stdin>', ax153)).
% 8.26/8.42 thf(ax37, axiom, p209, file('<stdin>', ax37)).
% 8.26/8.42 thf(pax241, axiom, (p241=>![X1:int]:(ftimes_times_int @ X1 @ fzero_zero_int)=(fzero_zero_int)), file('<stdin>', pax241)).
% 8.26/8.42 thf(ax118, axiom, p128, file('<stdin>', ax118)).
% 8.26/8.42 thf(pax112, axiom, (p112=>![X49:int, X31:int]:~(ford_less_int @ (fplus_plus_int @ (ftimes_times_int @ X49 @ X49) @ (ftimes_times_int @ X31 @ X31)) @ fzero_zero_int)), file('<stdin>', pax112)).
% 8.26/8.42 thf(pax61, axiom, (p61=>![X80:int]:(ftimes_times_int @ X80 @ fone_one_int)=(X80)), file('<stdin>', pax61)).
% 8.26/8.42 thf(pax1, axiom, (p1=>ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)), file('<stdin>', pax1)).
% 8.26/8.42 thf(ax244, axiom, p2, file('<stdin>', ax244)).
% 8.26/8.42 thf(ax5, axiom, p241, file('<stdin>', ax5)).
% 8.26/8.42 thf(ax134, axiom, p112, file('<stdin>', ax134)).
% 8.26/8.42 thf(ax185, axiom, p61, file('<stdin>', ax185)).
% 8.26/8.42 thf(ax245, axiom, p1, file('<stdin>', ax245)).
% 8.26/8.42 thf(c_0_26, plain, ![X345:int]:(~p136|(fbit0 @ X345)=(fplus_plus_int @ X345 @ X345)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax136])])])).
% 8.26/8.42 thf(c_0_27, plain, ![X523:int, X524:int]:(~p59|(ftimes_times_int @ (fbit0 @ X523) @ X524)=(fbit0 @ (ftimes_times_int @ X523 @ X524))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax59])])])).
% 8.26/8.42 thf(c_0_28, plain, ![X519:int]:(~p62|(ftimes_times_int @ fone_one_int @ X519)=(X519)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax62])])])).
% 8.26/8.42 thf(c_0_29, plain, ![X331:int]:(~p141|(ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X331))=(fnumber_number_of_int @ (fbit0 @ X331))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax141])])])).
% 8.26/8.42 thf(c_0_30, plain, ![X1:int]:((fbit0 @ X1)=(fplus_plus_int @ X1 @ X1)|~p136), inference(split_conjunct,[status(thm)],[c_0_26])).
% 8.26/8.42 thf(c_0_31, plain, p136, inference(split_conjunct,[status(thm)],[ax110])).
% 8.26/8.42 thf(c_0_32, plain, ![X1:int, X4:int]:((ftimes_times_int @ (fbit0 @ X1) @ X4)=(fbit0 @ (ftimes_times_int @ X1 @ X4))|~p59), inference(split_conjunct,[status(thm)],[c_0_27])).
% 8.26/8.42 thf(c_0_33, plain, p59, inference(split_conjunct,[status(thm)],[ax187])).
% 8.26/8.42 thf(c_0_34, plain, ![X1:int]:((ftimes_times_int @ fone_one_int @ X1)=(X1)|~p62), inference(split_conjunct,[status(thm)],[c_0_28])).
% 8.26/8.42 thf(c_0_35, plain, p62, inference(split_conjunct,[status(thm)],[ax184])).
% 8.26/8.42 thf(c_0_36, plain, (~p117|(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), inference(fof_nnf,[status(thm)],[pax117])).
% 8.26/8.42 thf(c_0_37, plain, ![X437:int, X438:int]:(~p93|(fplus_plus_int @ X437 @ X438)=(fplus_plus_int @ X438 @ X437)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax93])])])).
% 8.26/8.42 thf(c_0_38, plain, ![X201:int]:(~p209|(ftimes_times_int @ X201 @ X201)=(fpower_power_int @ X201 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax209])])])).
% 8.26/8.42 thf(c_0_39, plain, (~p128|(fpls)=(fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax128])).
% 8.26/8.42 thf(c_0_40, plain, (~p2|(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)), inference(fof_nnf,[status(thm)],[pax2])).
% 8.26/8.42 thf(c_0_41, plain, ![X1:int]:((ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X1))=(fnumber_number_of_int @ (fbit0 @ X1))|~p141), inference(split_conjunct,[status(thm)],[c_0_29])).
% 8.26/8.42 thf(c_0_42, plain, ![X1:int]:(fplus_plus_int @ X1 @ X1)=(fbit0 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 8.26/8.42 thf(c_0_43, plain, ![X1:int, X4:int]:(ftimes_times_int @ (fbit0 @ X1) @ X4)=(fbit0 @ (ftimes_times_int @ X1 @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 8.26/8.42 thf(c_0_44, plain, ![X1:int]:(ftimes_times_int @ fone_one_int @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 8.26/8.42 thf(c_0_45, plain, p141, inference(split_conjunct,[status(thm)],[ax105])).
% 8.26/8.42 thf(c_0_46, plain, ((fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))|~p117), inference(split_conjunct,[status(thm)],[c_0_36])).
% 8.26/8.42 thf(c_0_47, plain, p117, inference(split_conjunct,[status(thm)],[ax129])).
% 8.26/8.42 thf(c_0_48, plain, ![X4:int, X1:int]:((fplus_plus_int @ X1 @ X4)=(fplus_plus_int @ X4 @ X1)|~p93), inference(split_conjunct,[status(thm)],[c_0_37])).
% 8.26/8.42 thf(c_0_49, plain, p93, inference(split_conjunct,[status(thm)],[ax153])).
% 8.26/8.42 thf(c_0_50, plain, ![X1:int]:((ftimes_times_int @ X1 @ X1)=(fpower_power_int @ X1 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))|~p209), inference(split_conjunct,[status(thm)],[c_0_38])).
% 8.26/8.42 thf(c_0_51, plain, p209, inference(split_conjunct,[status(thm)],[ax37])).
% 8.26/8.42 thf(c_0_52, plain, ![X107:int]:(~p241|(ftimes_times_int @ X107 @ fzero_zero_int)=(fzero_zero_int)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax241])])])).
% 8.26/8.42 thf(c_0_53, plain, ((fpls)=(fzero_zero_int)|~p128), inference(split_conjunct,[status(thm)],[c_0_39])).
% 8.26/8.42 thf(c_0_54, plain, p128, inference(split_conjunct,[status(thm)],[ax118])).
% 8.26/8.42 thf(c_0_55, plain, ![X379:int, X380:int]:(~p112|~ford_less_int @ (fplus_plus_int @ (ftimes_times_int @ X379 @ X379) @ (ftimes_times_int @ X380 @ X380)) @ fzero_zero_int), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax112])])])])).
% 8.26/8.42 thf(c_0_56, plain, ![X521:int]:(~p61|(ftimes_times_int @ X521 @ fone_one_int)=(X521)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax61])])])).
% 8.26/8.42 thf(c_0_57, plain, (~p1|ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax1])).
% 8.26/8.42 thf(c_0_58, plain, ((fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)|~p2), inference(split_conjunct,[status(thm)],[c_0_40])).
% 8.26/8.42 thf(c_0_59, plain, ![X1:int]:(fnumber_number_of_int @ (fbit0 @ X1))=(fbit0 @ (fnumber_number_of_int @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42]), c_0_43]), c_0_44]), c_0_45])])).
% 8.26/8.42 thf(c_0_60, plain, (fnumber_number_of_int @ (fbit1 @ fpls))=(fone_one_int), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 8.26/8.42 thf(c_0_61, plain, ![X4:int, X1:int]:(fplus_plus_int @ X1 @ X4)=(fplus_plus_int @ X4 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 8.26/8.42 thf(c_0_62, plain, ![X1:int]:(ftimes_times_int @ X1 @ X1)=(fpower_power_int @ X1 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 8.26/8.42 thf(c_0_63, plain, p2, inference(split_conjunct,[status(thm)],[ax244])).
% 8.26/8.42 thf(c_0_64, plain, ![X1:int]:((ftimes_times_int @ X1 @ fzero_zero_int)=(fzero_zero_int)|~p241), inference(split_conjunct,[status(thm)],[c_0_52])).
% 8.26/8.42 thf(c_0_65, plain, (fzero_zero_int)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 8.26/8.42 thf(c_0_66, plain, p241, inference(split_conjunct,[status(thm)],[ax5])).
% 8.26/8.42 thf(c_0_67, plain, ![X1:int, X4:int]:(~p112|~ford_less_int @ (fplus_plus_int @ (ftimes_times_int @ X1 @ X1) @ (ftimes_times_int @ X4 @ X4)) @ fzero_zero_int), inference(split_conjunct,[status(thm)],[c_0_55])).
% 8.26/8.42 thf(c_0_68, plain, p112, inference(split_conjunct,[status(thm)],[ax134])).
% 8.26/8.42 thf(c_0_69, plain, ![X1:int]:((ftimes_times_int @ X1 @ fone_one_int)=(X1)|~p61), inference(split_conjunct,[status(thm)],[c_0_56])).
% 8.26/8.42 thf(c_0_70, plain, p61, inference(split_conjunct,[status(thm)],[ax185])).
% 8.26/8.42 thf(c_0_71, plain, (ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)|~p1), inference(split_conjunct,[status(thm)],[c_0_57])).
% 8.26/8.42 thf(c_0_72, plain, (ftimes_times_int @ (fplus_plus_int @ fone_one_int @ (fbit0 @ (fbit0 @ fm))) @ ft)=(fplus_plus_int @ fone_one_int @ (ftimes_times_int @ fs @ fs)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59]), c_0_59]), c_0_60]), c_0_43]), c_0_43]), c_0_44]), c_0_61]), c_0_62]), c_0_61]), c_0_63])])).
% 8.26/8.42 thf(c_0_73, plain, ![X1:int]:(ftimes_times_int @ X1 @ fpls)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65]), c_0_65]), c_0_66])])).
% 8.26/8.42 thf(c_0_74, plain, p1, inference(split_conjunct,[status(thm)],[ax245])).
% 8.26/8.42 thf(c_0_75, plain, ![X1:int, X4:int]:~ford_less_int @ (fplus_plus_int @ (ftimes_times_int @ X1 @ X1) @ (ftimes_times_int @ X4 @ X4)) @ fpls, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68]), c_0_65])])).
% 8.26/8.42 thf(c_0_76, plain, ![X1:int]:(ftimes_times_int @ X1 @ fone_one_int)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 8.26/8.42 thf(c_0_77, plain, ford_less_int @ (fplus_plus_int @ fone_one_int @ (ftimes_times_int @ fs @ fs)) @ fpls, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_59]), c_0_59]), c_0_60]), c_0_43]), c_0_43]), c_0_44]), c_0_61]), c_0_72]), c_0_59]), c_0_59]), c_0_60]), c_0_43]), c_0_43]), c_0_44]), c_0_61]), c_0_65]), c_0_73]), c_0_74])])).
% 8.26/8.42 thf(c_0_78, plain, ![X1:int]:~ford_less_int @ (fplus_plus_int @ fone_one_int @ (ftimes_times_int @ X1 @ X1)) @ fpls, inference(spm,[status(thm)],[c_0_75, c_0_76])).
% 8.26/8.42 thf(c_0_79, plain, ($false), inference(sr,[status(thm)],[c_0_77, c_0_78]), ['proof']).
% 8.26/8.42 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h19,h18,h16,h17,h14,h15,h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0])],[])).
% 8.26/8.42 thf(pax136, axiom, (p136=>![X49:int]:(fbit0 @ X49)=(fplus_plus_int @ X49 @ X49)), file('<stdin>', pax136)).
% 8.26/8.42 thf(pax59, axiom, (p59=>![X85:int, X86:int]:(ftimes_times_int @ (fbit0 @ X85) @ X86)=(fbit0 @ (ftimes_times_int @ X85 @ X86))), file('<stdin>', pax59)).
% 8.26/8.42 thf(pax62, axiom, (p62=>![X85:int]:(ftimes_times_int @ fone_one_int @ X85)=(X85)), file('<stdin>', pax62)).
% 8.26/8.42 thf(pax93, axiom, (p93=>![X77:int, X78:int]:(fplus_plus_int @ X77 @ X78)=(fplus_plus_int @ X78 @ X77)), file('<stdin>', pax93)).
% 8.26/8.42 thf(pax209, axiom, (p209=>![X20:int]:(ftimes_times_int @ X20 @ X20)=(fpower_power_int @ X20 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), file('<stdin>', pax209)).
% 8.26/8.42 thf(pax128, axiom, (p128=>(fpls)=(fzero_zero_int)), file('<stdin>', pax128)).
% 8.26/8.42 thf(pax141, axiom, (p141=>![X49:int]:(ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X49))=(fnumber_number_of_int @ (fbit0 @ X49))), file('<stdin>', pax141)).
% 8.26/8.42 thf(ax122, axiom, p136, file('<stdin>', ax122)).
% 8.26/8.42 thf(ax199, axiom, p59, file('<stdin>', ax199)).
% 8.26/8.42 thf(ax196, axiom, p62, file('<stdin>', ax196)).
% 8.26/8.42 thf(pax117, axiom, (p117=>(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), file('<stdin>', pax117)).
% 8.26/8.42 thf(pax248, axiom, (p248=>(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(fzero_zero_int)), file('<stdin>', pax248)).
% 8.26/8.42 thf(ax165, axiom, p93, file('<stdin>', ax165)).
% 8.26/8.42 thf(ax49, axiom, p209, file('<stdin>', ax49)).
% 8.26/8.42 thf(ax130, axiom, p128, file('<stdin>', ax130)).
% 8.26/8.42 thf(pax2, axiom, (p2=>(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)), file('<stdin>', pax2)).
% 8.26/8.42 thf(ax117, axiom, p141, file('<stdin>', ax117)).
% 8.26/8.42 thf(ax141, axiom, p117, file('<stdin>', ax141)).
% 8.26/8.42 thf(ax255, axiom, p248, file('<stdin>', ax255)).
% 8.26/8.42 thf(pax241, axiom, (p241=>![X8:int]:(ftimes_times_int @ X8 @ fzero_zero_int)=(fzero_zero_int)), file('<stdin>', pax241)).
% 8.26/8.42 thf(nax130, axiom, (p130<=ford_less_int @ fpls @ fpls), file('<stdin>', nax130)).
% 8.26/8.42 thf(ax128, axiom, ~(p130), file('<stdin>', ax128)).
% 8.26/8.42 thf(pax1, axiom, (p1=>ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)), file('<stdin>', pax1)).
% 8.26/8.42 thf(ax256, axiom, p2, file('<stdin>', ax256)).
% 8.26/8.42 thf(ax17, axiom, p241, file('<stdin>', ax17)).
% 8.26/8.42 thf(ax257, axiom, p1, file('<stdin>', ax257)).
% 8.26/8.42 thf(c_0_26, plain, ![X384:int]:(~p136|(fbit0 @ X384)=(fplus_plus_int @ X384 @ X384)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax136])])])).
% 8.26/8.42 thf(c_0_27, plain, ![X562:int, X563:int]:(~p59|(ftimes_times_int @ (fbit0 @ X562) @ X563)=(fbit0 @ (ftimes_times_int @ X562 @ X563))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax59])])])).
% 8.26/8.42 thf(c_0_28, plain, ![X558:int]:(~p62|(ftimes_times_int @ fone_one_int @ X558)=(X558)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax62])])])).
% 8.26/8.42 thf(c_0_29, plain, ![X476:int, X477:int]:(~p93|(fplus_plus_int @ X476 @ X477)=(fplus_plus_int @ X477 @ X476)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax93])])])).
% 8.26/8.42 thf(c_0_30, plain, ![X240:int]:(~p209|(ftimes_times_int @ X240 @ X240)=(fpower_power_int @ X240 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax209])])])).
% 8.26/8.42 thf(c_0_31, plain, (~p128|(fpls)=(fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax128])).
% 8.26/8.42 thf(c_0_32, plain, ![X370:int]:(~p141|(ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X370))=(fnumber_number_of_int @ (fbit0 @ X370))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax141])])])).
% 8.26/8.42 thf(c_0_33, plain, ![X1:int]:((fbit0 @ X1)=(fplus_plus_int @ X1 @ X1)|~p136), inference(split_conjunct,[status(thm)],[c_0_26])).
% 8.26/8.42 thf(c_0_34, plain, p136, inference(split_conjunct,[status(thm)],[ax122])).
% 8.26/8.42 thf(c_0_35, plain, ![X1:int, X2:int]:((ftimes_times_int @ (fbit0 @ X1) @ X2)=(fbit0 @ (ftimes_times_int @ X1 @ X2))|~p59), inference(split_conjunct,[status(thm)],[c_0_27])).
% 8.26/8.42 thf(c_0_36, plain, p59, inference(split_conjunct,[status(thm)],[ax199])).
% 8.26/8.42 thf(c_0_37, plain, ![X1:int]:((ftimes_times_int @ fone_one_int @ X1)=(X1)|~p62), inference(split_conjunct,[status(thm)],[c_0_28])).
% 8.26/8.42 thf(c_0_38, plain, p62, inference(split_conjunct,[status(thm)],[ax196])).
% 8.26/8.42 thf(c_0_39, plain, (~p117|(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), inference(fof_nnf,[status(thm)],[pax117])).
% 8.26/8.42 thf(c_0_40, plain, (~p248|(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax248])).
% 8.26/8.42 thf(c_0_41, plain, ![X2:int, X1:int]:((fplus_plus_int @ X1 @ X2)=(fplus_plus_int @ X2 @ X1)|~p93), inference(split_conjunct,[status(thm)],[c_0_29])).
% 8.26/8.42 thf(c_0_42, plain, p93, inference(split_conjunct,[status(thm)],[ax165])).
% 8.26/8.42 thf(c_0_43, plain, ![X1:int]:((ftimes_times_int @ X1 @ X1)=(fpower_power_int @ X1 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))|~p209), inference(split_conjunct,[status(thm)],[c_0_30])).
% 8.26/8.42 thf(c_0_44, plain, p209, inference(split_conjunct,[status(thm)],[ax49])).
% 8.26/8.42 thf(c_0_45, plain, ((fpls)=(fzero_zero_int)|~p128), inference(split_conjunct,[status(thm)],[c_0_31])).
% 8.26/8.42 thf(c_0_46, plain, p128, inference(split_conjunct,[status(thm)],[ax130])).
% 8.26/8.42 thf(c_0_47, plain, (~p2|(fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)), inference(fof_nnf,[status(thm)],[pax2])).
% 8.26/8.42 thf(c_0_48, plain, ![X1:int]:((ftimes_times_int @ (fplus_plus_int @ fone_one_int @ fone_one_int) @ (fnumber_number_of_int @ X1))=(fnumber_number_of_int @ (fbit0 @ X1))|~p141), inference(split_conjunct,[status(thm)],[c_0_32])).
% 8.26/8.42 thf(c_0_49, plain, ![X1:int]:(fplus_plus_int @ X1 @ X1)=(fbit0 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 8.26/8.42 thf(c_0_50, plain, ![X1:int, X2:int]:(ftimes_times_int @ (fbit0 @ X1) @ X2)=(fbit0 @ (ftimes_times_int @ X1 @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 8.26/8.42 thf(c_0_51, plain, ![X1:int]:(ftimes_times_int @ fone_one_int @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 8.26/8.42 thf(c_0_52, plain, p141, inference(split_conjunct,[status(thm)],[ax117])).
% 8.26/8.42 thf(c_0_53, plain, ((fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))|~p117), inference(split_conjunct,[status(thm)],[c_0_39])).
% 8.26/8.42 thf(c_0_54, plain, p117, inference(split_conjunct,[status(thm)],[ax141])).
% 8.26/8.42 thf(c_0_55, plain, ((fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(fzero_zero_int)|~p248), inference(split_conjunct,[status(thm)],[c_0_40])).
% 8.26/8.42 thf(c_0_56, plain, ![X2:int, X1:int]:(fplus_plus_int @ X1 @ X2)=(fplus_plus_int @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 8.26/8.42 thf(c_0_57, plain, ![X1:int]:(ftimes_times_int @ X1 @ X1)=(fpower_power_int @ X1 @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 8.26/8.42 thf(c_0_58, plain, (fzero_zero_int)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46])])).
% 8.26/8.42 thf(c_0_59, plain, p248, inference(split_conjunct,[status(thm)],[ax255])).
% 8.26/8.42 thf(c_0_60, plain, ![X146:int]:(~p241|(ftimes_times_int @ X146 @ fzero_zero_int)=(fzero_zero_int)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax241])])])).
% 8.26/8.42 thf(c_0_61, plain, (~ford_less_int @ fpls @ fpls|p130), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax130])])).
% 8.26/8.42 thf(c_0_62, plain, ~p130, inference(fof_simplification,[status(thm)],[ax128])).
% 8.26/8.42 thf(c_0_63, plain, (~p1|ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax1])).
% 8.26/8.42 thf(c_0_64, plain, ((fplus_plus_int @ (fpower_power_int @ fs @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls)))) @ fone_one_int)=(ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft)|~p2), inference(split_conjunct,[status(thm)],[c_0_47])).
% 8.26/8.42 thf(c_0_65, plain, ![X1:int]:(fnumber_number_of_int @ (fbit0 @ X1))=(fbit0 @ (fnumber_number_of_int @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49]), c_0_50]), c_0_51]), c_0_52])])).
% 8.26/8.42 thf(c_0_66, plain, (fnumber_number_of_int @ (fbit1 @ fpls))=(fone_one_int), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 8.26/8.42 thf(c_0_67, plain, (fplus_plus_int @ fone_one_int @ (ftimes_times_int @ fs @ fs))=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 8.26/8.42 thf(c_0_68, plain, p2, inference(split_conjunct,[status(thm)],[ax256])).
% 8.26/8.42 thf(c_0_69, plain, ![X1:int]:((ftimes_times_int @ X1 @ fzero_zero_int)=(fzero_zero_int)|~p241), inference(split_conjunct,[status(thm)],[c_0_60])).
% 8.26/8.42 thf(c_0_70, plain, p241, inference(split_conjunct,[status(thm)],[ax17])).
% 8.26/8.42 thf(c_0_71, plain, (p130|~ford_less_int @ fpls @ fpls), inference(split_conjunct,[status(thm)],[c_0_61])).
% 8.26/8.42 thf(c_0_72, plain, ~p130, inference(split_conjunct,[status(thm)],[c_0_62])).
% 8.26/8.42 thf(c_0_73, plain, (ford_less_int @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ ft) @ (ftimes_times_int @ (fplus_plus_int @ (ftimes_times_int @ (fnumber_number_of_int @ (fbit0 @ (fbit0 @ (fbit1 @ fpls)))) @ fm) @ fone_one_int) @ fzero_zero_int)|~p1), inference(split_conjunct,[status(thm)],[c_0_63])).
% 8.26/8.42 thf(c_0_74, plain, (ftimes_times_int @ (fplus_plus_int @ fone_one_int @ (fbit0 @ (fbit0 @ fm))) @ ft)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_56]), c_0_65]), c_0_65]), c_0_66]), c_0_50]), c_0_50]), c_0_51]), c_0_56]), c_0_57]), c_0_67]), c_0_68])])).
% 8.26/8.42 thf(c_0_75, plain, ![X1:int]:(ftimes_times_int @ X1 @ fpls)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_58]), c_0_58]), c_0_70])])).
% 8.26/8.42 thf(c_0_76, plain, p1, inference(split_conjunct,[status(thm)],[ax257])).
% 8.26/8.42 thf(c_0_77, plain, ~ford_less_int @ fpls @ fpls, inference(sr,[status(thm)],[c_0_71, c_0_72])).
% 8.26/8.42 thf(c_0_78, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_56]), c_0_65]), c_0_65]), c_0_66]), c_0_50]), c_0_50]), c_0_51]), c_0_74]), c_0_56]), c_0_65]), c_0_65]), c_0_66]), c_0_50]), c_0_50]), c_0_51]), c_0_58]), c_0_75]), c_0_76])]), c_0_77]), ['proof']).
% 8.26/8.42 thf(2,plain,$false,inference(eprover,[status(thm),assumptions([h20,h18,h16,h17,h14,h15,h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0])],[])).
% 8.26/8.42 thf(fact_4_calculation_I2_J,axiom,((t = zero_zero_int) => (((plus_plus_int @ ((power_power_int @ s) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ one_one_int) = zero_zero_int))).
% 8.26/8.42 thf(3,plain,$false,inference(tab_imp,[status(thm),assumptions([h18,h16,h17,h14,h15,h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_imp(discharge,[h19]),tab_imp(discharge,[h20])],[fact_4_calculation_I2_J,1,2,h19,h20])).
% 8.26/8.42 thf(fact_30__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,(~((![X1:int]:(~((((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)) @ X1)))))))).
% 8.26/8.42 thf(4,plain,$false,inference(tab_negall,[status(thm),assumptions([h16,h17,h14,h15,h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h18]),tab_negall(eigenvar,eigen__3)],[fact_30__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_,3,h18])).
% 8.26/8.42 thf(5,plain,$false,inference(tab_negimp,[status(thm),assumptions([h14,h15,h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h16,h17])],[h14,4,h16,h17])).
% 8.26/8.42 thf(fact_274_s0p,axiom,(~(((~((((ord_less_eq_int @ zero_zero_int) @ s) => (~(((ord_less_int @ s) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ s) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)))))))).
% 8.26/8.42 thf(6,plain,$false,inference(tab_negimp,[status(thm),assumptions([h12,h13,h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h14,h15])],[fact_274_s0p,5,h14,h15])).
% 8.26/8.42 thf(7,plain,$false,inference(tab_negimp,[status(thm),assumptions([h10,h11,h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h12,h13])],[h10,6,h12,h13])).
% 8.26/8.42 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h8,h9,h7,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h10,h11])],[h8,7,h10,h11])).
% 8.26/8.42 thf(9,plain,$false,inference(tab_negimp,[status(thm),assumptions([h7,h5,h6,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h8,h9])],[h7,8,h8,h9])).
% 8.26/8.42 thf(fact_287__096EX_B_As_O_A0_A_060_061_As_A_G_As_A_060_A4_A_K_Am_A_L_A1_A_G_A_091s1,axiom,(~((![X1:int]:((~(((~((((ord_less_eq_int @ zero_zero_int) @ X1) => (~(((ord_less_int @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((![X2:int]:((~(((~((((ord_less_eq_int @ zero_zero_int) @ X2) => (~(((ord_less_int @ X2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ X2) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (X2 = X1)))))))))).
% 8.26/8.42 thf(10,plain,$false,inference(tab_negall,[status(thm),assumptions([h5,h6,h3,h4,h2,h1,h0]),tab_negall(discharge,[h7]),tab_negall(eigenvar,eigen__2)],[fact_287__096EX_B_As_O_A0_A_060_061_As_A_G_As_A_060_A4_A_K_Am_A_L_A1_A_G_A_091s1,9,h7])).
% 8.26/8.42 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h2,h1,h0]),tab_negimp(discharge,[h5,h6])],[h3,10,h5,h6])).
% 8.26/8.42 thf(12,plain,$false,inference(tab_negimp,[status(thm),assumptions([h2,h1,h0]),tab_negimp(discharge,[h3,h4])],[h2,11,h3,h4])).
% 8.26/8.42 thf(fact_288__096_B_Bthesis_O_A_I_B_Bs_O_A0_A_060_061_As_A_G_As_A_060_A4_A_K_Am_A_L_,axiom,(~((![X1:int]:((~((((ord_less_eq_int @ zero_zero_int) @ X1) => (~(((ord_less_int @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))) => (~((((zcong @ s1) @ X1) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int))))))))).
% 8.26/8.42 thf(13,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[fact_288__096_B_Bthesis_O_A_I_B_Bs_O_A0_A_060_061_As_A_G_As_A_060_A4_A_K_Am_A_L_,12,h2])).
% 8.26/8.42 thf(fact_455__096_B_Bthesis_O_A_I_B_Bs1_O_A_091s1_A_094_A2_A_061_A_N1_093_A_Imod_A4_,axiom,(~((![X1:int]:(~((((zcong @ ((power_power_int @ X1) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ (number_number_of_int @ min)) @ ((plus_plus_int @ ((times_times_int @ (number_number_of_int @ (bit0 @ (bit0 @ (bit1 @ pls))))) @ m)) @ one_one_int)))))))).
% 8.26/8.42 thf(14,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[fact_455__096_B_Bthesis_O_A_I_B_Bs1_O_A_091s1_A_094_A2_A_061_A_N1_093_A_Imod_A4_,13,h1])).
% 8.26/8.42 thf(0,theorem,((ord_less_int @ ((plus_plus_int @ ((power_power_int @ s) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls))))) @ one_one_int)) @ zero_zero_int),inference(contra,[status(thm),contra(discharge,[h0])],[14,h0])).
% 8.26/8.42 % SZS output end Proof
%------------------------------------------------------------------------------