%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM693^1 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n019.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:11:49 PM UTC 2025
% Result : Theorem 1.81s 2.00s
% Output : Proof 1.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUM693^1 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 22:04:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 1.81/2.00 % SZS status Theorem
% 1.81/2.00 % Mode: mode506
% 1.81/2.00 % Inferences: 4042
% 1.81/2.00 % SZS output start Proof
% 1.81/2.00 thf(satz24,conjecture,((~(((more @ x) @ n_1))) => (x = n_1))).
% 1.81/2.00 thf(h0,negated_conjecture,(~(((~(((more @ x) @ n_1))) => (x = n_1)))),inference(assume_negation,[status(cth)],[satz24])).
% 1.81/2.00 thf(nax1, axiom, (p1<=(~(fmore @ fx @ fn_1)=>(fx)=(fn_1))), file('<stdin>', nax1)).
% 1.81/2.00 thf(ax1264, axiom, ~(p1), file('<stdin>', ax1264)).
% 1.81/2.00 thf(nax24, axiom, (p24<=((fx)=(fn_1)=>~((fn_1)=(fn_1)))), file('<stdin>', nax24)).
% 1.81/2.00 thf(ax1241, axiom, (~(p3)|p23), file('<stdin>', ax1241)).
% 1.81/2.00 thf(ax1236, axiom, (~(p24)|~(p7)|~(p15)), file('<stdin>', ax1236)).
% 1.81/2.00 thf(ax1242, axiom, (~(p23)|p7|~(p22)), file('<stdin>', ax1242)).
% 1.81/2.00 thf(ax1262, axiom, p3, file('<stdin>', ax1262)).
% 1.81/2.00 thf(ax805, axiom, p15, file('<stdin>', ax805)).
% 1.81/2.00 thf(ax1195, axiom, (~(p20)|p65), file('<stdin>', ax1195)).
% 1.81/2.00 thf(ax1194, axiom, (~(p65)|p64), file('<stdin>', ax1194)).
% 1.81/2.00 thf(ax1250, axiom, p20, file('<stdin>', ax1250)).
% 1.81/2.00 thf(ax1193, axiom, (~(p64)|~(p51)|p63), file('<stdin>', ax1193)).
% 1.81/2.00 thf(ax1205, axiom, (p22|p51), file('<stdin>', ax1205)).
% 1.81/2.00 thf(ax1249, axiom, (~(p20)|p19), file('<stdin>', ax1249)).
% 1.81/2.00 thf(ax1189, axiom, (~(p3)|p66), file('<stdin>', ax1189)).
% 1.81/2.00 thf(ax1191, axiom, (~(p62)|~(p61)|p7), file('<stdin>', ax1191)).
% 1.81/2.00 thf(ax1192, axiom, (~(p63)|p62), file('<stdin>', ax1192)).
% 1.81/2.00 thf(ax1227, axiom, (~(p19)|p37), file('<stdin>', ax1227)).
% 1.81/2.00 thf(ax1190, axiom, (~(p66)|p61|~(p60)), file('<stdin>', ax1190)).
% 1.81/2.00 thf(ax1226, axiom, (~(p37)|p1|p36), file('<stdin>', ax1226)).
% 1.81/2.00 thf(pax35, axiom, (p35=>((fn_1)=(fn_1)=>~((~(fmore @ fx @ fn_1)=>(fx)=(fn_1))))), file('<stdin>', pax35)).
% 1.81/2.00 thf(ax1225, axiom, (~(p36)|p35), file('<stdin>', ax1225)).
% 1.81/2.00 thf(pax51, axiom, (p51=>(fx)=(fsuc @ f__0)), file('<stdin>', pax51)).
% 1.81/2.00 thf(pax133, axiom, (p133=>(fsuc @ f__0)=(fsuc @ f__2)), file('<stdin>', pax133)).
% 1.81/2.00 thf(ax1106, axiom, (p60|p133), file('<stdin>', ax1106)).
% 1.81/2.00 thf(pax4, axiom, (p4=>![X1:nat, X2:nat]:fmore @ (fpl @ X1 @ X2) @ X1), file('<stdin>', pax4)).
% 1.81/2.00 thf(pax5, axiom, (p5=>![X1:nat]:(fsuc @ X1)=(fpl @ fn_1 @ X1)), file('<stdin>', pax5)).
% 1.81/2.00 thf(ax1261, axiom, p4, file('<stdin>', ax1261)).
% 1.81/2.00 thf(ax1260, axiom, p5, file('<stdin>', ax1260)).
% 1.81/2.00 thf(c_0_29, plain, ((~fmore @ fx @ fn_1|p1)&((fx)!=(fn_1)|p1)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])])).
% 1.81/2.00 thf(c_0_30, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1264])).
% 1.81/2.00 thf(c_0_31, plain, (((fx)=(fn_1)|p24)&((fn_1)=(fn_1)|p24)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax24])])])).
% 1.81/2.00 thf(c_0_32, plain, (p1|(fx)!=(fn_1)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.81/2.00 thf(c_0_33, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_30])).
% 1.81/2.00 thf(c_0_34, plain, (~p3|p23), inference(fof_simplification,[status(thm)],[ax1241])).
% 1.81/2.00 thf(c_0_35, plain, (~p24|~p7|~p15), inference(fof_simplification,[status(thm)],[ax1236])).
% 1.81/2.00 thf(c_0_36, plain, ((fx)=(fn_1)|p24), inference(split_conjunct,[status(thm)],[c_0_31])).
% 1.81/2.00 thf(c_0_37, plain, (fx)!=(fn_1), inference(sr,[status(thm)],[c_0_32, c_0_33])).
% 1.81/2.00 thf(c_0_38, plain, (~p23|p7|~p22), inference(fof_simplification,[status(thm)],[ax1242])).
% 1.81/2.00 thf(c_0_39, plain, (p23|~p3), inference(split_conjunct,[status(thm)],[c_0_34])).
% 1.81/2.00 thf(c_0_40, plain, p3, inference(split_conjunct,[status(thm)],[ax1262])).
% 1.81/2.00 thf(c_0_41, plain, (~p24|~p7|~p15), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.81/2.00 thf(c_0_42, plain, p15, inference(split_conjunct,[status(thm)],[ax805])).
% 1.81/2.00 thf(c_0_43, plain, p24, inference(sr,[status(thm)],[c_0_36, c_0_37])).
% 1.81/2.00 thf(c_0_44, plain, (~p20|p65), inference(fof_simplification,[status(thm)],[ax1195])).
% 1.81/2.00 thf(c_0_45, plain, (p7|~p23|~p22), inference(split_conjunct,[status(thm)],[c_0_38])).
% 1.81/2.00 thf(c_0_46, plain, p23, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 1.81/2.00 thf(c_0_47, plain, ~p7, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42]), c_0_43])])).
% 1.81/2.00 thf(c_0_48, plain, (~p65|p64), inference(fof_simplification,[status(thm)],[ax1194])).
% 1.81/2.00 thf(c_0_49, plain, (p65|~p20), inference(split_conjunct,[status(thm)],[c_0_44])).
% 1.81/2.00 thf(c_0_50, plain, p20, inference(split_conjunct,[status(thm)],[ax1250])).
% 1.81/2.00 thf(c_0_51, plain, (~p64|~p51|p63), inference(fof_simplification,[status(thm)],[ax1193])).
% 1.81/2.00 thf(c_0_52, plain, (p22|p51), inference(split_conjunct,[status(thm)],[ax1205])).
% 1.81/2.00 thf(c_0_53, plain, ~p22, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46])]), c_0_47])).
% 1.81/2.00 thf(c_0_54, plain, (p64|~p65), inference(split_conjunct,[status(thm)],[c_0_48])).
% 1.81/2.00 thf(c_0_55, plain, p65, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 1.81/2.00 thf(c_0_56, plain, (~p20|p19), inference(fof_simplification,[status(thm)],[ax1249])).
% 1.81/2.00 thf(c_0_57, plain, (~p3|p66), inference(fof_simplification,[status(thm)],[ax1189])).
% 1.81/2.00 thf(c_0_58, plain, (~p62|~p61|p7), inference(fof_simplification,[status(thm)],[ax1191])).
% 1.81/2.00 thf(c_0_59, plain, (~p63|p62), inference(fof_simplification,[status(thm)],[ax1192])).
% 1.81/2.00 thf(c_0_60, plain, (p63|~p64|~p51), inference(split_conjunct,[status(thm)],[c_0_51])).
% 1.81/2.00 thf(c_0_61, plain, p51, inference(sr,[status(thm)],[c_0_52, c_0_53])).
% 1.81/2.00 thf(c_0_62, plain, p64, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 1.81/2.00 thf(c_0_63, plain, (~p19|p37), inference(fof_simplification,[status(thm)],[ax1227])).
% 1.81/2.00 thf(c_0_64, plain, (p19|~p20), inference(split_conjunct,[status(thm)],[c_0_56])).
% 1.81/2.00 thf(c_0_65, plain, (~p66|p61|~p60), inference(fof_simplification,[status(thm)],[ax1190])).
% 1.81/2.00 thf(c_0_66, plain, (p66|~p3), inference(split_conjunct,[status(thm)],[c_0_57])).
% 1.81/2.00 thf(c_0_67, plain, (p7|~p62|~p61), inference(split_conjunct,[status(thm)],[c_0_58])).
% 1.81/2.00 thf(c_0_68, plain, (p62|~p63), inference(split_conjunct,[status(thm)],[c_0_59])).
% 1.81/2.00 thf(c_0_69, plain, p63, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61]), c_0_62])])).
% 1.81/2.00 thf(c_0_70, plain, (~p37|p1|p36), inference(fof_simplification,[status(thm)],[ax1226])).
% 1.81/2.00 thf(c_0_71, plain, (p37|~p19), inference(split_conjunct,[status(thm)],[c_0_63])).
% 1.81/2.00 thf(c_0_72, plain, p19, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_50])])).
% 1.81/2.00 thf(c_0_73, plain, (p61|~p66|~p60), inference(split_conjunct,[status(thm)],[c_0_65])).
% 1.81/2.00 thf(c_0_74, plain, p66, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_40])])).
% 1.81/2.00 thf(c_0_75, plain, (~p61|~p62), inference(sr,[status(thm)],[c_0_67, c_0_47])).
% 1.81/2.00 thf(c_0_76, plain, p62, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])])).
% 1.81/2.00 thf(c_0_77, plain, ((~fmore @ fx @ fn_1|(fn_1)!=(fn_1)|~p35)&((fx)!=(fn_1)|(fn_1)!=(fn_1)|~p35)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax35])])])).
% 1.81/2.00 thf(c_0_78, plain, (~p36|p35), inference(fof_simplification,[status(thm)],[ax1225])).
% 1.81/2.00 thf(c_0_79, plain, (p1|p36|~p37), inference(split_conjunct,[status(thm)],[c_0_70])).
% 1.81/2.00 thf(c_0_80, plain, p37, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_72])])).
% 1.81/2.00 thf(c_0_81, plain, (~p51|(fx)=(fsuc @ f__0)), inference(fof_nnf,[status(thm)],[pax51])).
% 1.81/2.00 thf(c_0_82, plain, (p61|~p60), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 1.81/2.00 thf(c_0_83, plain, ~p61, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_76])])).
% 1.81/2.00 thf(c_0_84, plain, (~fmore @ fx @ fn_1|(fn_1)!=(fn_1)|~p35), inference(split_conjunct,[status(thm)],[c_0_77])).
% 1.81/2.00 thf(c_0_85, plain, (p35|~p36), inference(split_conjunct,[status(thm)],[c_0_78])).
% 1.81/2.00 thf(c_0_86, plain, p36, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_79, c_0_80])]), c_0_33])).
% 1.81/2.00 thf(c_0_87, plain, ((fx)=(fsuc @ f__0)|~p51), inference(split_conjunct,[status(thm)],[c_0_81])).
% 1.81/2.00 thf(c_0_88, plain, (~p133|(fsuc @ f__0)=(fsuc @ f__2)), inference(fof_nnf,[status(thm)],[pax133])).
% 1.81/2.00 thf(c_0_89, plain, (p60|p133), inference(split_conjunct,[status(thm)],[ax1106])).
% 1.81/2.00 thf(c_0_90, plain, ~p60, inference(sr,[status(thm)],[c_0_82, c_0_83])).
% 1.81/2.00 thf(c_0_91, plain, ![X1392:nat, X1393:nat]:(~p4|fmore @ (fpl @ X1392 @ X1393) @ X1392), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 1.81/2.00 thf(c_0_92, plain, ![X1390:nat]:(~p5|(fsuc @ X1390)=(fpl @ fn_1 @ X1390)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 1.81/2.00 thf(c_0_93, plain, (~p35|~fmore @ fx @ fn_1), inference(cn,[status(thm)],[c_0_84])).
% 1.81/2.00 thf(c_0_94, plain, p35, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_86])])).
% 1.81/2.00 thf(c_0_95, plain, (fx)=(fsuc @ f__0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_87, c_0_61])])).
% 1.81/2.00 thf(c_0_96, plain, ((fsuc @ f__0)=(fsuc @ f__2)|~p133), inference(split_conjunct,[status(thm)],[c_0_88])).
% 1.81/2.00 thf(c_0_97, plain, p133, inference(sr,[status(thm)],[c_0_89, c_0_90])).
% 1.81/2.00 thf(c_0_98, plain, ![X2:nat, X1:nat]:(fmore @ (fpl @ X1 @ X2) @ X1|~p4), inference(split_conjunct,[status(thm)],[c_0_91])).
% 1.81/2.00 thf(c_0_99, plain, p4, inference(split_conjunct,[status(thm)],[ax1261])).
% 1.81/2.00 thf(c_0_100, plain, ![X1:nat]:((fsuc @ X1)=(fpl @ fn_1 @ X1)|~p5), inference(split_conjunct,[status(thm)],[c_0_92])).
% 1.81/2.00 thf(c_0_101, plain, p5, inference(split_conjunct,[status(thm)],[ax1260])).
% 1.81/2.00 thf(c_0_102, plain, ~fmore @ (fsuc @ f__0) @ fn_1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94]), c_0_95])])).
% 1.81/2.00 thf(c_0_103, plain, (fsuc @ f__0)=(fsuc @ f__2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 1.81/2.00 thf(c_0_104, plain, ![X2:nat, X1:nat]:fmore @ (fpl @ X1 @ X2) @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 1.81/2.00 thf(c_0_105, plain, ![X1:nat]:(fpl @ fn_1 @ X1)=(fsuc @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_100, c_0_101])])).
% 1.81/2.00 thf(c_0_106, plain, ~fmore @ (fsuc @ f__2) @ fn_1, inference(rw,[status(thm)],[c_0_102, c_0_103])).
% 1.81/2.00 thf(c_0_107, plain, ![X1:nat]:fmore @ (fsuc @ X1) @ fn_1, inference(spm,[status(thm)],[c_0_104, c_0_105])).
% 1.81/2.00 thf(c_0_108, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_107])]), ['proof']).
% 1.81/2.00 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.81/2.00 thf(0,theorem,((~(((more @ x) @ n_1))) => (x = n_1)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.81/2.00 % SZS output end Proof
%------------------------------------------------------------------------------