%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP153^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 : n005.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:07 PM UTC 2025
% Result : Theorem 2.07s 2.29s
% Output : Proof 2.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP153^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.34 % Computer : n005.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 18:50:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 2.07/2.29 % SZS status Theorem
% 2.07/2.29 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 2.07/2.29 % Inferences: 23
% 2.07/2.29 % SZS output start Proof
% 2.07/2.29 thf(ty_a, type, a : $tType).
% 2.07/2.29 thf(ty_product_prod_a_a, type, product_prod_a_a : $tType).
% 2.07/2.29 thf(ty_set_Product_prod_a_a, type, set_Product_prod_a_a : $tType).
% 2.07/2.29 thf(ty_set_a, type, set_a : $tType).
% 2.07/2.29 thf(ty_member_a, type, member_a : (a>set_a>$o)).
% 2.07/2.29 thf(ty_relation, type, relation : set_Product_prod_a_a).
% 2.07/2.29 thf(ty_member449909584od_a_a, type, member449909584od_a_a : (product_prod_a_a>set_Product_prod_a_a>$o)).
% 2.07/2.29 thf(ty_z, type, z : a).
% 2.07/2.29 thf(ty_y, type, y : a).
% 2.07/2.29 thf(ty_carrier, type, carrier : set_a).
% 2.07/2.29 thf(ty_product_Pair_a_a, type, product_Pair_a_a : (a>a>product_prod_a_a)).
% 2.07/2.29 thf(conj_0,conjecture,(~((((member_a @ z) @ carrier) => (~(((member_a @ y) @ carrier))))))).
% 2.07/2.29 thf(h0,negated_conjecture,(((member_a @ z) @ carrier) => (~(((member_a @ y) @ carrier)))),inference(assume_negation,[status(cth)],[conj_0])).
% 2.07/2.29 thf(h1,assumption,(~(((member_a @ z) @ carrier))),introduced(assumption,[])).
% 2.07/2.29 thf(h2,assumption,(~(((member_a @ y) @ carrier))),introduced(assumption,[])).
% 2.07/2.29 thf(h3,assumption,((member449909584od_a_a @ ((product_Pair_a_a @ z) @ y)) @ relation),introduced(assumption,[])).
% 2.07/2.29 thf(h4,assumption,((member449909584od_a_a @ ((product_Pair_a_a @ y) @ z)) @ relation),introduced(assumption,[])).
% 2.07/2.29 thf(pax9, axiom, (p9=>![X39:a, X40:a]:(fmember449909584od_a_a @ (fproduct_Pair_a_a @ X39 @ X40) @ frelation=>fmember_a @ X39 @ fcarrier)), file('<stdin>', pax9)).
% 2.07/2.29 thf(pax2, axiom, (p2=>fmember449909584od_a_a @ (fproduct_Pair_a_a @ fz @ fy) @ frelation), file('<stdin>', pax2)).
% 2.07/2.29 thf(nax52, axiom, (p52<=fmember_a @ fz @ fcarrier), file('<stdin>', nax52)).
% 2.07/2.29 thf(ax9, axiom, ~(p52), file('<stdin>', ax9)).
% 2.07/2.29 thf(ax52, axiom, p9, file('<stdin>', ax52)).
% 2.07/2.29 thf(ax59, axiom, p2, file('<stdin>', ax59)).
% 2.07/2.29 thf(c_0_6, plain, ![X227:a, X228:a]:(~p9|(~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X227 @ X228) @ frelation|fmember_a @ X227 @ fcarrier)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax9])])])).
% 2.07/2.29 thf(c_0_7, plain, (~p2|fmember449909584od_a_a @ (fproduct_Pair_a_a @ fz @ fy) @ frelation), inference(fof_nnf,[status(thm)],[pax2])).
% 2.07/2.29 thf(c_0_8, plain, (~fmember_a @ fz @ fcarrier|p52), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax52])])).
% 2.07/2.29 thf(c_0_9, plain, ~p52, inference(fof_simplification,[status(thm)],[ax9])).
% 2.07/2.29 thf(c_0_10, plain, ![X2:a, X3:a]:(fmember_a @ X2 @ fcarrier|~p9|~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X2 @ X3) @ frelation), inference(split_conjunct,[status(thm)],[c_0_6])).
% 2.07/2.29 thf(c_0_11, plain, p9, inference(split_conjunct,[status(thm)],[ax52])).
% 2.07/2.29 thf(c_0_12, plain, (fmember449909584od_a_a @ (fproduct_Pair_a_a @ fz @ fy) @ frelation|~p2), inference(split_conjunct,[status(thm)],[c_0_7])).
% 2.07/2.29 thf(c_0_13, plain, p2, inference(split_conjunct,[status(thm)],[ax59])).
% 2.07/2.29 thf(c_0_14, plain, (p52|~fmember_a @ fz @ fcarrier), inference(split_conjunct,[status(thm)],[c_0_8])).
% 2.07/2.29 thf(c_0_15, plain, ~p52, inference(split_conjunct,[status(thm)],[c_0_9])).
% 2.07/2.29 thf(c_0_16, plain, ![X2:a, X3:a]:(fmember_a @ X2 @ fcarrier|~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X2 @ X3) @ frelation), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 2.07/2.29 thf(c_0_17, plain, fmember449909584od_a_a @ (fproduct_Pair_a_a @ fz @ fy) @ frelation, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 2.07/2.29 thf(c_0_18, plain, ~fmember_a @ fz @ fcarrier, inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 2.07/2.29 thf(c_0_19, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18]), ['proof']).
% 2.07/2.29 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h3,h4,h1,h0])],[])).
% 2.07/2.29 thf(fact_0_assms,axiom,(~((((member449909584od_a_a @ ((product_Pair_a_a @ z) @ y)) @ relation) => (~(((member449909584od_a_a @ ((product_Pair_a_a @ y) @ z)) @ relation))))))).
% 2.07/2.29 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h0]),tab_negimp(discharge,[h3,h4])],[fact_0_assms,1,h3,h4])).
% 2.07/2.29 thf(pax9, axiom, (p9=>![X42:a, X43:a]:(fmember449909584od_a_a @ (fproduct_Pair_a_a @ X42 @ X43) @ frelation=>fmember_a @ X42 @ fcarrier)), file('<stdin>', pax9)).
% 2.07/2.29 thf(pax1, axiom, (p1=>fmember449909584od_a_a @ (fproduct_Pair_a_a @ fy @ fz) @ frelation), file('<stdin>', pax1)).
% 2.07/2.29 thf(nax63, axiom, (p63<=fmember_a @ fy @ fcarrier), file('<stdin>', nax63)).
% 2.07/2.29 thf(ax28, axiom, ~(p63), file('<stdin>', ax28)).
% 2.07/2.29 thf(ax71, axiom, p9, file('<stdin>', ax71)).
% 2.07/2.29 thf(ax79, axiom, p1, file('<stdin>', ax79)).
% 2.07/2.29 thf(c_0_6, plain, ![X254:a, X255:a]:(~p9|(~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X254 @ X255) @ frelation|fmember_a @ X254 @ fcarrier)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax9])])])).
% 2.07/2.29 thf(c_0_7, plain, (~p1|fmember449909584od_a_a @ (fproduct_Pair_a_a @ fy @ fz) @ frelation), inference(fof_nnf,[status(thm)],[pax1])).
% 2.07/2.29 thf(c_0_8, plain, (~fmember_a @ fy @ fcarrier|p63), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax63])])).
% 2.07/2.29 thf(c_0_9, plain, ~p63, inference(fof_simplification,[status(thm)],[ax28])).
% 2.07/2.29 thf(c_0_10, plain, ![X3:a, X5:a]:(fmember_a @ X3 @ fcarrier|~p9|~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X3 @ X5) @ frelation), inference(split_conjunct,[status(thm)],[c_0_6])).
% 2.07/2.29 thf(c_0_11, plain, p9, inference(split_conjunct,[status(thm)],[ax71])).
% 2.07/2.29 thf(c_0_12, plain, (fmember449909584od_a_a @ (fproduct_Pair_a_a @ fy @ fz) @ frelation|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 2.07/2.29 thf(c_0_13, plain, p1, inference(split_conjunct,[status(thm)],[ax79])).
% 2.07/2.29 thf(c_0_14, plain, (p63|~fmember_a @ fy @ fcarrier), inference(split_conjunct,[status(thm)],[c_0_8])).
% 2.07/2.29 thf(c_0_15, plain, ~p63, inference(split_conjunct,[status(thm)],[c_0_9])).
% 2.07/2.29 thf(c_0_16, plain, ![X3:a, X5:a]:(fmember_a @ X3 @ fcarrier|~fmember449909584od_a_a @ (fproduct_Pair_a_a @ X3 @ X5) @ frelation), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 2.07/2.29 thf(c_0_17, plain, fmember449909584od_a_a @ (fproduct_Pair_a_a @ fy @ fz) @ frelation, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 2.07/2.29 thf(c_0_18, plain, ~fmember_a @ fy @ fcarrier, inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 2.07/2.29 thf(c_0_19, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18]), ['proof']).
% 2.07/2.29 thf(3,plain,$false,inference(eprover,[status(thm),assumptions([h3,h4,h2,h0])],[])).
% 2.07/2.29 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h2,h0]),tab_negimp(discharge,[h3,h4])],[fact_0_assms,3,h3,h4])).
% 2.07/2.29 thf(5,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[h0,2,4,h1,h2])).
% 2.07/2.29 thf(0,theorem,(~((((member_a @ z) @ carrier) => (~(((member_a @ y) @ carrier)))))),inference(contra,[status(thm),contra(discharge,[h0])],[5,h0])).
% 2.07/2.29 % SZS output end Proof
%------------------------------------------------------------------------------