%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP199^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 : n014.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:16 PM UTC 2025
% Result : Theorem 3.65s 3.90s
% Output : Proof 3.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP199^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.13/0.35 % Computer : n014.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 18:12:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.65/3.90 % SZS status Theorem
% 3.65/3.90 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 3.65/3.90 % Inferences: 18
% 3.65/3.90 % SZS output start Proof
% 3.65/3.90 thf(ty_denotational_interp, type, denotational_interp : $tType).
% 3.65/3.90 thf(ty_option_trm, type, option_trm : $tType).
% 3.65/3.90 thf(ty_variable, type, variable : $tType).
% 3.65/3.90 thf(ty_produc1418842292n_game, type, produc1418842292n_game : $tType).
% 3.65/3.90 thf(ty_char, type, char : $tType).
% 3.65/3.90 thf(ty_trm, type, trm : $tType).
% 3.65/3.90 thf(ty_set_variable, type, set_variable : $tType).
% 3.65/3.90 thf(ty_real, type, real : $tType).
% 3.65/3.90 thf(ty_uSubst516392818stappt, type, uSubst516392818stappt : (produc1418842292n_game>set_variable>trm>option_trm)).
% 3.65/3.90 thf(ty_zero_zero_real, type, zero_zero_real : real).
% 3.65/3.90 thf(ty_rVar, type, rVar : (char>variable)).
% 3.65/3.90 thf(ty_theta, type, theta : trm).
% 3.65/3.90 thf(ty_uSubst1599435252djoint, type, uSubst1599435252djoint : (produc1418842292n_game>denotational_interp>(variable>real)>denotational_interp)).
% 3.65/3.90 thf(ty_denota1778088425es_ODE, type, denota1778088425es_ODE : (denotational_interp>(real>variable>real)>char>trm>$o)).
% 3.65/3.90 thf(ty_eigen__1, type, eigen__1 : (trm>denotational_interp>trm>denotational_interp>char>(real>variable>real)>variable>real)).
% 3.65/3.90 thf(ty_eigen__0, type, eigen__0 : (trm>denotational_interp>trm>denotational_interp>char>(real>variable>real)>variable>real)).
% 3.65/3.90 thf(ty_dVar, type, dVar : (char>variable)).
% 3.65/3.90 thf(ty_u, type, u : set_variable).
% 3.65/3.90 thf(ty_i, type, i : denotational_interp).
% 3.65/3.90 thf(ty_insert_variable, type, insert_variable : (variable>set_variable>set_variable)).
% 3.65/3.90 thf(ty_bot_bot_set_variable, type, bot_bot_set_variable : set_variable).
% 3.65/3.90 thf(ty_denota1863255036rm_sem, type, denota1863255036rm_sem : (denotational_interp>trm>(variable>real)>real)).
% 3.65/3.90 thf(ty_omega, type, omega : (variable>real)).
% 3.65/3.90 thf(ty_the_trm, type, the_trm : (option_trm>trm)).
% 3.65/3.90 thf(ty_sup_sup_set_variable, type, sup_sup_set_variable : (set_variable>set_variable>set_variable)).
% 3.65/3.90 thf(ty_f, type, f : (real>variable>real)).
% 3.65/3.90 thf(ty_denota1419872369iation, type, denota1419872369iation : ((variable>real)>(variable>real)>set_variable>$o)).
% 3.65/3.90 thf(ty_x, type, x : char).
% 3.65/3.90 thf(ty_sigma, type, sigma : produc1418842292n_game).
% 3.65/3.90 thf(conj_0,conjecture,(((denota1419872369iation @ (f @ zero_zero_real)) @ omega) @ ((sup_sup_set_variable @ ((insert_variable @ (rVar @ x)) @ ((insert_variable @ (dVar @ x)) @ bot_bot_set_variable))) @ u))).
% 3.65/3.90 thf(h0,negated_conjecture,(~((((denota1419872369iation @ (f @ zero_zero_real)) @ omega) @ ((sup_sup_set_variable @ ((insert_variable @ (rVar @ x)) @ ((insert_variable @ (dVar @ x)) @ bot_bot_set_variable))) @ u)))),inference(assume_negation,[status(cth)],[conj_0])).
% 3.65/3.90 thf(h1,assumption,(~(((((denota1778088425es_ODE @ i) @ f) @ x) @ (the_trm @ (((uSubst516392818stappt @ sigma) @ ((sup_sup_set_variable @ u) @ ((insert_variable @ (rVar @ x)) @ ((insert_variable @ (dVar @ x)) @ bot_bot_set_variable)))) @ theta))))),introduced(assumption,[])).
% 3.65/3.90 thf(h2,assumption,((((denota1778088425es_ODE @ (((uSubst1599435252djoint @ sigma) @ i) @ omega)) @ f) @ x) @ theta),introduced(assumption,[])).
% 3.65/3.90 thf(h3,assumption,(![X1:trm]:(![X2:denotational_interp]:(![X3:trm]:(![X4:denotational_interp]:(![X5:char]:(![X6:real>variable>real]:((~((![X7:variable>real]:((((denota1419872369iation @ X7) @ (X6 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X5)) @ ((insert_variable @ (dVar @ X5)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X4) @ X3) @ X7) = (((denota1863255036rm_sem @ X2) @ X1) @ X7)))))) = (~(((((denota1419872369iation @ ((((((eigen__0 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6)) @ (X6 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X5)) @ ((insert_variable @ (dVar @ X5)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X4) @ X3) @ ((((((eigen__0 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6)) = (((denota1863255036rm_sem @ X2) @ X1) @ ((((((eigen__0 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6))))))))))))),introduced(assumption,[])).
% 3.65/3.90 thf(pax3, axiom, (p3=>![X70:variable, X71:set_variable, X69:set_variable]:(fsup_sup_set_variable @ (finsert_variable @ X70 @ X71) @ X69)=(finsert_variable @ X70 @ (fsup_sup_set_variable @ X71 @ X69))), file('<stdin>', pax3)).
% 3.65/3.90 thf(pax6, axiom, (p6=>![X67:set_variable]:(fsup_sup_set_variable @ fbot_bot_set_variable @ X67)=(X67)), file('<stdin>', pax6)).
% 3.65/3.90 thf(pax4, axiom, (p4=>![X67:set_variable, X68:variable, X69:set_variable]:(fsup_sup_set_variable @ X67 @ (finsert_variable @ X68 @ X69))=(finsert_variable @ X68 @ (fsup_sup_set_variable @ X67 @ X69))), file('<stdin>', pax4)).
% 3.65/3.90 thf(pax7, axiom, (p7=>![X67:set_variable]:(fsup_sup_set_variable @ X67 @ fbot_bot_set_variable)=(X67)), file('<stdin>', pax7)).
% 3.65/3.90 thf(nax87, axiom, (p87<=fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)), file('<stdin>', nax87)).
% 3.65/3.90 thf(ax85, axiom, p3, file('<stdin>', ax85)).
% 3.65/3.90 thf(ax82, axiom, p6, file('<stdin>', ax82)).
% 3.65/3.90 thf(ax1, axiom, ~(p87), file('<stdin>', ax1)).
% 3.65/3.90 thf(pax1, axiom, (p1=>fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))), file('<stdin>', pax1)).
% 3.65/3.90 thf(ax84, axiom, p4, file('<stdin>', ax84)).
% 3.65/3.90 thf(ax81, axiom, p7, file('<stdin>', ax81)).
% 3.65/3.90 thf(ax87, axiom, p1, file('<stdin>', ax87)).
% 3.65/3.90 thf(c_0_12, plain, ![X324:variable, X325:set_variable, X326:set_variable]:(~p3|(fsup_sup_set_variable @ (finsert_variable @ X324 @ X325) @ X326)=(finsert_variable @ X324 @ (fsup_sup_set_variable @ X325 @ X326))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 3.65/3.90 thf(c_0_13, plain, ![X316:set_variable]:(~p6|(fsup_sup_set_variable @ fbot_bot_set_variable @ X316)=(X316)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 3.65/3.90 thf(c_0_14, plain, ![X318:set_variable, X319:variable, X320:set_variable]:(~p4|(fsup_sup_set_variable @ X318 @ (finsert_variable @ X319 @ X320))=(finsert_variable @ X319 @ (fsup_sup_set_variable @ X318 @ X320))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 3.65/3.90 thf(c_0_15, plain, ![X314:set_variable]:(~p7|(fsup_sup_set_variable @ X314 @ fbot_bot_set_variable)=(X314)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 3.65/3.90 thf(c_0_16, plain, (~fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)|p87), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax87])])).
% 3.65/3.90 thf(c_0_17, plain, ![X2:set_variable, X14:variable, X6:set_variable]:((fsup_sup_set_variable @ (finsert_variable @ X14 @ X2) @ X6)=(finsert_variable @ X14 @ (fsup_sup_set_variable @ X2 @ X6))|~p3), inference(split_conjunct,[status(thm)],[c_0_12])).
% 3.65/3.90 thf(c_0_18, plain, p3, inference(split_conjunct,[status(thm)],[ax85])).
% 3.65/3.90 thf(c_0_19, plain, ![X2:set_variable]:((fsup_sup_set_variable @ fbot_bot_set_variable @ X2)=(X2)|~p6), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.65/3.90 thf(c_0_20, plain, p6, inference(split_conjunct,[status(thm)],[ax82])).
% 3.65/3.90 thf(c_0_21, plain, ~p87, inference(fof_simplification,[status(thm)],[ax1])).
% 3.65/3.90 thf(c_0_22, plain, (~p1|fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))), inference(fof_nnf,[status(thm)],[pax1])).
% 3.65/3.90 thf(c_0_23, plain, ![X2:set_variable, X14:variable, X6:set_variable]:((fsup_sup_set_variable @ X2 @ (finsert_variable @ X14 @ X6))=(finsert_variable @ X14 @ (fsup_sup_set_variable @ X2 @ X6))|~p4), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.65/3.90 thf(c_0_24, plain, p4, inference(split_conjunct,[status(thm)],[ax84])).
% 3.65/3.90 thf(c_0_25, plain, ![X2:set_variable]:((fsup_sup_set_variable @ X2 @ fbot_bot_set_variable)=(X2)|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 3.65/3.90 thf(c_0_26, plain, p7, inference(split_conjunct,[status(thm)],[ax81])).
% 3.65/3.90 thf(c_0_27, plain, (p87|~fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 3.65/3.90 thf(c_0_28, plain, ![X2:set_variable, X14:variable, X6:set_variable]:(fsup_sup_set_variable @ (finsert_variable @ X14 @ X2) @ X6)=(finsert_variable @ X14 @ (fsup_sup_set_variable @ X2 @ X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 3.65/3.90 thf(c_0_29, plain, ![X2:set_variable]:(fsup_sup_set_variable @ fbot_bot_set_variable @ X2)=(X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 3.65/3.90 thf(c_0_30, plain, ~p87, inference(split_conjunct,[status(thm)],[c_0_21])).
% 3.65/3.90 thf(c_0_31, plain, (fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))|~p1), inference(split_conjunct,[status(thm)],[c_0_22])).
% 3.65/3.90 thf(c_0_32, plain, ![X2:set_variable, X14:variable, X6:set_variable]:(fsup_sup_set_variable @ X2 @ (finsert_variable @ X14 @ X6))=(finsert_variable @ X14 @ (fsup_sup_set_variable @ X2 @ X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 3.65/3.90 thf(c_0_33, plain, ![X2:set_variable]:(fsup_sup_set_variable @ X2 @ fbot_bot_set_variable)=(X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 3.65/3.90 thf(c_0_34, plain, p1, inference(split_conjunct,[status(thm)],[ax87])).
% 3.65/3.90 thf(c_0_35, plain, ~fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fu)), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28]), c_0_28]), c_0_29]), c_0_30])).
% 3.65/3.90 thf(c_0_36, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32]), c_0_32]), c_0_33]), c_0_34])]), c_0_35]), ['proof']).
% 3.65/3.90 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h3,h1,h0])],[])).
% 3.65/3.90 thf(fact_153__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rr_O_A_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,(~((![X1:trm>denotational_interp>trm>denotational_interp>char>(real>variable>real)>variable>real]:(~((![X2:trm]:(![X3:denotational_interp]:(![X4:trm]:(![X5:denotational_interp]:(![X6:char]:(![X7:real>variable>real]:((~((![X8:variable>real]:((((denota1419872369iation @ X8) @ (X7 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X6)) @ ((insert_variable @ (dVar @ X6)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X5) @ X4) @ X8) = (((denota1863255036rm_sem @ X3) @ X2) @ X8)))))) = (~(((((denota1419872369iation @ ((((((X1 @ X2) @ X3) @ X4) @ X5) @ X6) @ X7)) @ (X7 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X6)) @ ((insert_variable @ (dVar @ X6)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X5) @ X4) @ ((((((X1 @ X2) @ X3) @ X4) @ X5) @ X6) @ X7)) = (((denota1863255036rm_sem @ X3) @ X2) @ ((((((X1 @ X2) @ X3) @ X4) @ X5) @ X6) @ X7))))))))))))))))))).
% 3.65/3.90 thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h3]),tab_negall(eigenvar,eigen__0)],[fact_153__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rr_O_A_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,1,h3])).
% 3.65/3.90 thf(h4,assumption,(![X1:trm]:(![X2:denotational_interp]:(![X3:trm]:(![X4:denotational_interp]:(![X5:char]:(![X6:real>variable>real]:((~((![X7:variable>real]:((((denota1419872369iation @ X7) @ (X6 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X5)) @ ((insert_variable @ (dVar @ X5)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X4) @ X3) @ X7) = (((denota1863255036rm_sem @ X2) @ X1) @ X7)))))) = (~(((((denota1419872369iation @ ((((((eigen__1 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6)) @ (X6 @ zero_zero_real)) @ ((insert_variable @ (rVar @ X5)) @ ((insert_variable @ (dVar @ X5)) @ bot_bot_set_variable))) => ((((denota1863255036rm_sem @ X4) @ X3) @ ((((((eigen__1 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6)) = (((denota1863255036rm_sem @ X2) @ X1) @ ((((((eigen__1 @ X1) @ X2) @ X3) @ X4) @ X5) @ X6))))))))))))),introduced(assumption,[])).
% 3.65/3.90 thf(pax4, axiom, (p4=>![X78:set_variable, X79:variable, X80:set_variable]:(fsup_sup_set_variable @ X78 @ (finsert_variable @ X79 @ X80))=(finsert_variable @ X79 @ (fsup_sup_set_variable @ X78 @ X80))), file('<stdin>', pax4)).
% 3.65/3.90 thf(pax7, axiom, (p7=>![X78:set_variable]:(fsup_sup_set_variable @ X78 @ fbot_bot_set_variable)=(X78)), file('<stdin>', pax7)).
% 3.65/3.90 thf(pax3, axiom, (p3=>![X81:variable, X82:set_variable, X80:set_variable]:(fsup_sup_set_variable @ (finsert_variable @ X81 @ X82) @ X80)=(finsert_variable @ X81 @ (fsup_sup_set_variable @ X82 @ X80))), file('<stdin>', pax3)).
% 3.65/3.90 thf(pax6, axiom, (p6=>![X78:set_variable]:(fsup_sup_set_variable @ fbot_bot_set_variable @ X78)=(X78)), file('<stdin>', pax6)).
% 3.65/3.90 thf(pax1, axiom, (p1=>fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))), file('<stdin>', pax1)).
% 3.65/3.90 thf(ax105, axiom, p4, file('<stdin>', ax105)).
% 3.65/3.90 thf(ax102, axiom, p7, file('<stdin>', ax102)).
% 3.65/3.90 thf(nax87, axiom, (p87<=fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)), file('<stdin>', nax87)).
% 3.65/3.90 thf(ax106, axiom, p3, file('<stdin>', ax106)).
% 3.65/3.90 thf(ax103, axiom, p6, file('<stdin>', ax103)).
% 3.65/3.90 thf(ax108, axiom, p1, file('<stdin>', ax108)).
% 3.65/3.90 thf(ax23, axiom, ~(p87), file('<stdin>', ax23)).
% 3.65/3.90 thf(c_0_12, plain, ![X387:set_variable, X388:variable, X389:set_variable]:(~p4|(fsup_sup_set_variable @ X387 @ (finsert_variable @ X388 @ X389))=(finsert_variable @ X388 @ (fsup_sup_set_variable @ X387 @ X389))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 3.65/3.90 thf(c_0_13, plain, ![X383:set_variable]:(~p7|(fsup_sup_set_variable @ X383 @ fbot_bot_set_variable)=(X383)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 3.65/3.90 thf(c_0_14, plain, ![X393:variable, X394:set_variable, X395:set_variable]:(~p3|(fsup_sup_set_variable @ (finsert_variable @ X393 @ X394) @ X395)=(finsert_variable @ X393 @ (fsup_sup_set_variable @ X394 @ X395))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 3.65/3.90 thf(c_0_15, plain, ![X385:set_variable]:(~p6|(fsup_sup_set_variable @ fbot_bot_set_variable @ X385)=(X385)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 3.65/3.90 thf(c_0_16, plain, (~p1|fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))), inference(fof_nnf,[status(thm)],[pax1])).
% 3.65/3.90 thf(c_0_17, plain, ![X4:set_variable, X8:variable, X15:set_variable]:((fsup_sup_set_variable @ X4 @ (finsert_variable @ X8 @ X15))=(finsert_variable @ X8 @ (fsup_sup_set_variable @ X4 @ X15))|~p4), inference(split_conjunct,[status(thm)],[c_0_12])).
% 3.65/3.90 thf(c_0_18, plain, p4, inference(split_conjunct,[status(thm)],[ax105])).
% 3.65/3.90 thf(c_0_19, plain, ![X4:set_variable]:((fsup_sup_set_variable @ X4 @ fbot_bot_set_variable)=(X4)|~p7), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.65/3.90 thf(c_0_20, plain, p7, inference(split_conjunct,[status(thm)],[ax102])).
% 3.65/3.90 thf(c_0_21, plain, (~fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)|p87), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax87])])).
% 3.65/3.90 thf(c_0_22, plain, ![X4:set_variable, X8:variable, X15:set_variable]:((fsup_sup_set_variable @ (finsert_variable @ X8 @ X4) @ X15)=(finsert_variable @ X8 @ (fsup_sup_set_variable @ X4 @ X15))|~p3), inference(split_conjunct,[status(thm)],[c_0_14])).
% 3.65/3.90 thf(c_0_23, plain, p3, inference(split_conjunct,[status(thm)],[ax106])).
% 3.65/3.90 thf(c_0_24, plain, ![X4:set_variable]:((fsup_sup_set_variable @ fbot_bot_set_variable @ X4)=(X4)|~p6), inference(split_conjunct,[status(thm)],[c_0_15])).
% 3.65/3.90 thf(c_0_25, plain, p6, inference(split_conjunct,[status(thm)],[ax103])).
% 3.65/3.90 thf(c_0_26, plain, (fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ fu @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)))|~p1), inference(split_conjunct,[status(thm)],[c_0_16])).
% 3.65/3.90 thf(c_0_27, plain, ![X4:set_variable, X8:variable, X15:set_variable]:(fsup_sup_set_variable @ X4 @ (finsert_variable @ X8 @ X15))=(finsert_variable @ X8 @ (fsup_sup_set_variable @ X4 @ X15)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 3.65/3.90 thf(c_0_28, plain, ![X4:set_variable]:(fsup_sup_set_variable @ X4 @ fbot_bot_set_variable)=(X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 3.65/3.90 thf(c_0_29, plain, p1, inference(split_conjunct,[status(thm)],[ax108])).
% 3.65/3.90 thf(c_0_30, plain, ~p87, inference(fof_simplification,[status(thm)],[ax23])).
% 3.65/3.90 thf(c_0_31, plain, (p87|~fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (fsup_sup_set_variable @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fbot_bot_set_variable)) @ fu)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 3.65/3.90 thf(c_0_32, plain, ![X4:set_variable, X8:variable, X15:set_variable]:(fsup_sup_set_variable @ (finsert_variable @ X8 @ X4) @ X15)=(finsert_variable @ X8 @ (fsup_sup_set_variable @ X4 @ X15)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 3.65/3.90 thf(c_0_33, plain, ![X4:set_variable]:(fsup_sup_set_variable @ fbot_bot_set_variable @ X4)=(X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 3.65/3.90 thf(c_0_34, plain, fdenota1419872369iation @ (ff @ fzero_zero_real) @ fomega @ (finsert_variable @ (frVar @ fx) @ (finsert_variable @ (fdVar @ fx) @ fu)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27]), c_0_27]), c_0_28]), c_0_29])])).
% 3.65/3.90 thf(c_0_35, plain, ~p87, inference(split_conjunct,[status(thm)],[c_0_30])).
% 3.65/3.90 thf(c_0_36, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32]), c_0_32]), c_0_33]), c_0_34])]), c_0_35]), ['proof']).
% 3.65/3.90 thf(3,plain,$false,inference(eprover,[status(thm),assumptions([h4,h2,h0])],[])).
% 3.65/3.90 thf(4,plain,$false,inference(tab_negall,[status(thm),assumptions([h2,h0]),tab_negall(discharge,[h4]),tab_negall(eigenvar,eigen__1)],[fact_153__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062rr_O_A_092_060forall_062x0_Ax1_Ax2_Ax3_Ax4_Ax5_O_A_I_092_060exists_062v6_O_AUvariation_Av6_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_Av6_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_Av6_J_A_061_A_IUvariation_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_Ix5_A0_J_A_123RVar_Ax4_M_ADVar_Ax4_125_A_092_060and_062_Aterm__sem_Ax3_Ax2_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_A_092_060noteq_062_Aterm__sem_Ax1_Ax0_A_Irr_Ax0_Ax1_Ax2_Ax3_Ax4_Ax5_J_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,3,h4])).
% 3.65/3.90 thf(fact_192_l2r,axiom,(((((denota1778088425es_ODE @ i) @ f) @ x) @ (the_trm @ (((uSubst516392818stappt @ sigma) @ ((sup_sup_set_variable @ u) @ ((insert_variable @ (rVar @ x)) @ ((insert_variable @ (dVar @ x)) @ bot_bot_set_variable)))) @ theta))) => ((((denota1778088425es_ODE @ (((uSubst1599435252djoint @ sigma) @ i) @ omega)) @ f) @ x) @ theta))).
% 3.65/3.90 thf(5,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[fact_192_l2r,2,4,h1,h2])).
% 3.65/3.90 thf(0,theorem,(((denota1419872369iation @ (f @ zero_zero_real)) @ omega) @ ((sup_sup_set_variable @ ((insert_variable @ (rVar @ x)) @ ((insert_variable @ (dVar @ x)) @ bot_bot_set_variable))) @ u)),inference(contra,[status(thm),contra(discharge,[h0])],[5,h0])).
% 3.65/3.90 % SZS output end Proof
%------------------------------------------------------------------------------