%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM925^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 : n016.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 23.69s 23.82s
% Output : Proof 23.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM925^3 : TPTP v9.2.0. Released v5.3.0.
% 0.06/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n016.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:57:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 23.69/23.82 % SZS status Theorem
% 23.69/23.82 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 23.69/23.82 % Inferences: 1748
% 23.69/23.82 % SZS output start Proof
% 23.69/23.82 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)))).
% 23.69/23.82 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])).
% 23.69/23.82 thf(ax1992, axiom, (~(p944)|p945), file('<stdin>', ax1992)).
% 23.69/23.82 thf(pax92, axiom, (p92=>(fpls)=(fzero_zero_int)), file('<stdin>', pax92)).
% 23.69/23.82 thf(pax155, axiom, (p155=>![X709:int]:(fnumber_number_of_int @ X709)=(X709)), file('<stdin>', pax155)).
% 23.69/23.82 thf(ax1991, axiom, (~(p945)|p946), file('<stdin>', ax1991)).
% 23.69/23.82 thf(ax1993, axiom, p944, file('<stdin>', ax1993)).
% 23.69/23.82 thf(pax25, axiom, (p25=>(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), file('<stdin>', pax25)).
% 23.69/23.82 thf(ax2844, axiom, p92, file('<stdin>', ax2844)).
% 23.69/23.82 thf(ax2781, axiom, p155, file('<stdin>', ax2781)).
% 23.69/23.82 thf(pax97, axiom, (p97=>![X732:int]:(fbit0 @ X732)=(fplus_plus_int @ X732 @ X732)), file('<stdin>', pax97)).
% 23.69/23.82 thf(ax1990, axiom, (~(p946)|~(p1)|p943), file('<stdin>', ax1990)).
% 23.69/23.82 thf(pax197, axiom, (p197=>![X692:nat, X695:int]:(~((X695)=(fzero_zero_int))=>~((fpower_power_int @ X695 @ X692)=(fzero_zero_int)))), file('<stdin>', pax197)).
% 23.69/23.82 thf(pax943, axiom, (p943=>(fzero_zero_int)=(fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))), file('<stdin>', pax943)).
% 23.69/23.82 thf(ax2911, axiom, p25, file('<stdin>', ax2911)).
% 23.69/23.82 thf(ax2839, axiom, p97, file('<stdin>', ax2839)).
% 23.69/23.82 thf(ax2935, axiom, p1, file('<stdin>', ax2935)).
% 23.69/23.82 thf(pax2, axiom, (p2=>ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), file('<stdin>', pax2)).
% 23.69/23.82 thf(nax45, axiom, (p45<=ford_less_int @ fpls @ fpls), file('<stdin>', nax45)).
% 23.69/23.82 thf(ax2891, axiom, ~(p45), file('<stdin>', ax2891)).
% 23.69/23.82 thf(ax2739, axiom, p197, file('<stdin>', ax2739)).
% 23.69/23.82 thf(ax2934, axiom, p2, file('<stdin>', ax2934)).
% 23.69/23.82 thf(pax1026, axiom, (p1026=>(fzero_zero_int)=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), file('<stdin>', pax1026)).
% 23.69/23.82 thf(nax1026, axiom, (p1026<=(fzero_zero_int)=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), file('<stdin>', nax1026)).
% 23.69/23.82 thf(c_0_22, plain, (~p944|p945), inference(fof_simplification,[status(thm)],[ax1992])).
% 23.69/23.82 thf(c_0_23, plain, (~p92|(fpls)=(fzero_zero_int)), inference(fof_nnf,[status(thm)],[pax92])).
% 23.69/23.82 thf(c_0_24, plain, ![X3319:int]:(~p155|(fnumber_number_of_int @ X3319)=(X3319)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax155])])])).
% 23.69/23.82 thf(c_0_25, plain, (~p945|p946), inference(fof_simplification,[status(thm)],[ax1991])).
% 23.69/23.82 thf(c_0_26, plain, (p945|~p944), inference(split_conjunct,[status(thm)],[c_0_22])).
% 23.69/23.82 thf(c_0_27, plain, p944, inference(split_conjunct,[status(thm)],[ax1993])).
% 23.69/23.82 thf(c_0_28, plain, (~p25|(fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))), inference(fof_nnf,[status(thm)],[pax25])).
% 23.69/23.82 thf(c_0_29, plain, ((fpls)=(fzero_zero_int)|~p92), inference(split_conjunct,[status(thm)],[c_0_23])).
% 23.69/23.82 thf(c_0_30, plain, p92, inference(split_conjunct,[status(thm)],[ax2844])).
% 23.69/23.82 thf(c_0_31, plain, ![X1:int]:((fnumber_number_of_int @ X1)=(X1)|~p155), inference(split_conjunct,[status(thm)],[c_0_24])).
% 23.69/23.82 thf(c_0_32, plain, p155, inference(split_conjunct,[status(thm)],[ax2781])).
% 23.69/23.82 thf(c_0_33, plain, ![X3441:int]:(~p97|(fbit0 @ X3441)=(fplus_plus_int @ X3441 @ X3441)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax97])])])).
% 23.69/23.82 thf(c_0_34, plain, (~p946|~p1|p943), inference(fof_simplification,[status(thm)],[ax1990])).
% 23.69/23.82 thf(c_0_35, plain, (p946|~p945), inference(split_conjunct,[status(thm)],[c_0_25])).
% 23.69/23.82 thf(c_0_36, plain, p945, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 23.69/23.82 thf(c_0_37, plain, ![X3213:nat, X3214:int]:(~p197|((X3214)=(fzero_zero_int)|(fpower_power_int @ X3214 @ X3213)!=(fzero_zero_int))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax197])])])])).
% 23.69/23.82 thf(c_0_38, plain, (~p943|(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)],[pax943])).
% 23.69/23.82 thf(c_0_39, plain, ((fone_one_int)=(fnumber_number_of_int @ (fbit1 @ fpls))|~p25), inference(split_conjunct,[status(thm)],[c_0_28])).
% 23.69/23.82 thf(c_0_40, plain, (fpls)=(fzero_zero_int), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 23.69/23.82 thf(c_0_41, plain, ![X1:int]:(fnumber_number_of_int @ X1)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 23.69/23.82 thf(c_0_42, plain, p25, inference(split_conjunct,[status(thm)],[ax2911])).
% 23.69/23.82 thf(c_0_43, plain, ![X1:int]:((fbit0 @ X1)=(fplus_plus_int @ X1 @ X1)|~p97), inference(split_conjunct,[status(thm)],[c_0_33])).
% 23.69/23.82 thf(c_0_44, plain, p97, inference(split_conjunct,[status(thm)],[ax2839])).
% 23.69/23.82 thf(c_0_45, plain, (p943|~p946|~p1), inference(split_conjunct,[status(thm)],[c_0_34])).
% 23.69/23.82 thf(c_0_46, plain, p1, inference(split_conjunct,[status(thm)],[ax2935])).
% 23.69/23.82 thf(c_0_47, plain, p946, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 23.69/23.82 thf(c_0_48, plain, (~p2|ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), inference(fof_nnf,[status(thm)],[pax2])).
% 23.69/23.82 thf(c_0_49, plain, (~ford_less_int @ fpls @ fpls|p45), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax45])])).
% 23.69/23.82 thf(c_0_50, plain, ~p45, inference(fof_simplification,[status(thm)],[ax2891])).
% 23.69/23.82 thf(c_0_51, plain, ![X1:int, X2:nat]:((X1)=(fzero_zero_int)|~p197|(fpower_power_int @ X1 @ X2)!=(fzero_zero_int)), inference(split_conjunct,[status(thm)],[c_0_37])).
% 23.69/23.82 thf(c_0_52, plain, p197, inference(split_conjunct,[status(thm)],[ax2739])).
% 23.69/23.82 thf(c_0_53, plain, ((fzero_zero_int)=(fpower_power_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)) @ (fnumber_number_of_nat @ (fbit0 @ (fbit1 @ fpls))))|~p943), inference(split_conjunct,[status(thm)],[c_0_38])).
% 23.69/23.82 thf(c_0_54, plain, (fbit1 @ fzero_zero_int)=(fone_one_int), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40]), c_0_41]), c_0_42])])).
% 23.69/23.82 thf(c_0_55, plain, ![X1:int]:(fbit0 @ X1)=(fplus_plus_int @ X1 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 23.69/23.82 thf(c_0_56, plain, p943, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_47])])).
% 23.69/23.82 thf(c_0_57, plain, (ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))|~p2), inference(split_conjunct,[status(thm)],[c_0_48])).
% 23.69/23.82 thf(c_0_58, plain, p2, inference(split_conjunct,[status(thm)],[ax2934])).
% 23.69/23.82 thf(c_0_59, plain, (~p1026|(fzero_zero_int)=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), inference(fof_nnf,[status(thm)],[pax1026])).
% 23.69/23.82 thf(c_0_60, plain, (p45|~ford_less_int @ fpls @ fpls), inference(split_conjunct,[status(thm)],[c_0_49])).
% 23.69/23.82 thf(c_0_61, plain, ~p45, inference(split_conjunct,[status(thm)],[c_0_50])).
% 23.69/23.82 thf(c_0_62, plain, ![X1:int, X2:nat]:((X1)=(fzero_zero_int)|(fpower_power_int @ X1 @ X2)!=(fzero_zero_int)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 23.69/23.82 thf(c_0_63, 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)))=(fzero_zero_int), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_40]), c_0_54]), c_0_55]), c_0_56])])).
% 23.69/23.82 thf(c_0_64, plain, ((fzero_zero_int)!=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))|p1026), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1026])])).
% 23.69/23.82 thf(c_0_65, plain, ford_less_int @ fzero_zero_int @ (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57, c_0_58])])).
% 23.69/23.82 thf(c_0_66, plain, ((fzero_zero_int)=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))|~p1026), inference(split_conjunct,[status(thm)],[c_0_59])).
% 23.69/23.82 thf(c_0_67, plain, ~ford_less_int @ fzero_zero_int @ fzero_zero_int, inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_40]), c_0_40]), c_0_61])).
% 23.69/23.82 thf(c_0_68, plain, (fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))=(fzero_zero_int), inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 23.69/23.82 thf(c_0_69, plain, (p1026|(fzero_zero_int)!=(fplus_plus_int @ fone_one_int @ (fsemiri1621563631at_int @ fn))), inference(split_conjunct,[status(thm)],[c_0_64])).
% 23.69/23.82 thf(c_0_70, plain, ~p1026, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_67])).
% 23.69/23.82 thf(c_0_71, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_68, c_0_69, c_0_70]), ['proof']).
% 23.69/23.82 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.69/23.82 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])).
% 23.69/23.82 % SZS output end Proof
%------------------------------------------------------------------------------