%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP220^3 : TPTP v9.2.1. Bugfixed v9.2.1.
% 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 : Tue Oct 14 12:39:44 PM UTC 2025
% Result : Theorem 23.73s 24.16s
% Output : Proof 23.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP220^3 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n014.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Fri Oct 10 14:05:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 23.73/24.16 % SZS status Theorem
% 23.73/24.16 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 23.73/24.16 % Inferences: 0
% 23.73/24.16 % SZS output start Proof
% 23.73/24.16 thf(conj_0,conjecture,(~(((vEBT_VEBT_membermima @ (vEBT_vebt_buildup @ ((divide_divide_nat @ (suc @ (suc @ va))) @ (numeral_numeral_nat @ (bit0 @ one))))) @ y)))).
% 23.73/24.16 thf(h0,negated_conjecture,((vEBT_VEBT_membermima @ (vEBT_vebt_buildup @ ((divide_divide_nat @ (suc @ (suc @ va))) @ (numeral_numeral_nat @ (bit0 @ one))))) @ y),inference(assume_negation,[status(cth)],[conj_0])).
% 23.73/24.16 thf(pax848, axiom, (p848=>(fsuc)=(fplus_plus_nat @ fone_one_nat)), file('<stdin>', pax848)).
% 23.73/24.16 thf(pax738, axiom, (p738=>![X1042:nat]:(fplus_plus_nat @ X1042 @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fsuc @ X1042))), file('<stdin>', pax738)).
% 23.73/24.16 thf(ax839, axiom, p848, file('<stdin>', ax839)).
% 23.73/24.16 thf(pax2, axiom, (p2=>fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))), file('<stdin>', pax2)).
% 23.73/24.16 thf(ax949, axiom, p738, file('<stdin>', ax949)).
% 23.73/24.16 thf(pax3, axiom, (p3=>![X1811:nat, X1803:nat]:(fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))=>((X1811)=(fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=>~(fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ X1811) @ X1803)))), file('<stdin>', pax3)).
% 23.73/24.16 thf(ax1685, axiom, p2, file('<stdin>', ax1685)).
% 23.73/24.16 thf(pax6, axiom, (p6=>![X1811:nat]:(fdivide_divide_nat @ (fsuc @ (fsuc @ X1811)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fdivide_divide_nat @ X1811 @ (fnumeral_numeral_nat @ (fbit0 @ fone))))), file('<stdin>', pax6)).
% 23.73/24.16 thf(ax1684, axiom, p3, file('<stdin>', ax1684)).
% 23.73/24.16 thf(ax1681, axiom, p6, file('<stdin>', ax1681)).
% 23.73/24.16 thf(pax1, axiom, (p1=>fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ (fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))) @ fy), file('<stdin>', pax1)).
% 23.73/24.16 thf(ax1686, axiom, p1, file('<stdin>', ax1686)).
% 23.73/24.16 thf(c_0_12, plain, (~p848|(fsuc)=(fplus_plus_nat @ fone_one_nat)), inference(fof_nnf,[status(thm)],[pax848])).
% 23.73/24.16 thf(c_0_13, plain, ![X4506:nat]:(~p738|(fplus_plus_nat @ X4506 @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fsuc @ X4506))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax738])])])).
% 23.73/24.16 thf(c_0_14, plain, ((fsuc)=(fplus_plus_nat @ fone_one_nat)|~p848), inference(split_conjunct,[status(thm)],[c_0_12])).
% 23.73/24.16 thf(c_0_15, plain, p848, inference(split_conjunct,[status(thm)],[ax839])).
% 23.73/24.16 thf(c_0_16, plain, (~p2|fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))), inference(fof_nnf,[status(thm)],[pax2])).
% 23.73/24.16 thf(c_0_17, plain, ![X2:nat]:((fplus_plus_nat @ X2 @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fsuc @ X2))|~p738), inference(split_conjunct,[status(thm)],[c_0_13])).
% 23.73/24.16 thf(c_0_18, plain, (fsuc)=(fplus_plus_nat @ fone_one_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 23.73/24.16 thf(c_0_19, plain, p738, inference(split_conjunct,[status(thm)],[ax949])).
% 23.73/24.16 thf(c_0_20, plain, ![X6330:nat, X6331:nat]:(~p3|(~fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))|((X6330)!=(fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))|~fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ X6330) @ X6331))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax3])])])])).
% 23.73/24.16 thf(c_0_21, plain, (fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))|~p2), inference(split_conjunct,[status(thm)],[c_0_16])).
% 23.73/24.16 thf(c_0_22, plain, ![X2:nat]:(fplus_plus_nat @ fone_one_nat @ (fplus_plus_nat @ fone_one_nat @ X2))=(fplus_plus_nat @ X2 @ (fnumeral_numeral_nat @ (fbit0 @ fone))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18]), c_0_18]), c_0_19])])).
% 23.73/24.16 thf(c_0_23, plain, p2, inference(split_conjunct,[status(thm)],[ax1685])).
% 23.73/24.16 thf(c_0_24, plain, ![X6320:nat]:(~p6|(fdivide_divide_nat @ (fsuc @ (fsuc @ X6320)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fdivide_divide_nat @ X6320 @ (fnumeral_numeral_nat @ (fbit0 @ fone))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 23.73/24.16 thf(c_0_25, plain, ![X2:nat, X4:nat]:(~p3|~fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fsuc @ (fsuc @ fva))|(X2)!=(fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))|~fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ X2) @ X4), inference(split_conjunct,[status(thm)],[c_0_20])).
% 23.73/24.16 thf(c_0_26, plain, p3, inference(split_conjunct,[status(thm)],[ax1684])).
% 23.73/24.16 thf(c_0_27, plain, fdvd_dvd_nat @ (fnumeral_numeral_nat @ (fbit0 @ fone)) @ (fplus_plus_nat @ fva @ (fnumeral_numeral_nat @ (fbit0 @ fone))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_18]), c_0_18]), c_0_22]), c_0_23])])).
% 23.73/24.16 thf(c_0_28, plain, ![X2:nat]:((fdivide_divide_nat @ (fsuc @ (fsuc @ X2)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fsuc @ (fdivide_divide_nat @ X2 @ (fnumeral_numeral_nat @ (fbit0 @ fone))))|~p6), inference(split_conjunct,[status(thm)],[c_0_24])).
% 23.73/24.16 thf(c_0_29, plain, p6, inference(split_conjunct,[status(thm)],[ax1681])).
% 23.73/24.16 thf(c_0_30, plain, (~p1|fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ (fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))) @ fy), inference(fof_nnf,[status(thm)],[pax1])).
% 23.73/24.16 thf(c_0_31, plain, ![X2:nat]:~fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ (fdivide_divide_nat @ (fplus_plus_nat @ fva @ (fnumeral_numeral_nat @ (fbit0 @ fone))) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))) @ X2, inference(er,[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)],[c_0_25, c_0_18]), c_0_18]), c_0_22]), c_0_26]), c_0_18]), c_0_18]), c_0_22]), c_0_27])])])).
% 23.73/24.16 thf(c_0_32, plain, ![X2:nat]:(fdivide_divide_nat @ (fplus_plus_nat @ X2 @ (fnumeral_numeral_nat @ (fbit0 @ fone))) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))=(fplus_plus_nat @ fone_one_nat @ (fdivide_divide_nat @ X2 @ (fnumeral_numeral_nat @ (fbit0 @ fone)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_18]), c_0_18]), c_0_22]), c_0_18]), c_0_29])])).
% 23.73/24.16 thf(c_0_33, plain, (fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ (fdivide_divide_nat @ (fsuc @ (fsuc @ fva)) @ (fnumeral_numeral_nat @ (fbit0 @ fone)))) @ fy|~p1), inference(split_conjunct,[status(thm)],[c_0_30])).
% 23.73/24.16 thf(c_0_34, plain, p1, inference(split_conjunct,[status(thm)],[ax1686])).
% 23.73/24.16 thf(c_0_35, plain, ![X2:nat]:~fvEBT_VEBT_membermima @ (fvEBT_vebt_buildup @ (fplus_plus_nat @ fone_one_nat @ (fdivide_divide_nat @ fva @ (fnumeral_numeral_nat @ (fbit0 @ fone))))) @ X2, inference(rw,[status(thm)],[c_0_31, c_0_32])).
% 23.73/24.16 thf(c_0_36, 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)],[c_0_33, c_0_18]), c_0_18]), c_0_22]), c_0_32]), c_0_34])]), c_0_35]), ['proof']).
% 23.73/24.16 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.73/24.16 thf(0,theorem,(~(((vEBT_VEBT_membermima @ (vEBT_vebt_buildup @ ((divide_divide_nat @ (suc @ (suc @ va))) @ (numeral_numeral_nat @ (bit0 @ one))))) @ y))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.73/24.16 % SZS output end Proof
%------------------------------------------------------------------------------