%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP146^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 : n001.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:06 PM UTC 2025
% Result : Theorem 37.65s 37.70s
% Output : Proof 37.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP146^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n001.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.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed Oct 8 18:08:38 EDT 2025
% 0.12/0.35 % CPUTime :
% 37.65/37.70 % SZS status Theorem
% 37.65/37.70 % Mode: mode478:USE_SINE=true:SINE_TOLERANCE=2.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 37.65/37.70 % Inferences: 140
% 37.65/37.70 % SZS output start Proof
% 37.65/37.70 thf(conj_0,conjecture,(xx = ((((auto_ll_on_flow0_a @ f) @ x) @ x2) @ ((minus_minus_real @ ss) @ tt)))).
% 37.65/37.70 thf(h0,negated_conjecture,(~((xx = ((((auto_ll_on_flow0_a @ f) @ x) @ x2) @ ((minus_minus_real @ ss) @ tt))))),inference(assume_negation,[status(cth)],[conj_0])).
% 37.65/37.70 thf(pax22, axiom, (p22=>![X116:real]:(fminus_minus_real @ fzero_zero_real @ X116)=(fuminus_uminus_real @ X116)), file('<stdin>', pax22)).
% 37.65/37.70 thf(pax101, axiom, (p101=>![X69:real, X66:real]:(fminus_minus_real @ X69 @ (fuminus_uminus_real @ X66))=(fplus_plus_real @ X69 @ X66)), file('<stdin>', pax101)).
% 37.65/37.70 thf(ax1090, axiom, p22, file('<stdin>', ax1090)).
% 37.65/37.70 thf(pax5, axiom, (p5=>fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)), file('<stdin>', pax5)).
% 37.65/37.70 thf(pax3, axiom, (p3=>(fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt)=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)), file('<stdin>', pax3)).
% 37.65/37.70 thf(ax345, axiom, (~(p84)|p762), file('<stdin>', ax345)).
% 37.65/37.70 thf(pax6, axiom, (p6=>fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)), file('<stdin>', pax6)).
% 37.65/37.70 thf(ax811, axiom, (~(p24)|p300), file('<stdin>', ax811)).
% 37.65/37.70 thf(ax363, axiom, (~(p82)|p744), file('<stdin>', ax363)).
% 37.65/37.70 thf(ax826, axiom, (~(p23)|p285), file('<stdin>', ax826)).
% 37.65/37.70 thf(pax761, axiom, (p761=>![X19:real]:(fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)=>(fmember_real @ X19 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))=>fmember_real @ (fplus_plus_real @ ftt @ X19) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)))), file('<stdin>', pax761)).
% 37.65/37.70 thf(ax1011, axiom, p101, file('<stdin>', ax1011)).
% 37.65/37.70 thf(ax1107, axiom, p5, file('<stdin>', ax1107)).
% 37.65/37.70 thf(ax1109, axiom, p3, file('<stdin>', ax1109)).
% 37.65/37.70 thf(ax346, axiom, (~(p762)|p761), file('<stdin>', ax346)).
% 37.65/37.70 thf(ax1028, axiom, p84, file('<stdin>', ax1028)).
% 37.65/37.70 thf(pax299, axiom, (p299=>(fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)=>fmember_real @ (fminus_minus_real @ fzero_zero_real @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)))), file('<stdin>', pax299)).
% 37.65/37.70 thf(ax1106, axiom, p6, file('<stdin>', ax1106)).
% 37.65/37.70 thf(ax812, axiom, (~(p300)|p299), file('<stdin>', ax812)).
% 37.65/37.70 thf(ax1088, axiom, p24, file('<stdin>', ax1088)).
% 37.65/37.70 thf(pax743, axiom, (p743=>![X23:real]:(fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)=>(fmember_real @ X23 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))=>(fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fplus_plus_real @ ftt @ X23))=(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt) @ X23)))), file('<stdin>', pax743)).
% 37.65/37.70 thf(ax364, axiom, (~(p744)|p743), file('<stdin>', ax364)).
% 37.65/37.70 thf(ax1030, axiom, p82, file('<stdin>', ax1030)).
% 37.65/37.70 thf(pax284, axiom, (p284=>(fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)=>(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ (fminus_minus_real @ fzero_zero_real @ fss))=(fx2))), file('<stdin>', pax284)).
% 37.65/37.70 thf(ax827, axiom, (~(p285)|p284), file('<stdin>', ax827)).
% 37.65/37.70 thf(ax1089, axiom, p23, file('<stdin>', ax1089)).
% 37.65/37.70 thf(pax61, axiom, (p61=>![X94:real, X95:real]:(fuminus_uminus_real @ (fminus_minus_real @ X94 @ X95))=(fminus_minus_real @ X95 @ X94)), file('<stdin>', pax61)).
% 37.65/37.70 thf(pax60, axiom, (p60=>![X94:real]:(fminus_minus_real @ X94 @ fzero_zero_real)=(X94)), file('<stdin>', pax60)).
% 37.65/37.70 thf(pax23, axiom, (p23=>![X116:real, X119:a]:(fmember_real @ X116 @ (fauto_l612940ivl0_a @ ff @ fx @ X119)=>(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ X119 @ X116) @ (fminus_minus_real @ fzero_zero_real @ X116))=(X119))), file('<stdin>', pax23)).
% 37.65/37.70 thf(ax1051, axiom, p61, file('<stdin>', ax1051)).
% 37.65/37.70 thf(ax1052, axiom, p60, file('<stdin>', ax1052)).
% 37.65/37.70 thf(nax121, axiom, (p121<=(fxx)=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ (fminus_minus_real @ fss @ ftt))), file('<stdin>', nax121)).
% 37.65/37.70 thf(ax991, axiom, ~(p121), file('<stdin>', ax991)).
% 37.65/37.70 thf(c_0_33, plain, ![X2613:real]:(~p22|(fminus_minus_real @ fzero_zero_real @ X2613)=(fuminus_uminus_real @ X2613)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 37.65/37.70 thf(c_0_34, plain, ![X2271:real, X2272:real]:(~p101|(fminus_minus_real @ X2271 @ (fuminus_uminus_real @ X2272))=(fplus_plus_real @ X2271 @ X2272)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax101])])])).
% 37.65/37.70 thf(c_0_35, plain, ![X1:real]:((fminus_minus_real @ fzero_zero_real @ X1)=(fuminus_uminus_real @ X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_33])).
% 37.65/37.70 thf(c_0_36, plain, p22, inference(split_conjunct,[status(thm)],[ax1090])).
% 37.65/37.70 thf(c_0_37, plain, (~p5|fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)), inference(fof_nnf,[status(thm)],[pax5])).
% 37.65/37.70 thf(c_0_38, plain, (~p3|(fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt)=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)), inference(fof_nnf,[status(thm)],[pax3])).
% 37.65/37.70 thf(c_0_39, plain, (~p84|p762), inference(fof_simplification,[status(thm)],[ax345])).
% 37.65/37.70 thf(c_0_40, plain, (~p6|fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)), inference(fof_nnf,[status(thm)],[pax6])).
% 37.65/37.70 thf(c_0_41, plain, (~p24|p300), inference(fof_simplification,[status(thm)],[ax811])).
% 37.65/37.70 thf(c_0_42, plain, (~p82|p744), inference(fof_simplification,[status(thm)],[ax363])).
% 37.65/37.70 thf(c_0_43, plain, (~p23|p285), inference(fof_simplification,[status(thm)],[ax826])).
% 37.65/37.70 thf(c_0_44, plain, ![X905:real]:(~p761|(~fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|(~fmember_real @ X905 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))|fmember_real @ (fplus_plus_real @ ftt @ X905) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax761])])])).
% 37.65/37.70 thf(c_0_45, plain, ![X1:real, X3:real]:((fminus_minus_real @ X1 @ (fuminus_uminus_real @ X3))=(fplus_plus_real @ X1 @ X3)|~p101), inference(split_conjunct,[status(thm)],[c_0_34])).
% 37.65/37.70 thf(c_0_46, plain, ![X1:real]:(fuminus_uminus_real @ X1)=(fminus_minus_real @ fzero_zero_real @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 37.65/37.70 thf(c_0_47, plain, p101, inference(split_conjunct,[status(thm)],[ax1011])).
% 37.65/37.70 thf(c_0_48, plain, (fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~p5), inference(split_conjunct,[status(thm)],[c_0_37])).
% 37.65/37.70 thf(c_0_49, plain, p5, inference(split_conjunct,[status(thm)],[ax1107])).
% 37.65/37.70 thf(c_0_50, plain, ((fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt)=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)|~p3), inference(split_conjunct,[status(thm)],[c_0_38])).
% 37.65/37.70 thf(c_0_51, plain, p3, inference(split_conjunct,[status(thm)],[ax1109])).
% 37.65/37.70 thf(c_0_52, plain, (~p762|p761), inference(fof_simplification,[status(thm)],[ax346])).
% 37.65/37.70 thf(c_0_53, plain, (p762|~p84), inference(split_conjunct,[status(thm)],[c_0_39])).
% 37.65/37.70 thf(c_0_54, plain, p84, inference(split_conjunct,[status(thm)],[ax1028])).
% 37.65/37.70 thf(c_0_55, plain, (~p299|(~fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)|fmember_real @ (fminus_minus_real @ fzero_zero_real @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)))), inference(fof_nnf,[status(thm)],[pax299])).
% 37.65/37.70 thf(c_0_56, plain, (fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)|~p6), inference(split_conjunct,[status(thm)],[c_0_40])).
% 37.65/37.70 thf(c_0_57, plain, p6, inference(split_conjunct,[status(thm)],[ax1106])).
% 37.65/37.70 thf(c_0_58, plain, (~p300|p299), inference(fof_simplification,[status(thm)],[ax812])).
% 37.65/37.70 thf(c_0_59, plain, (p300|~p24), inference(split_conjunct,[status(thm)],[c_0_41])).
% 37.65/37.70 thf(c_0_60, plain, p24, inference(split_conjunct,[status(thm)],[ax1088])).
% 37.65/37.70 thf(c_0_61, plain, ![X963:real]:(~p743|(~fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|(~fmember_real @ X963 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))|(fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fplus_plus_real @ ftt @ X963))=(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt) @ X963)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax743])])])).
% 37.65/37.70 thf(c_0_62, plain, (~p744|p743), inference(fof_simplification,[status(thm)],[ax364])).
% 37.65/37.70 thf(c_0_63, plain, (p744|~p82), inference(split_conjunct,[status(thm)],[c_0_42])).
% 37.65/37.70 thf(c_0_64, plain, p82, inference(split_conjunct,[status(thm)],[ax1030])).
% 37.65/37.70 thf(c_0_65, plain, (~p284|(~fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)|(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ (fminus_minus_real @ fzero_zero_real @ fss))=(fx2))), inference(fof_nnf,[status(thm)],[pax284])).
% 37.65/37.70 thf(c_0_66, plain, (~p285|p284), inference(fof_simplification,[status(thm)],[ax827])).
% 37.65/37.70 thf(c_0_67, plain, (p285|~p23), inference(split_conjunct,[status(thm)],[c_0_43])).
% 37.65/37.70 thf(c_0_68, plain, p23, inference(split_conjunct,[status(thm)],[ax1089])).
% 37.65/37.70 thf(c_0_69, plain, ![X1:real]:(fmember_real @ (fplus_plus_real @ ftt @ X1) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~p761|~fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))), inference(split_conjunct,[status(thm)],[c_0_44])).
% 37.65/37.70 thf(c_0_70, plain, ![X1:real, X3:real]:(fplus_plus_real @ X1 @ X3)=(fminus_minus_real @ X1 @ (fminus_minus_real @ fzero_zero_real @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_47])])).
% 37.65/37.70 thf(c_0_71, plain, fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 37.65/37.70 thf(c_0_72, plain, (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt)=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 37.65/37.70 thf(c_0_73, plain, (p761|~p762), inference(split_conjunct,[status(thm)],[c_0_52])).
% 37.65/37.70 thf(c_0_74, plain, p762, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 37.65/37.70 thf(c_0_75, plain, (fmember_real @ (fminus_minus_real @ fzero_zero_real @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))|~p299|~fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)), inference(split_conjunct,[status(thm)],[c_0_55])).
% 37.65/37.70 thf(c_0_76, plain, fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 37.65/37.70 thf(c_0_77, plain, (p299|~p300), inference(split_conjunct,[status(thm)],[c_0_58])).
% 37.65/37.70 thf(c_0_78, plain, p300, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])])).
% 37.65/37.70 thf(c_0_79, plain, ![X2429:real, X2430:real]:(~p61|(fuminus_uminus_real @ (fminus_minus_real @ X2429 @ X2430))=(fminus_minus_real @ X2430 @ X2429)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax61])])])).
% 37.65/37.70 thf(c_0_80, plain, ![X2433:real]:(~p60|(fminus_minus_real @ X2433 @ fzero_zero_real)=(X2433)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax60])])])).
% 37.65/37.70 thf(c_0_81, plain, ![X1:real]:((fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fplus_plus_real @ ftt @ X1))=(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt) @ X1)|~p743|~fmember_real @ ftt @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ ftt))), inference(split_conjunct,[status(thm)],[c_0_61])).
% 37.65/37.70 thf(c_0_82, plain, (p743|~p744), inference(split_conjunct,[status(thm)],[c_0_62])).
% 37.65/37.70 thf(c_0_83, plain, p744, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 37.65/37.70 thf(c_0_84, plain, ((fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ (fminus_minus_real @ fzero_zero_real @ fss))=(fx2)|~p284|~fmember_real @ fss @ (fauto_l612940ivl0_a @ ff @ fx @ fx2)), inference(split_conjunct,[status(thm)],[c_0_65])).
% 37.65/37.70 thf(c_0_85, plain, (p284|~p285), inference(split_conjunct,[status(thm)],[c_0_66])).
% 37.65/37.70 thf(c_0_86, plain, p285, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68])])).
% 37.65/37.70 thf(c_0_87, plain, ![X2609:real, X2610:a]:(~p23|(~fmember_real @ X2609 @ (fauto_l612940ivl0_a @ ff @ fx @ X2610)|(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ X2610 @ X2609) @ (fminus_minus_real @ fzero_zero_real @ X2609))=(X2610))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax23])])])).
% 37.65/37.70 thf(c_0_88, plain, ![X1:real]:(fmember_real @ (fminus_minus_real @ ftt @ (fminus_minus_real @ fzero_zero_real @ X1)) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))|~p761), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70]), c_0_71]), c_0_72])])).
% 37.65/37.70 thf(c_0_89, plain, p761, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 37.65/37.70 thf(c_0_90, plain, (fmember_real @ (fminus_minus_real @ fzero_zero_real @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))|~p299), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_76])])).
% 37.65/37.70 thf(c_0_91, plain, p299, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_78])])).
% 37.65/37.70 thf(c_0_92, plain, ![X3:real, X1:real]:((fuminus_uminus_real @ (fminus_minus_real @ X1 @ X3))=(fminus_minus_real @ X3 @ X1)|~p61), inference(split_conjunct,[status(thm)],[c_0_79])).
% 37.65/37.70 thf(c_0_93, plain, p61, inference(split_conjunct,[status(thm)],[ax1051])).
% 37.65/37.70 thf(c_0_94, plain, ![X1:real]:((fminus_minus_real @ X1 @ fzero_zero_real)=(X1)|~p60), inference(split_conjunct,[status(thm)],[c_0_80])).
% 37.65/37.70 thf(c_0_95, plain, p60, inference(split_conjunct,[status(thm)],[ax1052])).
% 37.65/37.70 thf(c_0_96, plain, ![X1:real]:((fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fminus_minus_real @ ftt @ (fminus_minus_real @ fzero_zero_real @ X1)))=(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ X1)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))|~p743), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_81, c_0_70]), c_0_72]), c_0_71]), c_0_72])])).
% 37.65/37.70 thf(c_0_97, plain, p743, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 37.65/37.70 thf(c_0_98, plain, ((fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ (fminus_minus_real @ fzero_zero_real @ fss))=(fx2)|~p284), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_84, c_0_76])])).
% 37.65/37.70 thf(c_0_99, plain, p284, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_86])])).
% 37.65/37.70 thf(c_0_100, plain, ((fxx)!=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ (fminus_minus_real @ fss @ ftt))|p121), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax121])])).
% 37.65/37.70 thf(c_0_101, plain, ~p121, inference(fof_simplification,[status(thm)],[ax991])).
% 37.65/37.70 thf(c_0_102, plain, ![X1:real, X2:a]:((fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ X2 @ X1) @ (fminus_minus_real @ fzero_zero_real @ X1))=(X2)|~p23|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ X2)), inference(split_conjunct,[status(thm)],[c_0_87])).
% 37.65/37.70 thf(c_0_103, plain, ![X1:real]:(fmember_real @ (fminus_minus_real @ ftt @ (fminus_minus_real @ fzero_zero_real @ X1)) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 37.65/37.70 thf(c_0_104, plain, fmember_real @ (fminus_minus_real @ fzero_zero_real @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_91])])).
% 37.65/37.70 thf(c_0_105, plain, ![X3:real, X1:real]:(fminus_minus_real @ fzero_zero_real @ (fminus_minus_real @ X1 @ X3))=(fminus_minus_real @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_46]), c_0_93])])).
% 37.65/37.70 thf(c_0_106, plain, ![X1:real]:(fminus_minus_real @ X1 @ fzero_zero_real)=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_94, c_0_95])])).
% 37.65/37.70 thf(c_0_107, plain, ![X1:real]:((fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fminus_minus_real @ ftt @ (fminus_minus_real @ fzero_zero_real @ X1)))=(fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ X1)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 37.65/37.70 thf(c_0_108, plain, (fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ fss) @ (fminus_minus_real @ fzero_zero_real @ fss))=(fx2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 37.65/37.70 thf(c_0_109, plain, (p121|(fxx)!=(fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ (fminus_minus_real @ fss @ ftt))), inference(split_conjunct,[status(thm)],[c_0_100])).
% 37.65/37.70 thf(c_0_110, plain, ~p121, inference(split_conjunct,[status(thm)],[c_0_101])).
% 37.65/37.70 thf(c_0_111, plain, ![X1:real, X2:a]:((fauto_ll_on_flow0_a @ ff @ fx @ (fauto_ll_on_flow0_a @ ff @ fx @ X2 @ X1) @ (fminus_minus_real @ fzero_zero_real @ X1))=(X2)|~fmember_real @ X1 @ (fauto_l612940ivl0_a @ ff @ fx @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_102, c_0_68])])).
% 37.65/37.70 thf(c_0_112, plain, fmember_real @ (fminus_minus_real @ ftt @ fss) @ (fauto_l612940ivl0_a @ ff @ fx @ fxx), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_104]), c_0_105]), c_0_106])).
% 37.65/37.70 thf(c_0_113, plain, (fauto_ll_on_flow0_a @ ff @ fx @ fxx @ (fminus_minus_real @ ftt @ fss))=(fx2), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_104]), c_0_105]), c_0_106]), c_0_108])).
% 37.65/37.70 thf(c_0_114, plain, (fauto_ll_on_flow0_a @ ff @ fx @ fx2 @ (fminus_minus_real @ fss @ ftt))!=(fxx), inference(sr,[status(thm)],[c_0_109, c_0_110])).
% 37.65/37.70 thf(c_0_115, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_112]), c_0_113]), c_0_105]), c_0_114]), ['proof']).
% 37.65/37.70 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 37.65/37.70 thf(0,theorem,(xx = ((((auto_ll_on_flow0_a @ f) @ x) @ x2) @ ((minus_minus_real @ ss) @ tt))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 37.65/37.70 % SZS output end Proof
%------------------------------------------------------------------------------