%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM925^2 : 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 : n014.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:27 PM UTC 2025
% Result : Theorem 10.17s 10.29s
% Output : Proof 10.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUM925^2 : TPTP v9.2.0. Released v5.3.0.
% 0.08/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n014.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 22:13:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 10.17/10.29 % SZS status Theorem
% 10.17/10.29 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 10.17/10.29 % Inferences: 2
% 10.17/10.29 % SZS output start Proof
% 10.17/10.29 thf(conj_0,conjecture,(~((((power_power_int @ ((plus_plus_int @ one_one_int) @ (semiri1621563631at_int @ n))) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) = zero_zero_int)))).
% 10.17/10.29 thf(h0,negated_conjecture,(((power_power_int @ ((plus_plus_int @ one_one_int) @ (semiri1621563631at_int @ n))) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) = zero_zero_int),inference(assume_negation,[status(cth)],[conj_0])).
% 10.17/10.29 thf(ax6, axiom, (~(p291)|p292), file('<stdin>', ax6)).
% 10.17/10.29 thf(pax52, axiom, (p52=>![X81:int, X69:int]:(fplus_plus_int @ X81 @ X69)=(fplus_plus_int @ X69 @ X81)), file('<stdin>', pax52)).
% 10.17/10.29 thf(pax81, axiom, (p81=>(fpls)=(fzero_zero_int)), file('<stdin>', pax81)).
% 10.17/10.29 thf(ax5, axiom, (~(p292)|p293), file('<stdin>', ax5)).
% 10.17/10.29 thf(ax7, axiom, p291, file('<stdin>', ax7)).
% 10.17/10.29 thf(pax86, axiom, (p86=>![X79:int]:(fbit0 @ X79)=(fplus_plus_int @ X79 @ X79)), file('<stdin>', pax86)).
% 10.17/10.29 thf(pax104, axiom, (p104=>![X73:int]:(fbit1 @ X73)=(fplus_plus_int @ (fplus_plus_int @ fone_one_int @ X73) @ X73)), file('<stdin>', pax104)).
% 10.17/10.29 thf(ax245, axiom, p52, file('<stdin>', ax245)).
% 10.17/10.29 thf(pax87, axiom, (p87=>![X79:int]:(fplus_plus_int @ X79 @ fzero_zero_int)=(X79)), file('<stdin>', pax87)).
% 10.17/10.29 thf(ax216, axiom, p81, file('<stdin>', ax216)).
% 10.17/10.29 thf(pax88, axiom, (p88=>![X79:int]:(fplus_plus_int @ fzero_zero_int @ X79)=(X79)), file('<stdin>', pax88)).
% 10.17/10.29 thf(ax4, axiom, (~(p293)|~(p289)|p290), file('<stdin>', ax4)).
% 10.17/10.29 thf(pax138, axiom, (p138=>![X57:nat, X59:int]:(~((X59)=(fzero_zero_int))=>~((fpower_power_int @ X59 @ X57)=(fzero_zero_int)))), file('<stdin>', pax138)).
% 10.17/10.29 thf(pax290, axiom, (p290=>(fzero_zero_int)=(fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), file('<stdin>', pax290)).
% 10.17/10.29 thf(ax211, axiom, p86, file('<stdin>', ax211)).
% 10.17/10.29 thf(ax193, axiom, p104, file('<stdin>', ax193)).
% 10.17/10.29 thf(ax210, axiom, p87, file('<stdin>', ax210)).
% 10.17/10.29 thf(ax209, axiom, p88, file('<stdin>', ax209)).
% 10.17/10.29 thf(ax8, axiom, p289, file('<stdin>', ax8)).
% 10.17/10.29 thf(pax1, axiom, (p1=>ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), file('<stdin>', pax1)).
% 10.17/10.29 thf(ax159, axiom, p138, file('<stdin>', ax159)).
% 10.17/10.29 thf(nax40, axiom, (p40<=ford_less_int @ fpls @ fpls), file('<stdin>', nax40)).
% 10.17/10.29 thf(ax257, axiom, ~(p40), file('<stdin>', ax257)).
% 10.17/10.29 thf(ax296, axiom, p1, file('<stdin>', ax296)).
% 10.17/10.29 thf(c_0_24, plain, (~p291|p292), inference(fof_simplification,[status(thm)],[ax6])).
% 10.17/10.29 thf(c_0_25, plain, ![X584:int, X585:int]:(~p52|(fplus_plus_int @ X584 @ X585)=(fplus_plus_int @ X585 @ X584)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax52])])])).
% 10.17/10.29 thf(c_0_26, plain, (~p81|(fpls)=(fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax81])).
% 10.17/10.29 thf(c_0_27, plain, (~p292|p293), inference(fof_simplification,[status(thm)],[ax5])).
% 10.17/10.29 thf(c_0_28, plain, (p292|~p291), inference(split_conjunct,[status(thm)],[c_0_24])).
% 10.17/10.29 thf(c_0_29, plain, p291, inference(split_conjunct,[status(thm)],[ax7])).
% 10.17/10.29 thf(c_0_30, plain, ![X560:int]:(~p86|(fbit0 @ X560)=(fplus_plus_int @ X560 @ X560)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax86])])])).
% 10.17/10.29 thf(c_0_31, plain, ![X518:int]:(~p104|(fbit1 @ X518)=(fplus_plus_int @ (fplus_plus_int @ fone_one_int @ X518) @ X518)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax104])])])).
% 10.17/10.29 thf(c_0_32, plain, ![X2:int, X1:int]:((fplus_plus_int @ X1 @ X2)=(fplus_plus_int @ X2 @ X1)|~p52), inference(split_conjunct,[status(thm)],[c_0_25])).
% 10.17/10.29 thf(c_0_33, plain, p52, inference(split_conjunct,[status(thm)],[ax245])).
% 10.17/10.29 thf(c_0_34, plain, ![X558:int]:(~p87|(fplus_plus_int @ X558 @ fzero_zero_int)=(X558)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax87])])])).
% 10.17/10.29 thf(c_0_35, plain, ((fpls)=(fzero_zero_int)|~p81), inference(split_conjunct,[status(thm)],[c_0_26])).
% 10.17/10.29 thf(c_0_36, plain, p81, inference(split_conjunct,[status(thm)],[ax216])).
% 10.17/10.29 thf(c_0_37, plain, ![X556:int]:(~p88|(fplus_plus_int @ fzero_zero_int @ X556)=(X556)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax88])])])).
% 10.17/10.29 thf(c_0_38, plain, (~p293|~p289|p290), inference(fof_simplification,[status(thm)],[ax4])).
% 10.17/10.29 thf(c_0_39, plain, (p293|~p292), inference(split_conjunct,[status(thm)],[c_0_27])).
% 10.17/10.29 thf(c_0_40, plain, p292, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 10.17/10.29 thf(c_0_41, plain, ![X468:nat, X469:int]:(~p138|((X469)=(fzero_zero_int)|(fpower_power_int @ X469 @ X468)!=(fzero_zero_int))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax138])])])])).
% 10.17/10.29 thf(c_0_42, plain, (~p290|(fzero_zero_int)=(fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), inference(fof_nnf,[status(thm)],[pax290])).
% 10.17/10.29 thf(c_0_43, plain, ![X1:int]:((fbit0 @ X1)=(fplus_plus_int @ X1 @ X1)|~p86), inference(split_conjunct,[status(thm)],[c_0_30])).
% 10.17/10.29 thf(c_0_44, plain, p86, inference(split_conjunct,[status(thm)],[ax211])).
% 10.17/10.29 thf(c_0_45, plain, ![X1:int]:((fbit1 @ X1)=(fplus_plus_int @ (fplus_plus_int @ fone_one_int @ X1) @ X1)|~p104), inference(split_conjunct,[status(thm)],[c_0_31])).
% 10.17/10.29 thf(c_0_46, 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_32, c_0_33])])).
% 10.17/10.29 thf(c_0_47, plain, p104, inference(split_conjunct,[status(thm)],[ax193])).
% 10.17/10.29 thf(c_0_48, plain, ![X1:int]:((fplus_plus_int @ X1 @ fzero_zero_int)=(X1)|~p87), inference(split_conjunct,[status(thm)],[c_0_34])).
% 10.17/10.29 thf(c_0_49, plain, (fzero_zero_int)=(fpls), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 10.17/10.29 thf(c_0_50, plain, p87, inference(split_conjunct,[status(thm)],[ax210])).
% 10.17/10.29 thf(c_0_51, plain, ![X1:int]:((fplus_plus_int @ fzero_zero_int @ X1)=(X1)|~p88), inference(split_conjunct,[status(thm)],[c_0_37])).
% 10.17/10.29 thf(c_0_52, plain, p88, inference(split_conjunct,[status(thm)],[ax209])).
% 10.17/10.29 thf(c_0_53, plain, (p290|~p293|~p289), inference(split_conjunct,[status(thm)],[c_0_38])).
% 10.17/10.29 thf(c_0_54, plain, p289, inference(split_conjunct,[status(thm)],[ax8])).
% 10.17/10.29 thf(c_0_55, plain, p293, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 10.17/10.29 thf(c_0_56, plain, (~p1|ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), inference(fof_nnf,[status(thm)],[pax1])).
% 10.17/10.29 thf(c_0_57, plain, ![X1:int, X5:nat]:((X1)=(fzero_zero_int)|~p138|(fpower_power_int @ X1 @ X5)!=(fzero_zero_int)), inference(split_conjunct,[status(thm)],[c_0_41])).
% 10.17/10.29 thf(c_0_58, plain, p138, inference(split_conjunct,[status(thm)],[ax159])).
% 10.17/10.29 thf(c_0_59, plain, ((fzero_zero_int)=(fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))|~p290), inference(split_conjunct,[status(thm)],[c_0_42])).
% 10.17/10.29 thf(c_0_60, plain, ![X1:int]:(fbit0 @ X1)=(fplus_plus_int @ X1 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 10.17/10.29 thf(c_0_61, plain, ![X1:int]:(fbit1 @ X1)=(fplus_plus_int @ X1 @ (fplus_plus_int @ fone_one_int @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_47])])).
% 10.17/10.29 thf(c_0_62, plain, ![X1:int]:(fplus_plus_int @ X1 @ fpls)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49]), c_0_50])])).
% 10.17/10.29 thf(c_0_63, plain, ![X1:int]:(fplus_plus_int @ fpls @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_49]), c_0_52])])).
% 10.17/10.29 thf(c_0_64, plain, p290, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54]), c_0_55])])).
% 10.17/10.29 thf(c_0_65, plain, (~ford_less_int @ fpls @ fpls|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 10.17/10.29 thf(c_0_66, plain, ~p40, inference(fof_simplification,[status(thm)],[ax257])).
% 10.17/10.29 thf(c_0_67, plain, (ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))|~p1), inference(split_conjunct,[status(thm)],[c_0_56])).
% 10.17/10.29 thf(c_0_68, plain, p1, inference(split_conjunct,[status(thm)],[ax296])).
% 10.17/10.29 thf(c_0_69, plain, ![X1:int, X5:nat]:((X1)=(fpls)|(fpower_power_int @ X1 @ X5)!=(fpls)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_49]), c_0_49]), c_0_58])])).
% 10.17/10.29 thf(c_0_70, plain, (fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fplus_plus_int @ fone_one_int @ fone_one_int)))=(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)],[c_0_59, c_0_60]), c_0_61]), c_0_62]), c_0_63]), c_0_61]), c_0_62]), c_0_63]), c_0_49]), c_0_64])])).
% 10.17/10.29 thf(c_0_71, plain, (p40|~ford_less_int @ fpls @ fpls), inference(split_conjunct,[status(thm)],[c_0_65])).
% 10.17/10.29 thf(c_0_72, plain, ~p40, inference(split_conjunct,[status(thm)],[c_0_66])).
% 10.17/10.29 thf(c_0_73, plain, ford_less_int @ fpls @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_49]), c_0_68])])).
% 10.17/10.29 thf(c_0_74, plain, (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))=(fpls), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 10.17/10.29 thf(c_0_75, plain, ~ford_less_int @ fpls @ fpls, inference(sr,[status(thm)],[c_0_71, c_0_72])).
% 10.17/10.29 thf(c_0_76, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74]), c_0_75]), ['proof']).
% 10.17/10.29 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 10.17/10.29 thf(0,theorem,(~((((power_power_int @ ((plus_plus_int @ one_one_int) @ (semiri1621563631at_int @ n))) @ (number_number_of_nat @ (bit0 @ (bit1 @ pls)))) = zero_zero_int))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 10.17/10.29 % SZS output end Proof
%------------------------------------------------------------------------------