%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : NUM737^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 : n015.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:59 PM UTC 2025
% Result : Theorem 98.66s 98.56s
% Output : Proof 98.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM737^1 : TPTP v9.2.0. Released v3.7.0.
% 0.00/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.11/0.33 % Computer : n015.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed Oct 8 23:06:08 EDT 2025
% 0.11/0.33 % CPUTime :
% 98.66/98.56 % SZS status Theorem
% 98.66/98.56 % Mode: mode478
% 98.66/98.56 % Inferences: 71
% 98.66/98.56 % SZS output start Proof
% 98.66/98.56 thf(satz44,conjecture,((more @ ((ts @ (num @ z)) @ (den @ u))) @ ((ts @ (num @ u)) @ (den @ z)))).
% 98.66/98.56 thf(h0,negated_conjecture,(~(((more @ ((ts @ (num @ z)) @ (den @ u))) @ ((ts @ (num @ u)) @ (den @ z))))),inference(assume_negation,[status(cth)],[satz44])).
% 98.66/98.56 thf(ax978, axiom, (~(p4)|p22), file('<stdin>', ax978)).
% 98.66/98.56 thf(ax892, axiom, (~(p22)|p107), file('<stdin>', ax892)).
% 98.66/98.56 thf(ax998, axiom, p4, file('<stdin>', ax998)).
% 98.66/98.56 thf(pax7, axiom, (p7=>![X7:nat, X8:nat, X9:nat]:(fts @ (fts @ X7 @ X8) @ X9)=(fts @ X7 @ (fts @ X8 @ X9))), file('<stdin>', pax7)).
% 98.66/98.56 thf(nax9, axiom, (p9<=fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz))), file('<stdin>', nax9)).
% 98.66/98.56 thf(ax993, axiom, ~(p9), file('<stdin>', ax993)).
% 98.66/98.56 thf(pax107, axiom, (p107=>![X1:nat]:(fmore @ (fts @ (fts @ (fnum @ fz) @ (fden @ fu)) @ X1) @ (fts @ (fts @ (fnum @ fu) @ (fden @ fz)) @ X1)=>fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz)))), file('<stdin>', pax107)).
% 98.66/98.56 thf(ax995, axiom, p7, file('<stdin>', ax995)).
% 98.66/98.56 thf(pax6, axiom, (p6=>![X7:nat, X8:nat]:(fts @ X7 @ X8)=(fts @ X8 @ X7)), file('<stdin>', pax6)).
% 98.66/98.56 thf(pax2, axiom, (p2=>(fts @ (fnum @ fx) @ (fden @ fz))=(fts @ (fnum @ fz) @ (fden @ fx))), file('<stdin>', pax2)).
% 98.66/98.56 thf(ax996, axiom, p6, file('<stdin>', ax996)).
% 98.66/98.56 thf(ax1000, axiom, p2, file('<stdin>', ax1000)).
% 98.66/98.56 thf(ax954, axiom, (~(p5)|p46), file('<stdin>', ax954)).
% 98.66/98.56 thf(pax5, axiom, (p5=>![X7:nat, X8:nat, X9:nat]:(fmore @ X7 @ X8=>fmore @ (fts @ X9 @ X7) @ (fts @ X9 @ X8))), file('<stdin>', pax5)).
% 98.66/98.56 thf(ax501, axiom, (~(p46)|p498), file('<stdin>', ax501)).
% 98.66/98.56 thf(ax997, axiom, p5, file('<stdin>', ax997)).
% 98.66/98.56 thf(pax1, axiom, (p1=>fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))), file('<stdin>', pax1)).
% 98.66/98.56 thf(pax498, axiom, (p498=>![X1:nat]:(fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))=>fmore @ (fts @ X1 @ (fts @ (fnum @ fx) @ (fden @ fy))) @ (fts @ X1 @ (fts @ (fnum @ fy) @ (fden @ fx))))), file('<stdin>', pax498)).
% 98.66/98.56 thf(ax1001, axiom, p1, file('<stdin>', ax1001)).
% 98.66/98.56 thf(pax3, axiom, (p3=>(fts @ (fnum @ fy) @ (fden @ fu))=(fts @ (fnum @ fu) @ (fden @ fy))), file('<stdin>', pax3)).
% 98.66/98.56 thf(ax999, axiom, p3, file('<stdin>', ax999)).
% 98.66/98.56 thf(c_0_21, plain, (~p4|p22), inference(fof_simplification,[status(thm)],[ax978])).
% 98.66/98.56 thf(c_0_22, plain, (~p22|p107), inference(fof_simplification,[status(thm)],[ax892])).
% 98.66/98.56 thf(c_0_23, plain, (p22|~p4), inference(split_conjunct,[status(thm)],[c_0_21])).
% 98.66/98.56 thf(c_0_24, plain, p4, inference(split_conjunct,[status(thm)],[ax998])).
% 98.66/98.56 thf(c_0_25, plain, ![X1566:nat, X1567:nat, X1568:nat]:(~p7|(fts @ (fts @ X1566 @ X1567) @ X1568)=(fts @ X1566 @ (fts @ X1567 @ X1568))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 98.66/98.56 thf(c_0_26, plain, (~fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz))|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 98.66/98.56 thf(c_0_27, plain, ~p9, inference(fof_simplification,[status(thm)],[ax993])).
% 98.66/98.56 thf(c_0_28, plain, ![X1284:nat]:(~p107|(~fmore @ (fts @ (fts @ (fnum @ fz) @ (fden @ fu)) @ X1284) @ (fts @ (fts @ (fnum @ fu) @ (fden @ fz)) @ X1284)|fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax107])])])).
% 98.66/98.56 thf(c_0_29, plain, (p107|~p22), inference(split_conjunct,[status(thm)],[c_0_22])).
% 98.66/98.56 thf(c_0_30, plain, p22, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 98.66/98.56 thf(c_0_31, plain, ![X1:nat, X3:nat, X4:nat]:((fts @ (fts @ X1 @ X3) @ X4)=(fts @ X1 @ (fts @ X3 @ X4))|~p7), inference(split_conjunct,[status(thm)],[c_0_25])).
% 98.66/98.56 thf(c_0_32, plain, p7, inference(split_conjunct,[status(thm)],[ax995])).
% 98.66/98.56 thf(c_0_33, plain, (p9|~fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 98.66/98.56 thf(c_0_34, plain, ~p9, inference(split_conjunct,[status(thm)],[c_0_27])).
% 98.66/98.56 thf(c_0_35, plain, ![X1572:nat, X1573:nat]:(~p6|(fts @ X1572 @ X1573)=(fts @ X1573 @ X1572)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 98.66/98.56 thf(c_0_36, plain, (~p2|(fts @ (fnum @ fx) @ (fden @ fz))=(fts @ (fnum @ fz) @ (fden @ fx))), inference(fof_nnf,[status(thm)],[pax2])).
% 98.66/98.56 thf(c_0_37, plain, ![X1:nat]:(fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz))|~p107|~fmore @ (fts @ (fts @ (fnum @ fz) @ (fden @ fu)) @ X1) @ (fts @ (fts @ (fnum @ fu) @ (fden @ fz)) @ X1)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 98.66/98.56 thf(c_0_38, plain, p107, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 98.66/98.56 thf(c_0_39, plain, ![X1:nat, X3:nat, X4:nat]:(fts @ (fts @ X1 @ X3) @ X4)=(fts @ X1 @ (fts @ X3 @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 98.66/98.56 thf(c_0_40, plain, ~fmore @ (fts @ (fnum @ fz) @ (fden @ fu)) @ (fts @ (fnum @ fu) @ (fden @ fz)), inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 98.66/98.56 thf(c_0_41, plain, ![X3:nat, X1:nat]:((fts @ X1 @ X3)=(fts @ X3 @ X1)|~p6), inference(split_conjunct,[status(thm)],[c_0_35])).
% 98.66/98.56 thf(c_0_42, plain, p6, inference(split_conjunct,[status(thm)],[ax996])).
% 98.66/98.56 thf(c_0_43, plain, ((fts @ (fnum @ fx) @ (fden @ fz))=(fts @ (fnum @ fz) @ (fden @ fx))|~p2), inference(split_conjunct,[status(thm)],[c_0_36])).
% 98.66/98.56 thf(c_0_44, plain, p2, inference(split_conjunct,[status(thm)],[ax1000])).
% 98.66/98.56 thf(c_0_45, plain, ![X1:nat]:~fmore @ (fts @ (fnum @ fz) @ (fts @ (fden @ fu) @ X1)) @ (fts @ (fnum @ fu) @ (fts @ (fden @ fz) @ X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_39])]), c_0_40])).
% 98.66/98.56 thf(c_0_46, plain, ![X3:nat, X1:nat]:(fts @ X1 @ X3)=(fts @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 98.66/98.56 thf(c_0_47, plain, (fts @ (fnum @ fx) @ (fden @ fz))=(fts @ (fnum @ fz) @ (fden @ fx)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 98.66/98.56 thf(c_0_48, plain, (~p5|p46), inference(fof_simplification,[status(thm)],[ax954])).
% 98.66/98.56 thf(c_0_49, plain, ![X1:nat]:~fmore @ (fts @ (fnum @ fz) @ (fts @ (fden @ fu) @ X1)) @ (fts @ (fnum @ fu) @ (fts @ X1 @ (fden @ fz))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 98.66/98.56 thf(c_0_50, plain, ![X1:nat]:(fts @ (fnum @ fx) @ (fts @ (fden @ fz) @ X1))=(fts @ (fnum @ fz) @ (fts @ (fden @ fx) @ X1)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_47]), c_0_39])).
% 98.66/98.56 thf(c_0_51, plain, ![X1576:nat, X1577:nat, X1578:nat]:(~p5|(~fmore @ X1576 @ X1577|fmore @ (fts @ X1578 @ X1576) @ (fts @ X1578 @ X1577))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 98.66/98.56 thf(c_0_52, plain, (~p46|p498), inference(fof_simplification,[status(thm)],[ax501])).
% 98.66/98.56 thf(c_0_53, plain, (p46|~p5), inference(split_conjunct,[status(thm)],[c_0_48])).
% 98.66/98.56 thf(c_0_54, plain, p5, inference(split_conjunct,[status(thm)],[ax997])).
% 98.66/98.56 thf(c_0_55, plain, (~p1|fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))), inference(fof_nnf,[status(thm)],[pax1])).
% 98.66/98.56 thf(c_0_56, plain, ![X1:nat, X3:nat]:~fmore @ (fts @ (fnum @ fz) @ (fts @ (fden @ fu) @ (fts @ X1 @ X3))) @ (fts @ (fnum @ fu) @ (fts @ X1 @ (fts @ X3 @ (fden @ fz)))), inference(spm,[status(thm)],[c_0_49, c_0_39])).
% 98.66/98.56 thf(c_0_57, plain, ![X1:nat]:(fts @ (fnum @ fx) @ (fts @ X1 @ (fden @ fz)))=(fts @ (fnum @ fz) @ (fts @ (fden @ fx) @ X1)), inference(spm,[status(thm)],[c_0_50, c_0_46])).
% 98.66/98.56 thf(c_0_58, plain, ![X1:nat, X3:nat, X4:nat]:(fts @ X1 @ (fts @ X3 @ X4))=(fts @ X3 @ (fts @ X1 @ X4)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_46]), c_0_39])).
% 98.66/98.56 thf(c_0_59, plain, ![X1:nat, X4:nat, X3:nat]:(fmore @ (fts @ X4 @ X1) @ (fts @ X4 @ X3)|~p5|~fmore @ X1 @ X3), inference(split_conjunct,[status(thm)],[c_0_51])).
% 98.66/98.56 thf(c_0_60, plain, ![X502:nat]:(~p498|(~fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))|fmore @ (fts @ X502 @ (fts @ (fnum @ fx) @ (fden @ fy))) @ (fts @ X502 @ (fts @ (fnum @ fy) @ (fden @ fx))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax498])])])).
% 98.66/98.56 thf(c_0_61, plain, (p498|~p46), inference(split_conjunct,[status(thm)],[c_0_52])).
% 98.66/98.56 thf(c_0_62, plain, p46, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 98.66/98.56 thf(c_0_63, plain, (fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))|~p1), inference(split_conjunct,[status(thm)],[c_0_55])).
% 98.66/98.56 thf(c_0_64, plain, p1, inference(split_conjunct,[status(thm)],[ax1001])).
% 98.66/98.56 thf(c_0_65, plain, ![X1:nat]:~fmore @ (fts @ (fnum @ fz) @ (fts @ (fnum @ fx) @ (fts @ (fden @ fu) @ X1))) @ (fts @ (fnum @ fz) @ (fts @ (fnum @ fu) @ (fts @ (fden @ fx) @ X1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_58]), c_0_58])).
% 98.66/98.56 thf(c_0_66, plain, ![X1:nat, X3:nat, X4:nat]:(fmore @ (fts @ X1 @ X3) @ (fts @ X1 @ X4)|~fmore @ X3 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_54])])).
% 98.66/98.56 thf(c_0_67, plain, (~p3|(fts @ (fnum @ fy) @ (fden @ fu))=(fts @ (fnum @ fu) @ (fden @ fy))), inference(fof_nnf,[status(thm)],[pax3])).
% 98.66/98.56 thf(c_0_68, plain, ![X1:nat]:(fmore @ (fts @ X1 @ (fts @ (fnum @ fx) @ (fden @ fy))) @ (fts @ X1 @ (fts @ (fnum @ fy) @ (fden @ fx)))|~p498|~fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx))), inference(split_conjunct,[status(thm)],[c_0_60])).
% 98.66/98.56 thf(c_0_69, plain, p498, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 98.66/98.56 thf(c_0_70, plain, fmore @ (fts @ (fnum @ fx) @ (fden @ fy)) @ (fts @ (fnum @ fy) @ (fden @ fx)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 98.66/98.56 thf(c_0_71, plain, ![X1:nat]:~fmore @ (fts @ (fnum @ fx) @ (fts @ (fden @ fu) @ X1)) @ (fts @ (fnum @ fu) @ (fts @ (fden @ fx) @ X1)), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 98.66/98.56 thf(c_0_72, plain, ((fts @ (fnum @ fy) @ (fden @ fu))=(fts @ (fnum @ fu) @ (fden @ fy))|~p3), inference(split_conjunct,[status(thm)],[c_0_67])).
% 98.66/98.56 thf(c_0_73, plain, p3, inference(split_conjunct,[status(thm)],[ax999])).
% 98.66/98.56 thf(c_0_74, plain, ![X1:nat]:fmore @ (fts @ X1 @ (fts @ (fnum @ fx) @ (fden @ fy))) @ (fts @ X1 @ (fts @ (fnum @ fy) @ (fden @ fx))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69]), c_0_70])])).
% 98.66/98.56 thf(c_0_75, plain, ![X1:nat]:~fmore @ (fts @ (fnum @ fx) @ (fts @ X1 @ (fden @ fu))) @ (fts @ (fnum @ fu) @ (fts @ (fden @ fx) @ X1)), inference(spm,[status(thm)],[c_0_71, c_0_46])).
% 98.66/98.56 thf(c_0_76, plain, (fts @ (fnum @ fy) @ (fden @ fu))=(fts @ (fnum @ fu) @ (fden @ fy)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 98.66/98.56 thf(c_0_77, plain, ![X1:nat]:fmore @ (fts @ (fnum @ fx) @ (fts @ X1 @ (fden @ fy))) @ (fts @ X1 @ (fts @ (fnum @ fy) @ (fden @ fx))), inference(spm,[status(thm)],[c_0_74, c_0_58])).
% 98.66/98.56 thf(c_0_78, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_46]), c_0_77])]), ['proof']).
% 98.66/98.56 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 98.66/98.56 thf(0,theorem,((more @ ((ts @ (num @ z)) @ (den @ u))) @ ((ts @ (num @ u)) @ (den @ z))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 98.66/98.56 % SZS output end Proof
%------------------------------------------------------------------------------