%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM766^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 : n026.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:06 PM UTC 2025
% Result : Theorem 1.50s 1.71s
% Output : Proof 1.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : NUM766^1 : TPTP v9.2.0. Released v3.7.0.
% 0.05/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 22:26:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 1.50/1.71 % SZS status Theorem
% 1.50/1.71 % Mode: mode506
% 1.50/1.71 % Inferences: 854
% 1.50/1.71 % SZS output start Proof
% 1.50/1.71 thf(satz67a,conjecture,(~((![X1:frac]:(~(((eq @ ((pf @ y) @ X1)) @ x))))))).
% 1.50/1.71 thf(h0,negated_conjecture,(![X1:frac]:(~(((eq @ ((pf @ y) @ X1)) @ x)))),inference(assume_negation,[status(cth)],[satz67a])).
% 1.50/1.71 thf(pax9, axiom, (p9=>![X16:nat, X15:nat, X17:nat]:feq @ (fpf @ (ffr @ X16 @ X17) @ (ffr @ X15 @ X17)) @ (ffr @ (fpl @ X16 @ X15) @ X17)), file('<stdin>', pax9)).
% 1.50/1.71 thf(nax2, axiom, (p2<=![X22:nat]:~((fts @ (fnum @ fx) @ (fden @ fy))=(fpl @ (fts @ (fnum @ fy) @ (fden @ fx)) @ X22))), file('<stdin>', nax2)).
% 1.50/1.71 thf(ax1880, axiom, ~(p2), file('<stdin>', ax1880)).
% 1.50/1.71 thf(pax4, axiom, (p4=>![X18:frac, X19:frac, X20:frac]:(feq @ X18 @ X19=>(feq @ X19 @ X20=>feq @ X18 @ X20))), file('<stdin>', pax4)).
% 1.50/1.71 thf(pax11, axiom, (p11=>![X12:frac, X15:nat]:feq @ (ffr @ (fts @ (fnum @ X12) @ X15) @ (fts @ (fden @ X12) @ X15)) @ X12), file('<stdin>', pax11)).
% 1.50/1.71 thf(ax1873, axiom, p9, file('<stdin>', ax1873)).
% 1.50/1.71 thf(ax1878, axiom, p4, file('<stdin>', ax1878)).
% 1.50/1.71 thf(ax1871, axiom, p11, file('<stdin>', ax1871)).
% 1.50/1.71 thf(pax8, axiom, (p8=>![X16:nat, X15:nat]:(fts @ X16 @ X15)=(fts @ X15 @ X16)), file('<stdin>', pax8)).
% 1.50/1.71 thf(pax5, axiom, (p5=>![X18:frac, X19:frac, X20:frac, X21:frac]:(feq @ X18 @ X19=>(feq @ X20 @ X21=>feq @ (fpf @ X18 @ X20) @ (fpf @ X19 @ X21)))), file('<stdin>', pax5)).
% 1.50/1.71 thf(ax1874, axiom, p8, file('<stdin>', ax1874)).
% 1.50/1.71 thf(ax1877, axiom, p5, file('<stdin>', ax1877)).
% 1.50/1.71 thf(pax6, axiom, (p6=>![X18:frac, X15:nat]:feq @ X18 @ (ffr @ (fts @ (fnum @ X18) @ X15) @ (fts @ (fden @ X18) @ X15))), file('<stdin>', pax6)).
% 1.50/1.71 thf(ax1876, axiom, p6, file('<stdin>', ax1876)).
% 1.50/1.71 thf(pax1, axiom, (p1=>![X23:frac]:~(feq @ (fpf @ fy @ X23) @ fx)), file('<stdin>', pax1)).
% 1.50/1.71 thf(pax7, axiom, (p7=>![X18:frac]:feq @ X18 @ X18), file('<stdin>', pax7)).
% 1.50/1.71 thf(ax1881, axiom, p1, file('<stdin>', ax1881)).
% 1.50/1.71 thf(ax1875, axiom, p7, file('<stdin>', ax1875)).
% 1.50/1.71 thf(c_0_18, plain, ![X2528:nat, X2529:nat, X2530:nat]:(~p9|feq @ (fpf @ (ffr @ X2528 @ X2530) @ (ffr @ X2529 @ X2530)) @ (ffr @ (fpl @ X2528 @ X2529) @ X2530)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax9])])])).
% 1.50/1.71 thf(c_0_19, plain, ((fts @ (fnum @ fx) @ (fden @ fy))=(fpl @ (fts @ (fnum @ fy) @ (fden @ fx)) @ esk1268_0)|p2), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])])])).
% 1.50/1.71 thf(c_0_20, plain, ~p2, inference(fof_simplification,[status(thm)],[ax1880])).
% 1.50/1.71 thf(c_0_21, plain, ![X2552:frac, X2553:frac, X2554:frac]:(~p4|(~feq @ X2552 @ X2553|(~feq @ X2553 @ X2554|feq @ X2552 @ X2554))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 1.50/1.71 thf(c_0_22, plain, ![X2524:frac, X2525:nat]:(~p11|feq @ (ffr @ (fts @ (fnum @ X2524) @ X2525) @ (fts @ (fden @ X2524) @ X2525)) @ X2524), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax11])])])).
% 1.50/1.71 thf(c_0_23, plain, ![X1:nat, X7:nat, X5:nat]:(feq @ (fpf @ (ffr @ X1 @ X5) @ (ffr @ X7 @ X5)) @ (ffr @ (fpl @ X1 @ X7) @ X5)|~p9), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.50/1.71 thf(c_0_24, plain, p9, inference(split_conjunct,[status(thm)],[ax1873])).
% 1.50/1.71 thf(c_0_25, plain, ((fts @ (fnum @ fx) @ (fden @ fy))=(fpl @ (fts @ (fnum @ fy) @ (fden @ fx)) @ esk1268_0)|p2), inference(split_conjunct,[status(thm)],[c_0_19])).
% 1.50/1.71 thf(c_0_26, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_20])).
% 1.50/1.71 thf(c_0_27, plain, ![X2:frac, X3:frac, X4:frac]:(feq @ X2 @ X4|~p4|~feq @ X2 @ X3|~feq @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.50/1.71 thf(c_0_28, plain, p4, inference(split_conjunct,[status(thm)],[ax1878])).
% 1.50/1.71 thf(c_0_29, plain, ![X1:nat, X2:frac]:(feq @ (ffr @ (fts @ (fnum @ X2) @ X1) @ (fts @ (fden @ X2) @ X1)) @ X2|~p11), inference(split_conjunct,[status(thm)],[c_0_22])).
% 1.50/1.71 thf(c_0_30, plain, p11, inference(split_conjunct,[status(thm)],[ax1871])).
% 1.50/1.71 thf(c_0_31, plain, ![X2534:nat, X2535:nat]:(~p8|(fts @ X2534 @ X2535)=(fts @ X2535 @ X2534)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax8])])])).
% 1.50/1.71 thf(c_0_32, plain, ![X1:nat, X7:nat, X5:nat]:feq @ (fpf @ (ffr @ X1 @ X5) @ (ffr @ X7 @ X5)) @ (ffr @ (fpl @ X1 @ X7) @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 1.50/1.71 thf(c_0_33, plain, (fpl @ (fts @ (fnum @ fy) @ (fden @ fx)) @ esk1268_0)=(fts @ (fnum @ fx) @ (fden @ fy)), inference(sr,[status(thm)],[c_0_25, c_0_26])).
% 1.50/1.71 thf(c_0_34, plain, ![X2544:frac, X2545:frac, X2546:frac, X2547:frac]:(~p5|(~feq @ X2544 @ X2545|(~feq @ X2546 @ X2547|feq @ (fpf @ X2544 @ X2546) @ (fpf @ X2545 @ X2547)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 1.50/1.71 thf(c_0_35, plain, ![X2:frac, X3:frac, X4:frac]:(feq @ X2 @ X3|~feq @ X4 @ X3|~feq @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 1.50/1.71 thf(c_0_36, plain, ![X1:nat, X2:frac]:feq @ (ffr @ (fts @ (fnum @ X2) @ X1) @ (fts @ (fden @ X2) @ X1)) @ X2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 1.50/1.71 thf(c_0_37, plain, ![X5:nat, X1:nat]:((fts @ X1 @ X5)=(fts @ X5 @ X1)|~p8), inference(split_conjunct,[status(thm)],[c_0_31])).
% 1.50/1.71 thf(c_0_38, plain, p8, inference(split_conjunct,[status(thm)],[ax1874])).
% 1.50/1.71 thf(c_0_39, plain, ![X1:nat]:feq @ (fpf @ (ffr @ (fts @ (fnum @ fy) @ (fden @ fx)) @ X1) @ (ffr @ esk1268_0 @ X1)) @ (ffr @ (fts @ (fnum @ fx) @ (fden @ fy)) @ X1), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 1.50/1.71 thf(c_0_40, plain, ![X2:frac, X3:frac, X4:frac, X6:frac]:(feq @ (fpf @ X2 @ X4) @ (fpf @ X3 @ X6)|~p5|~feq @ X2 @ X3|~feq @ X4 @ X6), inference(split_conjunct,[status(thm)],[c_0_34])).
% 1.50/1.71 thf(c_0_41, plain, p5, inference(split_conjunct,[status(thm)],[ax1877])).
% 1.50/1.71 thf(c_0_42, plain, ![X2540:frac, X2541:nat]:(~p6|feq @ X2540 @ (ffr @ (fts @ (fnum @ X2540) @ X2541) @ (fts @ (fden @ X2540) @ X2541))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 1.50/1.71 thf(c_0_43, plain, ![X3:frac, X2:frac, X1:nat]:(feq @ X2 @ X3|~feq @ X2 @ (ffr @ (fts @ (fnum @ X3) @ X1) @ (fts @ (fden @ X3) @ X1))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 1.50/1.71 thf(c_0_44, plain, ![X5:nat, X1:nat]:(fts @ X1 @ X5)=(fts @ X5 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 1.50/1.71 thf(c_0_45, plain, ![X2:frac, X1:nat]:(feq @ X2 @ (ffr @ (fts @ (fnum @ fx) @ (fden @ fy)) @ X1)|~feq @ X2 @ (fpf @ (ffr @ (fts @ (fnum @ fy) @ (fden @ fx)) @ X1) @ (ffr @ esk1268_0 @ X1))), inference(spm,[status(thm)],[c_0_35, c_0_39])).
% 1.50/1.71 thf(c_0_46, plain, ![X3:frac, X2:frac, X6:frac, X4:frac]:(feq @ (fpf @ X2 @ X3) @ (fpf @ X4 @ X6)|~feq @ X3 @ X6|~feq @ X2 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41])])).
% 1.50/1.71 thf(c_0_47, plain, ![X2:frac, X1:nat]:(feq @ X2 @ (ffr @ (fts @ (fnum @ X2) @ X1) @ (fts @ (fden @ X2) @ X1))|~p6), inference(split_conjunct,[status(thm)],[c_0_42])).
% 1.50/1.71 thf(c_0_48, plain, p6, inference(split_conjunct,[status(thm)],[ax1876])).
% 1.50/1.71 thf(c_0_49, plain, ![X2560:frac]:(~p1|~feq @ (fpf @ fy @ X2560) @ fx), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1])])])])).
% 1.50/1.71 thf(c_0_50, plain, ![X2538:frac]:(~p7|feq @ X2538 @ X2538), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 1.50/1.71 thf(c_0_51, plain, ![X1:nat, X2:frac, X3:frac]:(feq @ X2 @ X3|~feq @ X2 @ (ffr @ (fts @ (fnum @ X3) @ X1) @ (fts @ X1 @ (fden @ X3)))), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 1.50/1.71 thf(c_0_52, plain, ![X3:frac, X2:frac, X1:nat]:(feq @ (fpf @ X2 @ X3) @ (ffr @ (fts @ (fnum @ fx) @ (fden @ fy)) @ X1)|~feq @ X2 @ (ffr @ (fts @ (fnum @ fy) @ (fden @ fx)) @ X1)|~feq @ X3 @ (ffr @ esk1268_0 @ X1)), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 1.50/1.71 thf(c_0_53, plain, ![X2:frac, X1:nat]:feq @ X2 @ (ffr @ (fts @ (fnum @ X2) @ X1) @ (fts @ (fden @ X2) @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48])])).
% 1.50/1.71 thf(c_0_54, plain, ![X2:frac]:(~p1|~feq @ (fpf @ fy @ X2) @ fx), inference(split_conjunct,[status(thm)],[c_0_49])).
% 1.50/1.71 thf(c_0_55, plain, p1, inference(split_conjunct,[status(thm)],[ax1881])).
% 1.50/1.71 thf(c_0_56, plain, ![X2:frac]:(feq @ X2 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_50])).
% 1.50/1.71 thf(c_0_57, plain, p7, inference(split_conjunct,[status(thm)],[ax1875])).
% 1.50/1.71 thf(c_0_58, plain, ![X2:frac, X3:frac]:(feq @ (fpf @ X2 @ X3) @ fx|~feq @ X2 @ (ffr @ (fts @ (fnum @ fy) @ (fden @ fx)) @ (fts @ (fden @ fx) @ (fden @ fy)))|~feq @ X3 @ (ffr @ esk1268_0 @ (fts @ (fden @ fx) @ (fden @ fy)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_44]), c_0_44])).
% 1.50/1.71 thf(c_0_59, plain, ![X1:nat, X2:frac]:feq @ X2 @ (ffr @ (fts @ (fnum @ X2) @ X1) @ (fts @ X1 @ (fden @ X2))), inference(spm,[status(thm)],[c_0_53, c_0_44])).
% 1.50/1.71 thf(c_0_60, plain, ![X2:frac]:~feq @ (fpf @ fy @ X2) @ fx, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 1.50/1.71 thf(c_0_61, plain, ![X1:nat, X2:frac, X3:frac]:(feq @ X2 @ X3|~feq @ X2 @ (ffr @ (fts @ X1 @ (fnum @ X3)) @ (fts @ X1 @ (fden @ X3)))), inference(spm,[status(thm)],[c_0_51, c_0_44])).
% 1.50/1.71 thf(c_0_62, plain, ![X2:frac]:feq @ X2 @ X2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 1.50/1.71 thf(c_0_63, plain, ![X2:frac]:~feq @ X2 @ (ffr @ esk1268_0 @ (fts @ (fden @ fx) @ (fden @ fy))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60])).
% 1.50/1.71 thf(c_0_64, plain, ![X1:nat, X2:frac]:feq @ (ffr @ (fts @ X1 @ (fnum @ X2)) @ (fts @ X1 @ (fden @ X2))) @ X2, inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 1.50/1.71 thf(c_0_65, plain, ($false), inference(spm,[status(thm)],[c_0_63, c_0_64]), ['proof']).
% 1.50/1.71 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.50/1.71 thf(0,theorem,(~((![X1:frac]:(~(((eq @ ((pf @ y) @ X1)) @ x)))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.50/1.71 % SZS output end Proof
%------------------------------------------------------------------------------