%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP276^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 : n024.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:59 PM UTC 2025
% Result : Theorem 25.06s 24.29s
% Output : Proof 25.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : ITP276^3 : TPTP v9.2.1. Bugfixed v9.2.1.
% 0.07/0.15 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.36 % Computer : n024.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Oct 10 15:22:08 EDT 2025
% 0.14/0.36 % CPUTime :
% 25.06/24.29 % SZS status Theorem
% 25.06/24.29 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 25.06/24.29 % Inferences: 0
% 25.06/24.29 % SZS output start Proof
% 25.06/24.29 thf(conj_0,conjecture,(info = (some_P7363390416028606310at_nat @ ((product_Pair_nat_nat @ mi) @ ma)))).
% 25.06/24.29 thf(h0,negated_conjecture,(~((info = (some_P7363390416028606310at_nat @ ((product_Pair_nat_nat @ mi) @ ma))))),inference(assume_negation,[status(cth)],[conj_0])).
% 25.06/24.29 thf(pax1236, axiom, (p1236=>(fsuc)=(fplus_plus_nat @ fone_one_nat)), file('<stdin>', pax1236)).
% 25.06/24.29 thf(pax787, axiom, (p787=>(fone_one_nat)=(fsuc @ fzero_zero_nat)), file('<stdin>', pax787)).
% 25.06/24.29 thf(ax321, axiom, p1236, file('<stdin>', ax321)).
% 25.06/24.29 thf(pax1543, axiom, (p1543=>![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ X2=>(fminus_minus_nat @ X1 @ X2)=(fzero_zero_nat))), file('<stdin>', pax1543)).
% 25.06/24.29 thf(pax1337, axiom, (p1337=>![X297:nat, X298:nat]:(fminus_minus_nat @ (fplus_plus_nat @ X297 @ X298) @ X298)=(X297)), file('<stdin>', pax1337)).
% 25.06/24.29 thf(pax871, axiom, (p871=>(fm)=(fna)), file('<stdin>', pax871)).
% 25.06/24.29 thf(pax25, axiom, (p25=>(fdeg)=(fsuc @ fzero_zero_nat)), file('<stdin>', pax25)).
% 25.06/24.29 thf(ax770, axiom, p787, file('<stdin>', ax770)).
% 25.06/24.29 thf(ax14, axiom, p1543, file('<stdin>', ax14)).
% 25.06/24.29 thf(ax220, axiom, p1337, file('<stdin>', ax220)).
% 25.06/24.29 thf(pax883, axiom, (p883=>(fdeg)=(fplus_plus_nat @ fna @ fm)), file('<stdin>', pax883)).
% 25.06/24.29 thf(ax686, axiom, p871, file('<stdin>', ax686)).
% 25.06/24.29 thf(ax1532, axiom, p25, file('<stdin>', ax1532)).
% 25.06/24.29 thf(pax1147, axiom, (p1147=>![X643:nat, X644:nat]:ford_less_eq_nat @ X643 @ (fplus_plus_nat @ X643 @ X644)), file('<stdin>', pax1147)).
% 25.06/24.29 thf(pax160, axiom, (p160=>![X2049:nat]:(~((X2049)=(fzero_zero_nat))=>~(![X2050:nat]:~((X2049)=(fsuc @ X2050))))), file('<stdin>', pax160)).
% 25.06/24.29 thf(ax674, axiom, p883, file('<stdin>', ax674)).
% 25.06/24.29 thf(ax410, axiom, p1147, file('<stdin>', ax410)).
% 25.06/24.29 thf(ax1397, axiom, p160, file('<stdin>', ax1397)).
% 25.06/24.29 thf(pax1333, axiom, (p1333=>![X303:nat]:(fminus_minus_nat @ X303 @ fzero_zero_nat)=(X303)), file('<stdin>', pax1333)).
% 25.06/24.29 thf(nax669, axiom, (p669<=(fzero_zero_nat)=(fone_one_nat)), file('<stdin>', nax669)).
% 25.06/24.29 thf(ax888, axiom, ~(p669), file('<stdin>', ax888)).
% 25.06/24.29 thf(ax224, axiom, p1333, file('<stdin>', ax224)).
% 25.06/24.29 thf(c_0_22, plain, (~p1236|(fsuc)=(fplus_plus_nat @ fone_one_nat)), inference(fof_nnf,[status(thm)],[pax1236])).
% 25.06/24.29 thf(c_0_23, plain, (~p787|(fone_one_nat)=(fsuc @ fzero_zero_nat)), inference(fof_nnf,[status(thm)],[pax787])).
% 25.06/24.29 thf(c_0_24, plain, ((fsuc)=(fplus_plus_nat @ fone_one_nat)|~p1236), inference(split_conjunct,[status(thm)],[c_0_22])).
% 25.06/24.29 thf(c_0_25, plain, p1236, inference(split_conjunct,[status(thm)],[ax321])).
% 25.06/24.29 thf(c_0_26, plain, ![X2384:nat, X2385:nat]:(~p1543|(~ford_less_eq_nat @ X2384 @ X2385|(fminus_minus_nat @ X2384 @ X2385)=(fzero_zero_nat))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1543])])])).
% 25.06/24.29 thf(c_0_27, plain, ![X3036:nat, X3037:nat]:(~p1337|(fminus_minus_nat @ (fplus_plus_nat @ X3036 @ X3037) @ X3037)=(X3036)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1337])])])).
% 25.06/24.29 thf(c_0_28, plain, (~p871|(fm)=(fna)), inference(fof_nnf,[status(thm)],[pax871])).
% 25.06/24.29 thf(c_0_29, plain, (~p25|(fdeg)=(fsuc @ fzero_zero_nat)), inference(fof_nnf,[status(thm)],[pax25])).
% 25.06/24.29 thf(c_0_30, plain, ((fone_one_nat)=(fsuc @ fzero_zero_nat)|~p787), inference(split_conjunct,[status(thm)],[c_0_23])).
% 25.06/24.29 thf(c_0_31, plain, (fsuc)=(fplus_plus_nat @ fone_one_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 25.06/24.29 thf(c_0_32, plain, p787, inference(split_conjunct,[status(thm)],[ax770])).
% 25.06/24.29 thf(c_0_33, plain, ![X1:nat, X2:nat]:((fminus_minus_nat @ X1 @ X2)=(fzero_zero_nat)|~p1543|~ford_less_eq_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 25.06/24.29 thf(c_0_34, plain, p1543, inference(split_conjunct,[status(thm)],[ax14])).
% 25.06/24.29 thf(c_0_35, plain, ![X2:nat, X1:nat]:((fminus_minus_nat @ (fplus_plus_nat @ X1 @ X2) @ X2)=(X1)|~p1337), inference(split_conjunct,[status(thm)],[c_0_27])).
% 25.06/24.29 thf(c_0_36, plain, p1337, inference(split_conjunct,[status(thm)],[ax220])).
% 25.06/24.29 thf(c_0_37, plain, (~p883|(fdeg)=(fplus_plus_nat @ fna @ fm)), inference(fof_nnf,[status(thm)],[pax883])).
% 25.06/24.29 thf(c_0_38, plain, ((fm)=(fna)|~p871), inference(split_conjunct,[status(thm)],[c_0_28])).
% 25.06/24.29 thf(c_0_39, plain, p871, inference(split_conjunct,[status(thm)],[ax686])).
% 25.06/24.29 thf(c_0_40, plain, ((fdeg)=(fsuc @ fzero_zero_nat)|~p25), inference(split_conjunct,[status(thm)],[c_0_29])).
% 25.06/24.29 thf(c_0_41, plain, (fplus_plus_nat @ fone_one_nat @ fzero_zero_nat)=(fone_one_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32])])).
% 25.06/24.29 thf(c_0_42, plain, p25, inference(split_conjunct,[status(thm)],[ax1532])).
% 25.06/24.29 thf(c_0_43, plain, ![X3826:nat, X3827:nat]:(~p1147|ford_less_eq_nat @ X3826 @ (fplus_plus_nat @ X3826 @ X3827)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1147])])])).
% 25.06/24.29 thf(c_0_44, plain, ![X7206:nat]:(~p160|((X7206)=(fzero_zero_nat)|(X7206)=(fsuc @ (esk2440_1 @ X7206)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax160])])])])])).
% 25.06/24.29 thf(c_0_45, plain, ![X1:nat, X2:nat]:((fminus_minus_nat @ X1 @ X2)=(fzero_zero_nat)|~ford_less_eq_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 25.06/24.29 thf(c_0_46, plain, ![X2:nat, X1:nat]:(fminus_minus_nat @ (fplus_plus_nat @ X1 @ X2) @ X2)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 25.06/24.29 thf(c_0_47, plain, ((fdeg)=(fplus_plus_nat @ fna @ fm)|~p883), inference(split_conjunct,[status(thm)],[c_0_37])).
% 25.06/24.29 thf(c_0_48, plain, (fm)=(fna), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])])).
% 25.06/24.29 thf(c_0_49, plain, (fdeg)=(fone_one_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_31]), c_0_41]), c_0_42])])).
% 25.06/24.29 thf(c_0_50, plain, p883, inference(split_conjunct,[status(thm)],[ax674])).
% 25.06/24.29 thf(c_0_51, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ (fplus_plus_nat @ X1 @ X2)|~p1147), inference(split_conjunct,[status(thm)],[c_0_43])).
% 25.06/24.29 thf(c_0_52, plain, p1147, inference(split_conjunct,[status(thm)],[ax410])).
% 25.06/24.29 thf(c_0_53, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|(X1)=(fsuc @ (esk2440_1 @ X1))|~p160), inference(split_conjunct,[status(thm)],[c_0_44])).
% 25.06/24.29 thf(c_0_54, plain, p160, inference(split_conjunct,[status(thm)],[ax1397])).
% 25.06/24.29 thf(c_0_55, plain, ![X1:nat, X2:nat]:((X1)=(fzero_zero_nat)|~ford_less_eq_nat @ (fplus_plus_nat @ X1 @ X2) @ X2), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 25.06/24.29 thf(c_0_56, plain, (fplus_plus_nat @ fna @ fna)=(fone_one_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48]), c_0_49]), c_0_50])])).
% 25.06/24.29 thf(c_0_57, plain, ![X1:nat, X2:nat]:ford_less_eq_nat @ X1 @ (fplus_plus_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 25.06/24.29 thf(c_0_58, plain, ![X1:nat]:((fplus_plus_nat @ fone_one_nat @ (esk2440_1 @ X1))=(X1)|(X1)=(fzero_zero_nat)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_31]), c_0_54])])).
% 25.06/24.29 thf(c_0_59, plain, ![X3050:nat]:(~p1333|(fminus_minus_nat @ X3050 @ fzero_zero_nat)=(X3050)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1333])])])).
% 25.06/24.29 thf(c_0_60, plain, ((fzero_zero_nat)!=(fone_one_nat)|p669), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax669])])).
% 25.06/24.29 thf(c_0_61, plain, ~p669, inference(fof_simplification,[status(thm)],[ax888])).
% 25.06/24.29 thf(c_0_62, plain, ((fna)=(fzero_zero_nat)|~ford_less_eq_nat @ fone_one_nat @ fna), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 25.06/24.29 thf(c_0_63, plain, ![X1:nat]:((X1)=(fzero_zero_nat)|ford_less_eq_nat @ fone_one_nat @ X1), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 25.06/24.29 thf(c_0_64, plain, ![X1:nat]:((fminus_minus_nat @ X1 @ fzero_zero_nat)=(X1)|~p1333), inference(split_conjunct,[status(thm)],[c_0_59])).
% 25.06/24.29 thf(c_0_65, plain, p1333, inference(split_conjunct,[status(thm)],[ax224])).
% 25.06/24.29 thf(c_0_66, plain, (p669|(fzero_zero_nat)!=(fone_one_nat)), inference(split_conjunct,[status(thm)],[c_0_60])).
% 25.06/24.29 thf(c_0_67, plain, ~p669, inference(split_conjunct,[status(thm)],[c_0_61])).
% 25.06/24.29 thf(c_0_68, plain, (fminus_minus_nat @ fone_one_nat @ fna)=(fna), inference(spm,[status(thm)],[c_0_46, c_0_56])).
% 25.06/24.29 thf(c_0_69, plain, (fna)=(fzero_zero_nat), inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 25.06/24.29 thf(c_0_70, plain, ![X1:nat]:(fminus_minus_nat @ X1 @ fzero_zero_nat)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 25.06/24.29 thf(c_0_71, plain, (fone_one_nat)!=(fzero_zero_nat), inference(sr,[status(thm)],[c_0_66, c_0_67])).
% 25.06/24.29 thf(c_0_72, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69]), c_0_70]), c_0_69]), c_0_71]), ['proof']).
% 25.06/24.29 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 25.06/24.29 thf(0,theorem,(info = (some_P7363390416028606310at_nat @ ((product_Pair_nat_nat @ mi) @ ma))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 25.06/24.29 % SZS output end Proof
%------------------------------------------------------------------------------