%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP028^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 : n012.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:45 PM UTC 2025
% Result : Theorem 1.31s 1.55s
% Output : Proof 1.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP028^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 : n012.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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 17:59:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 1.31/1.55 % SZS status Theorem
% 1.31/1.55 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 1.31/1.55 % Inferences: 640
% 1.31/1.55 % SZS output start Proof
% 1.31/1.55 thf(conj_1,conjecture,thesis).
% 1.31/1.55 thf(h0,negated_conjecture,(~(thesis)),inference(assume_negation,[status(cth)],[conj_1])).
% 1.31/1.55 thf(pax1012, axiom, (p1012=>((fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__6 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>fmember_set_a @ f__6 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc))))), file('<stdin>', pax1012)).
% 1.31/1.55 thf(ax23, axiom, (~(p1010)|p1012), file('<stdin>', ax23)).
% 1.31/1.55 thf(nax1010, axiom, (p1010<=![X5:set_set_a]:((X5)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__6 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>fmember_set_a @ f__6 @ X5)))), file('<stdin>', nax1010)).
% 1.31/1.55 thf(pax1026, axiom, (p1026=>![X1:set_set_a]:((X1)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__4 @ X1=>fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc))))), file('<stdin>', pax1026)).
% 1.31/1.55 thf(pax1030, axiom, (p1030=>![X1:set_set_a]:((X1)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>fmember_set_a @ f__4 @ X1)))), file('<stdin>', pax1030)).
% 1.31/1.55 thf(nax1026, axiom, (p1026<=![X1:set_set_a]:((X1)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__4 @ X1=>fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc))))), file('<stdin>', nax1026)).
% 1.31/1.55 thf(nax1, axiom, (p1<=fthesis), file('<stdin>', nax1)).
% 1.31/1.55 thf(ax1327, axiom, ~(p1), file('<stdin>', ax1327)).
% 1.31/1.55 thf(nax3, axiom, (p3<=![X543:set_a]:(~((~((fmember_set_a @ X543 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~(ford_less_eq_set_a @ fa1 @ X543)))=>~(ford_less_eq_set_a @ fa2 @ X543)))=>~(ford_less_eq_set_a @ fa3 @ X543))), file('<stdin>', nax3)).
% 1.31/1.55 thf(ax1325, axiom, ~(p3), file('<stdin>', ax1325)).
% 1.31/1.55 thf(pax109, axiom, (p109=>![X365:set_a]:(fmember_set_a @ X365 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>(ford_less_eq_set_a @ fa1 @ X365=>(ford_less_eq_set_a @ fa2 @ X365=>(ford_less_eq_set_a @ fa3 @ X365=>fthesis))))), file('<stdin>', pax109)).
% 1.31/1.55 thf(nax1030, axiom, (p1030<=![X1:set_set_a]:((X1)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>~((fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=>fmember_set_a @ f__4 @ X1)))), file('<stdin>', nax1030)).
% 1.31/1.55 thf(ax1219, axiom, p109, file('<stdin>', ax1219)).
% 1.31/1.55 thf(c_0_13, plain, (~p1012|(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1012])])).
% 1.31/1.55 thf(c_0_14, plain, (~p1010|p1012), inference(fof_simplification,[status(thm)],[ax23])).
% 1.31/1.55 thf(c_0_15, plain, (~p1012|(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.31/1.55 thf(c_0_16, plain, (((esk9_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1010)&(~fmember_set_a @ f__6 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|fmember_set_a @ f__6 @ esk9_0|p1010)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1010])])])])])).
% 1.31/1.55 thf(c_0_17, plain, (p1012|~p1010), inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.31/1.55 thf(c_0_18, plain, ~p1012, inference(cn,[status(thm)],[c_0_15])).
% 1.31/1.55 thf(c_0_19, plain, ![X548:set_set_a]:((fmember_set_a @ f__4 @ X548|(X548)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1026)&(~fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|(X548)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1026)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1026])])])])).
% 1.31/1.55 thf(c_0_20, plain, ((esk9_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1010), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.31/1.55 thf(c_0_21, plain, ~p1010, inference(sr,[status(thm)],[c_0_17, c_0_18])).
% 1.31/1.55 thf(c_0_22, plain, ![X1:set_set_a]:(fmember_set_a @ f__4 @ X1|(X1)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1026), inference(split_conjunct,[status(thm)],[c_0_19])).
% 1.31/1.55 thf(c_0_23, plain, (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)=(esk9_0), inference(sr,[status(thm)],[c_0_20, c_0_21])).
% 1.31/1.55 thf(c_0_24, plain, ![X546:set_set_a]:((fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|(X546)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1030)&(~fmember_set_a @ f__4 @ X546|(X546)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1030)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax1030])])])])).
% 1.31/1.55 thf(c_0_25, plain, (((esk2_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1026)&(~fmember_set_a @ f__4 @ esk2_0|fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1026)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1026])])])])])).
% 1.31/1.55 thf(c_0_26, plain, ![X1:set_set_a]:(~fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|(X1)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1026), inference(split_conjunct,[status(thm)],[c_0_19])).
% 1.31/1.55 thf(c_0_27, plain, (fmember_set_a @ f__4 @ esk9_0|~p1026), inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.31/1.55 thf(c_0_28, plain, ![X1:set_set_a]:(~fmember_set_a @ f__4 @ X1|(X1)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1030), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.31/1.55 thf(c_0_29, plain, ((esk2_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1026), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.31/1.55 thf(c_0_30, plain, ~p1026, inference(er,[status(thm)],[inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_23]), c_0_23]), c_0_27])])).
% 1.31/1.55 thf(c_0_31, plain, (~fthesis|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 1.31/1.55 thf(c_0_32, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1327])).
% 1.31/1.55 thf(c_0_33, plain, (~fmember_set_a @ f__4 @ esk9_0|~p1030), inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_23])])).
% 1.31/1.55 thf(c_0_34, plain, (esk9_0)=(esk2_0), inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_29, c_0_30]), c_0_23])).
% 1.31/1.55 thf(c_0_35, plain, ((((fmember_set_a @ esk956_0 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p3)&(ford_less_eq_set_a @ fa1 @ esk956_0|p3))&(ford_less_eq_set_a @ fa2 @ esk956_0|p3))&(ford_less_eq_set_a @ fa3 @ esk956_0|p3)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])])])])).
% 1.31/1.55 thf(c_0_36, plain, ~p3, inference(fof_simplification,[status(thm)],[ax1325])).
% 1.31/1.55 thf(c_0_37, plain, ![X1994:set_a]:(~p109|(~fmember_set_a @ X1994 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|(~ford_less_eq_set_a @ fa1 @ X1994|(~ford_less_eq_set_a @ fa2 @ X1994|(~ford_less_eq_set_a @ fa3 @ X1994|fthesis))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax109])])])).
% 1.31/1.55 thf(c_0_38, plain, (p1|~fthesis), inference(split_conjunct,[status(thm)],[c_0_31])).
% 1.31/1.55 thf(c_0_39, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_32])).
% 1.31/1.55 thf(c_0_40, plain, (((esk1_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1030)&(~fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|fmember_set_a @ f__4 @ esk1_0|p1030)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1030])])])])])).
% 1.31/1.55 thf(c_0_41, plain, ![X1:set_set_a]:(fmember_set_a @ f__4 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|(X1)!=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~p1030), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.31/1.55 thf(c_0_42, plain, (~fmember_set_a @ f__4 @ esk2_0|~p1030), inference(rw,[status(thm)],[c_0_33, c_0_34])).
% 1.31/1.55 thf(c_0_43, plain, (fmember_set_a @ esk956_0 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p3), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.31/1.55 thf(c_0_44, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_36])).
% 1.31/1.55 thf(c_0_45, plain, ![X24:set_a]:(fthesis|~p109|~fmember_set_a @ X24 @ (fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|~ford_less_eq_set_a @ fa1 @ X24|~ford_less_eq_set_a @ fa2 @ X24|~ford_less_eq_set_a @ fa3 @ X24), inference(split_conjunct,[status(thm)],[c_0_37])).
% 1.31/1.55 thf(c_0_46, plain, p109, inference(split_conjunct,[status(thm)],[ax1219])).
% 1.31/1.55 thf(c_0_47, plain, ~fthesis, inference(sr,[status(thm)],[c_0_38, c_0_39])).
% 1.31/1.55 thf(c_0_48, plain, ((esk1_0)=(fimage_64240033_set_a @ fproduc1040928388_a_a_e @ fc)|p1030), inference(split_conjunct,[status(thm)],[c_0_40])).
% 1.31/1.55 thf(c_0_49, plain, ~p1030, inference(er,[status(thm)],[inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_23]), c_0_34]), c_0_23]), c_0_34]), c_0_42])])).
% 1.31/1.55 thf(c_0_50, plain, fmember_set_a @ esk956_0 @ esk9_0, inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_23]), c_0_44])).
% 1.31/1.55 thf(c_0_51, plain, ![X24:set_a]:(~ford_less_eq_set_a @ fa2 @ X24|~ford_less_eq_set_a @ fa1 @ X24|~ford_less_eq_set_a @ fa3 @ X24|~fmember_set_a @ X24 @ esk2_0), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_23]), c_0_34])]), c_0_47])).
% 1.31/1.55 thf(c_0_52, plain, (esk2_0)=(esk1_0), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_48, c_0_49]), c_0_23]), c_0_34])).
% 1.31/1.55 thf(c_0_53, plain, (ford_less_eq_set_a @ fa3 @ esk956_0|p3), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.31/1.55 thf(c_0_54, plain, (ford_less_eq_set_a @ fa2 @ esk956_0|p3), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.31/1.55 thf(c_0_55, plain, (ford_less_eq_set_a @ fa1 @ esk956_0|p3), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.31/1.55 thf(c_0_56, plain, fmember_set_a @ esk956_0 @ esk2_0, inference(rw,[status(thm)],[c_0_50, c_0_34])).
% 1.31/1.55 thf(c_0_57, plain, ![X24:set_a]:(~ford_less_eq_set_a @ fa2 @ X24|~ford_less_eq_set_a @ fa1 @ X24|~ford_less_eq_set_a @ fa3 @ X24|~fmember_set_a @ X24 @ esk1_0), inference(rw,[status(thm)],[c_0_51, c_0_52])).
% 1.31/1.55 thf(c_0_58, plain, ford_less_eq_set_a @ fa3 @ esk956_0, inference(sr,[status(thm)],[c_0_53, c_0_44])).
% 1.31/1.55 thf(c_0_59, plain, ford_less_eq_set_a @ fa2 @ esk956_0, inference(sr,[status(thm)],[c_0_54, c_0_44])).
% 1.31/1.55 thf(c_0_60, plain, ford_less_eq_set_a @ fa1 @ esk956_0, inference(sr,[status(thm)],[c_0_55, c_0_44])).
% 1.31/1.55 thf(c_0_61, plain, fmember_set_a @ esk956_0 @ esk1_0, inference(rw,[status(thm)],[c_0_56, c_0_52])).
% 1.31/1.55 thf(c_0_62, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_58]), c_0_59]), c_0_60]), c_0_61])]), ['proof']).
% 1.31/1.55 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.31/1.55 thf(0,theorem,thesis,inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.31/1.55 % SZS output end Proof
%------------------------------------------------------------------------------