%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP083^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 : n023.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:46:55 PM UTC 2025
% Result : Theorem 0.38s 0.58s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP083^1 : TPTP v9.2.0. Released v7.5.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.36 % Computer : n023.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8042.1875MB
% 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Wed Oct 8 18:46:08 EDT 2025
% 0.12/0.36 % CPUTime :
% 0.38/0.58 % SZS status Theorem
% 0.38/0.58 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.38/0.58 % Inferences: 0
% 0.38/0.58 % SZS output start Proof
% 0.38/0.58 thf(ty_set_val, type, set_val : $tType).
% 0.38/0.58 thf(ty_option_list_val, type, option_list_val : $tType).
% 0.38/0.58 thf(ty_val, type, val : $tType).
% 0.38/0.58 thf(ty_node, type, node : $tType).
% 0.38/0.58 thf(ty_produc1432036078de_val, type, produc1432036078de_val : $tType).
% 0.38/0.58 thf(ty_list_node, type, list_node : $tType).
% 0.38/0.58 thf(ty_g, type, g : $tType).
% 0.38/0.58 thf(ty_phi_s, type, phi_s : val).
% 0.38/0.58 thf(ty_alpha_n, type, alpha_n : (g>list_node)).
% 0.38/0.58 thf(ty_sSA_CF1252180629de_val, type, sSA_CF1252180629de_val : ((g>list_node)>(g>node>set_val)>(g>produc1432036078de_val>option_list_val)>g>val>val>$o)).
% 0.38/0.58 thf(ty_eigen__0, type, eigen__0 : val).
% 0.38/0.58 thf(ty_g2, type, g2 : g).
% 0.38/0.58 thf(ty_defs, type, defs : (g>node>set_val)).
% 0.38/0.58 thf(ty_phis, type, phis : (g>produc1432036078de_val>option_list_val)).
% 0.38/0.58 thf(conj_0,conjecture,((member_val @ phi_s) @ ((((((sSA_CF1517915011eD_val @ alpha_n) @ inEdges) @ defs) @ uses) @ phis) @ g2))).
% 0.38/0.58 thf(h0,negated_conjecture,(~(((member_val @ phi_s) @ ((((((sSA_CF1517915011eD_val @ alpha_n) @ inEdges) @ defs) @ uses) @ phis) @ g2)))),inference(assume_negation,[status(cth)],[conj_0])).
% 0.38/0.58 thf(h1,assumption,((((((sSA_CF1252180629de_val @ alpha_n) @ defs) @ phis) @ g2) @ eigen__0) @ phi_s),introduced(assumption,[])).
% 0.38/0.58 thf(pax29, axiom, (p29=>![X16:val, X17:g]:(fmember_val @ X16 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X17)=>fmember_val @ X16 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X17 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X17 @ X16)))), file('<stdin>', pax29)).
% 0.38/0.58 thf(pax12, axiom, (p12=>(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s)=(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fs)), file('<stdin>', pax12)).
% 0.38/0.58 thf(pax4, axiom, (p4=>fmember_val @ fs @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ fg2)), file('<stdin>', pax4)).
% 0.38/0.58 thf(pax34, axiom, (p34=>(fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fs)), file('<stdin>', pax34)).
% 0.38/0.58 thf(pax39, axiom, (p39=>(fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fphi_s)), file('<stdin>', pax39)).
% 0.38/0.58 thf(pax24, axiom, (p24=>![X23:val, X24:g]:(fmember_val @ X23 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X24)=>fmember_node @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X24 @ X23) @ (fset_node2 @ (falpha_n @ X24)))), file('<stdin>', pax24)).
% 0.38/0.58 thf(pax40, axiom, (p40=>![X5:node, X2:g, X3:val, X6:val]:(fmember_node @ X5 @ (fset_node2 @ (falpha_n @ X2))=>(fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X5)=>(fmember_val @ X6 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X5)=>(~((X3)=(X6))=>~((fvar2 @ X2 @ X6)=(fvar2 @ X2 @ X3))))))), file('<stdin>', pax40)).
% 0.38/0.58 thf(ax12, axiom, p29, file('<stdin>', ax12)).
% 0.38/0.58 thf(ax29, axiom, p12, file('<stdin>', ax29)).
% 0.38/0.58 thf(ax37, axiom, p4, file('<stdin>', ax37)).
% 0.38/0.58 thf(ax7, axiom, p34, file('<stdin>', ax7)).
% 0.38/0.58 thf(ax2, axiom, p39, file('<stdin>', ax2)).
% 0.38/0.58 thf(ax17, axiom, p24, file('<stdin>', ax17)).
% 0.38/0.58 thf(pax7, axiom, (p7=>![X50:g, X51:val, X52:val]:(fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ X50 @ X51 @ X52=>fmember_val @ X52 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X50))), file('<stdin>', pax7)).
% 0.38/0.58 thf(pax3, axiom, (p3=>fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi2 @ fphi_s), file('<stdin>', pax3)).
% 0.38/0.58 thf(ax1, axiom, p40, file('<stdin>', ax1)).
% 0.38/0.58 thf(ax34, axiom, p7, file('<stdin>', ax34)).
% 0.38/0.58 thf(ax38, axiom, p3, file('<stdin>', ax38)).
% 0.38/0.58 thf(nax1, axiom, (p1<=(fphi_s)=(fs)), file('<stdin>', nax1)).
% 0.38/0.58 thf(ax40, axiom, ~(p1), file('<stdin>', ax40)).
% 0.38/0.58 thf(c_0_20, plain, ![X121:val, X122:g]:(~p29|(~fmember_val @ X121 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X122)|fmember_val @ X121 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X122 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X122 @ X121)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax29])])])).
% 0.38/0.58 thf(c_0_21, plain, (~p12|(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s)=(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fs)), inference(fof_nnf,[status(thm)],[pax12])).
% 0.38/0.58 thf(c_0_22, plain, (~p4|fmember_val @ fs @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ fg2)), inference(fof_nnf,[status(thm)],[pax4])).
% 0.38/0.58 thf(c_0_23, plain, (~p34|(fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fs)), inference(fof_nnf,[status(thm)],[pax34])).
% 0.38/0.58 thf(c_0_24, plain, (~p39|(fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fphi_s)), inference(fof_nnf,[status(thm)],[pax39])).
% 0.38/0.58 thf(c_0_25, plain, ![X145:val, X146:g]:(~p24|(~fmember_val @ X145 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X146)|fmember_node @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X146 @ X145) @ (fset_node2 @ (falpha_n @ X146)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax24])])])).
% 0.38/0.58 thf(c_0_26, plain, ![X65:node, X66:g, X67:val, X68:val]:(~p40|(~fmember_node @ X65 @ (fset_node2 @ (falpha_n @ X66))|(~fmember_val @ X67 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X66 @ X65)|(~fmember_val @ X68 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X66 @ X65)|((X67)=(X68)|(fvar2 @ X66 @ X68)!=(fvar2 @ X66 @ X67)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax40])])])])).
% 0.38/0.58 thf(c_0_27, plain, ![X3:val, X2:g]:(fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X2 @ X3))|~p29|~fmember_val @ X3 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.38/0.58 thf(c_0_28, plain, p29, inference(split_conjunct,[status(thm)],[ax12])).
% 0.38/0.58 thf(c_0_29, plain, ((fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s)=(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fs)|~p12), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.38/0.58 thf(c_0_30, plain, p12, inference(split_conjunct,[status(thm)],[ax29])).
% 0.38/0.58 thf(c_0_31, plain, (fmember_val @ fs @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ fg2)|~p4), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.38/0.58 thf(c_0_32, plain, p4, inference(split_conjunct,[status(thm)],[ax37])).
% 0.38/0.58 thf(c_0_33, plain, ((fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fs)|~p34), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.38/0.58 thf(c_0_34, plain, p34, inference(split_conjunct,[status(thm)],[ax7])).
% 0.38/0.58 thf(c_0_35, plain, ((fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fphi_s)|~p39), inference(split_conjunct,[status(thm)],[c_0_24])).
% 0.38/0.58 thf(c_0_36, plain, p39, inference(split_conjunct,[status(thm)],[ax2])).
% 0.38/0.58 thf(c_0_37, plain, ![X3:val, X2:g]:(fmember_node @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X2 @ X3) @ (fset_node2 @ (falpha_n @ X2))|~p24|~fmember_val @ X3 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.38/0.58 thf(c_0_38, plain, p24, inference(split_conjunct,[status(thm)],[ax17])).
% 0.38/0.58 thf(c_0_39, plain, ![X221:g, X222:val, X223:val]:(~p7|(~fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ X221 @ X222 @ X223|fmember_val @ X223 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X221))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 0.38/0.58 thf(c_0_40, plain, (~p3|fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi2 @ fphi_s), inference(fof_nnf,[status(thm)],[pax3])).
% 0.38/0.58 thf(c_0_41, plain, ![X1:node, X2:g, X4:val, X3:val]:((X3)=(X4)|~p40|~fmember_node @ X1 @ (fset_node2 @ (falpha_n @ X2))|~fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X1)|~fmember_val @ X4 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X1)|(fvar2 @ X2 @ X4)!=(fvar2 @ X2 @ X3)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.38/0.58 thf(c_0_42, plain, p40, inference(split_conjunct,[status(thm)],[ax1])).
% 0.38/0.58 thf(c_0_43, plain, ![X3:val, X2:g]:(fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X2 @ X3))|~fmember_val @ X3 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_28])])).
% 0.38/0.58 thf(c_0_44, plain, (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fs)=(fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 0.38/0.58 thf(c_0_45, plain, fmember_val @ fs @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ fg2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 0.38/0.58 thf(c_0_46, plain, (fvar2 @ fg2 @ fs)=(fvar2 @ fg2 @ fphi), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 0.38/0.58 thf(c_0_47, plain, (fvar2 @ fg2 @ fphi)=(fvar2 @ fg2 @ fphi_s), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 0.38/0.58 thf(c_0_48, plain, ![X3:val, X2:g]:(fmember_node @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ X2 @ X3) @ (fset_node2 @ (falpha_n @ X2))|~fmember_val @ X3 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 0.38/0.58 thf(c_0_49, plain, ![X2:g, X3:val, X4:val]:(fmember_val @ X4 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)|~p7|~fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ X2 @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.38/0.58 thf(c_0_50, plain, p7, inference(split_conjunct,[status(thm)],[ax34])).
% 0.38/0.58 thf(c_0_51, plain, (fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi2 @ fphi_s|~p3), inference(split_conjunct,[status(thm)],[c_0_40])).
% 0.38/0.58 thf(c_0_52, plain, p3, inference(split_conjunct,[status(thm)],[ax38])).
% 0.38/0.58 thf(c_0_53, plain, ((fphi_s)!=(fs)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 0.38/0.58 thf(c_0_54, plain, ~p1, inference(fof_simplification,[status(thm)],[ax40])).
% 0.38/0.58 thf(c_0_55, plain, ![X1:node, X4:val, X3:val, X2:g]:((X3)=(X4)|(fvar2 @ X2 @ X3)!=(fvar2 @ X2 @ X4)|~fmember_val @ X4 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X1)|~fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ X2 @ X1)|~fmember_node @ X1 @ (fset_node2 @ (falpha_n @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 0.38/0.58 thf(c_0_56, plain, fmember_val @ fs @ (fsSA_CF139593942de_val @ fdefs @ fphis @ fg2 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])])).
% 0.38/0.58 thf(c_0_57, plain, (fvar2 @ fg2 @ fs)=(fvar2 @ fg2 @ fphi_s), inference(rw,[status(thm)],[c_0_46, c_0_47])).
% 0.38/0.58 thf(c_0_58, plain, fmember_node @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s) @ (fset_node2 @ (falpha_n @ fg2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_44]), c_0_45])])).
% 0.38/0.58 thf(c_0_59, plain, ![X2:g, X4:val, X3:val]:(fmember_val @ X3 @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ X2)|~fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ X2 @ X4 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 0.38/0.58 thf(c_0_60, plain, fsSA_CF1252180629de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi2 @ fphi_s, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_52])])).
% 0.38/0.58 thf(c_0_61, plain, (p1|(fphi_s)!=(fs)), inference(split_conjunct,[status(thm)],[c_0_53])).
% 0.38/0.58 thf(c_0_62, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.38/0.58 thf(c_0_63, plain, ![X3:val]:((X3)=(fs)|(fvar2 @ fg2 @ X3)!=(fvar2 @ fg2 @ fphi_s)|~fmember_val @ X3 @ (fsSA_CF139593942de_val @ fdefs @ fphis @ fg2 @ (fsSA_CF551432799de_val @ falpha_n @ fdefs @ fphis @ fg2 @ fphi_s))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_57]), c_0_58])])).
% 0.38/0.58 thf(c_0_64, plain, fmember_val @ fphi_s @ (fsSA_CF1517915011eD_val @ falpha_n @ finEdges @ fdefs @ fuses @ fphis @ fg2), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 0.38/0.58 thf(c_0_65, plain, (fs)!=(fphi_s), inference(sr,[status(thm)],[c_0_61, c_0_62])).
% 0.38/0.58 thf(c_0_66, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_43]), c_0_64])]), c_0_65]), ['proof']).
% 0.38/0.58 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h1,h0])],[])).
% 0.38/0.58 thf(fact_5__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062_092_060phi_062_H_O_AphiArg_Ag_A_092_060phi_062_H_A_092_060phi_062_092_060_094sub_062s_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,axiom,(~((![X1:val]:(~(((((((sSA_CF1252180629de_val @ alpha_n) @ defs) @ phis) @ g2) @ X1) @ phi_s))))))).
% 0.38/0.58 thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[fact_5__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062_092_060phi_062_H_O_AphiArg_Ag_A_092_060phi_062_H_A_092_060phi_062_092_060_094sub_062s_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062,1,h1])).
% 0.38/0.58 thf(0,theorem,((member_val @ phi_s) @ ((((((sSA_CF1517915011eD_val @ alpha_n) @ inEdges) @ defs) @ uses) @ phis) @ g2)),inference(contra,[status(thm),contra(discharge,[h0])],[2,h0])).
% 0.38/0.58 % SZS output end Proof
%------------------------------------------------------------------------------