%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP130^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n023.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 01:47:03 PM UTC 2025
% Result : Theorem 121.28s 121.06s
% Output : Proof 121.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP130^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n023.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 18:19:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 121.28/121.06 % SZS status Theorem
% 121.28/121.06 % Mode: mode504:USE_SINE=true:SINE_TOLERANCE=2.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 121.28/121.06 % Inferences: 292
% 121.28/121.06 % SZS output start Proof
% 121.28/121.06 thf(ty_int, type, int : $tType).
% 121.28/121.06 thf(ty_zero_zero_int, type, zero_zero_int : int).
% 121.28/121.06 thf(ty_na, type, na : int).
% 121.28/121.06 thf(ty_ya, type, ya : int).
% 121.28/121.06 thf(ty_ord_less_int, type, ord_less_int : (int>int>$o)).
% 121.28/121.06 thf(sP1,plain,sP1 <=> (ya = zero_zero_int),introduced(definition,[new_symbols(definition,[sP1])])).
% 121.28/121.06 thf(conj_0,conjecture,((ord_less_real @ (ring_1_of_int_real @ na)) @ ((power_power_real @ (ring_1_of_int_real @ ya)) @ (suc @ pm)))).
% 121.28/121.06 thf(h0,negated_conjecture,(~(((ord_less_real @ (ring_1_of_int_real @ na)) @ ((power_power_real @ (ring_1_of_int_real @ ya)) @ (suc @ pm))))),inference(assume_negation,[status(cth)],[conj_0])).
% 121.28/121.06 thf(h1,assumption,(~(((ord_less_int @ ya) @ zero_zero_int))),introduced(assumption,[])).
% 121.28/121.06 thf(h2,assumption,(~(((ord_less_int @ na) @ zero_zero_int))),introduced(assumption,[])).
% 121.28/121.06 thf(h3,assumption,((ord_less_int @ zero_zero_int) @ ya),introduced(assumption,[])).
% 121.28/121.06 thf(h4,assumption,sP1,introduced(assumption,[])).
% 121.28/121.06 thf(pax60, axiom, (p60=>(fp)=(fsuc @ fpm)), file('<stdin>', pax60)).
% 121.28/121.06 thf(ax517, axiom, (~(p4)|p604), file('<stdin>', ax517)).
% 121.28/121.06 thf(pax7, axiom, (p7=>![X276:int, X277:int]:(ford_less_real @ (fring_1_of_int_real @ X276) @ (fring_1_of_int_real @ X277)<=>ford_less_int @ X276 @ X277)), file('<stdin>', pax7)).
% 121.28/121.06 thf(pax56, axiom, (p56=>ford_less_int @ fna @ (fpower_power_int @ fya @ fp)), file('<stdin>', pax56)).
% 121.28/121.06 thf(ax1092, axiom, p60, file('<stdin>', ax1092)).
% 121.28/121.06 thf(pax604, axiom, (p604=>![X95:nat]:(fring_1_of_int_real @ (fpower_power_int @ fya @ X95))=(fpower_power_real @ (fring_1_of_int_real @ fya) @ X95)), file('<stdin>', pax604)).
% 121.28/121.06 thf(ax1148, axiom, p4, file('<stdin>', ax1148)).
% 121.28/121.06 thf(nax147, axiom, (p147<=ford_less_real @ (fring_1_of_int_real @ fna) @ (fpower_power_real @ (fring_1_of_int_real @ fya) @ (fsuc @ fpm))), file('<stdin>', nax147)).
% 121.28/121.06 thf(ax1005, axiom, ~(p147), file('<stdin>', ax1005)).
% 121.28/121.06 thf(ax1145, axiom, p7, file('<stdin>', ax1145)).
% 121.28/121.06 thf(ax1096, axiom, p56, file('<stdin>', ax1096)).
% 121.28/121.06 thf(c_0_11, plain, (~p60|(fp)=(fsuc @ fpm)), inference(fof_nnf,[status(thm)],[pax60])).
% 121.28/121.06 thf(c_0_12, plain, (~p4|p604), inference(fof_simplification,[status(thm)],[ax517])).
% 121.28/121.06 thf(c_0_13, plain, ![X2431:int, X2432:int]:((~ford_less_real @ (fring_1_of_int_real @ X2431) @ (fring_1_of_int_real @ X2432)|ford_less_int @ X2431 @ X2432|~p7)&(~ford_less_int @ X2431 @ X2432|ford_less_real @ (fring_1_of_int_real @ X2431) @ (fring_1_of_int_real @ X2432)|~p7)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])])).
% 121.28/121.06 thf(c_0_14, plain, (~p56|ford_less_int @ fna @ (fpower_power_int @ fya @ fp)), inference(fof_nnf,[status(thm)],[pax56])).
% 121.28/121.06 thf(c_0_15, plain, ((fp)=(fsuc @ fpm)|~p60), inference(split_conjunct,[status(thm)],[c_0_11])).
% 121.28/121.06 thf(c_0_16, plain, p60, inference(split_conjunct,[status(thm)],[ax1092])).
% 121.28/121.06 thf(c_0_17, plain, ![X1008:nat]:(~p604|(fring_1_of_int_real @ (fpower_power_int @ fya @ X1008))=(fpower_power_real @ (fring_1_of_int_real @ fya) @ X1008)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax604])])])).
% 121.28/121.06 thf(c_0_18, plain, (p604|~p4), inference(split_conjunct,[status(thm)],[c_0_12])).
% 121.28/121.06 thf(c_0_19, plain, p4, inference(split_conjunct,[status(thm)],[ax1148])).
% 121.28/121.06 thf(c_0_20, plain, (~ford_less_real @ (fring_1_of_int_real @ fna) @ (fpower_power_real @ (fring_1_of_int_real @ fya) @ (fsuc @ fpm))|p147), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax147])])).
% 121.28/121.06 thf(c_0_21, plain, ~p147, inference(fof_simplification,[status(thm)],[ax1005])).
% 121.28/121.06 thf(c_0_22, plain, ![X13:int, X16:int]:(ford_less_real @ (fring_1_of_int_real @ X13) @ (fring_1_of_int_real @ X16)|~ford_less_int @ X13 @ X16|~p7), inference(split_conjunct,[status(thm)],[c_0_13])).
% 121.28/121.06 thf(c_0_23, plain, p7, inference(split_conjunct,[status(thm)],[ax1145])).
% 121.28/121.06 thf(c_0_24, plain, (ford_less_int @ fna @ (fpower_power_int @ fya @ fp)|~p56), inference(split_conjunct,[status(thm)],[c_0_14])).
% 121.28/121.06 thf(c_0_25, plain, (fp)=(fsuc @ fpm), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 121.28/121.06 thf(c_0_26, plain, p56, inference(split_conjunct,[status(thm)],[ax1096])).
% 121.28/121.06 thf(c_0_27, plain, ![X4:nat]:((fring_1_of_int_real @ (fpower_power_int @ fya @ X4))=(fpower_power_real @ (fring_1_of_int_real @ fya) @ X4)|~p604), inference(split_conjunct,[status(thm)],[c_0_17])).
% 121.28/121.06 thf(c_0_28, plain, p604, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 121.28/121.06 thf(c_0_29, plain, (p147|~ford_less_real @ (fring_1_of_int_real @ fna) @ (fpower_power_real @ (fring_1_of_int_real @ fya) @ (fsuc @ fpm))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 121.28/121.06 thf(c_0_30, plain, ~p147, inference(split_conjunct,[status(thm)],[c_0_21])).
% 121.28/121.06 thf(c_0_31, plain, ![X13:int, X16:int]:(ford_less_real @ (fring_1_of_int_real @ X13) @ (fring_1_of_int_real @ X16)|~ford_less_int @ X13 @ X16), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 121.28/121.06 thf(c_0_32, plain, ford_less_int @ fna @ (fpower_power_int @ fya @ (fsuc @ fpm)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25]), c_0_26])])).
% 121.28/121.06 thf(c_0_33, plain, ![X4:nat]:(fring_1_of_int_real @ (fpower_power_int @ fya @ X4))=(fpower_power_real @ (fring_1_of_int_real @ fya) @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 121.28/121.06 thf(c_0_34, plain, ~ford_less_real @ (fring_1_of_int_real @ fna) @ (fpower_power_real @ (fring_1_of_int_real @ fya) @ (fsuc @ fpm)), inference(sr,[status(thm)],[c_0_29, c_0_30])).
% 121.28/121.06 thf(c_0_35, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33]), c_0_34]), ['proof']).
% 121.28/121.06 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h3,h1,h2,h1,h2,h0])],[])).
% 121.28/121.06 thf(fact_19_y00,axiom,(~(sP1))).
% 121.28/121.06 thf(2,plain,$false,inference(tab_conflict,[status(thm),assumptions([h4,h1,h2,h1,h2,h0])],[h4,fact_19_y00])).
% 121.28/121.06 thf(fact_20__092_060open_0620_A_060_Ay_A_092_060or_062_Ay_A_061_A0_092_060close_062,axiom,((~(((ord_less_int @ zero_zero_int) @ ya))) => sP1)).
% 121.28/121.06 thf(3,plain,$false,inference(tab_imp,[status(thm),assumptions([h1,h2,h1,h2,h0]),tab_imp(discharge,[h3]),tab_imp(discharge,[h4])],[fact_20__092_060open_0620_A_060_Ay_A_092_060or_062_Ay_A_061_A0_092_060close_062,1,2,h3,h4])).
% 121.28/121.06 thf(fact_24_not_I1_J,axiom,(~(((~(((ord_less_int @ ya) @ zero_zero_int))) => ((ord_less_int @ na) @ zero_zero_int))))).
% 121.28/121.06 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h2,h0]),tab_negimp(discharge,[h1,h2])],[fact_24_not_I1_J,3,h1,h2])).
% 121.28/121.06 thf(5,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[fact_24_not_I1_J,4,h1,h2])).
% 121.28/121.06 thf(0,theorem,((ord_less_real @ (ring_1_of_int_real @ na)) @ ((power_power_real @ (ring_1_of_int_real @ ya)) @ (suc @ pm))),inference(contra,[status(thm),contra(discharge,[h0])],[5,h0])).
% 121.28/121.06 % SZS output end Proof
%------------------------------------------------------------------------------